fix printing of

abstract_syntax.py

@@ -499,7 +499,8 @@ def __eq__(self, other):
 
   def __str__(self):
       if isinstance(self.resolved_names, str):
-        error(self.location, 'resolved_names is a string but should be a list: ' \
+        error(self.location,
+              'resolved_names is a string but should be a list: ' \
               + self.resolved_names)
 
       if base_name(self.name) == 'zero' and not get_verbose():
@@ -509,8 +510,14 @@ def __str__(self):
       elif get_verbose():
         return self.name + '{' + ','.join(self.resolved_names) + '}'
       else:
-        return base_name(self.name)
+        if is_operator(self):
+          return 'operator ' + base_name(self.name)
+        else:
+          return base_name(self.name)
 
+  def operator_str(self):
+    return base_name(self.name)
+
   def reduce(self, env):
       if get_reduce_all() or (self in get_reduce_only()):
         res = env.get_value_of_term_var(self)
@@ -757,8 +764,10 @@ def copy(self):
 
   def __str__(self):
     if self.infix:
-      return op_arg_str(self, self.args[0]) + " " + str(self.rator) \
+      return op_arg_str(self, self.args[0]) + " " + operator_name(self.rator) \
         + " " + op_arg_str(self, self.args[1])
+    elif is_operator(self.rator): # prefix operator
+      return operator_name(self.rator) + " " + op_arg_str(self, self.args[0])
     elif isNat(self) and not get_verbose():
       return str(natToInt(self))
     elif isDeduceInt(self):
@@ -1320,7 +1329,9 @@ def copy(self):
   def __str__(self):
     match self.conclusion:
       case Bool(loc, tyof, False):
-        return 'not (' + str(self.premise) + ')'
+        return str(Call(self.location, self.typeof,
+                        Var(self.location, None, 'not'),
+                        [self.premise], False))
       case _:
         return '(if ' + str(self.premise) \
           + ' then ' + str(self.conclusion) + ')'

deduce.py

@@ -36,7 +36,8 @@ def deduce_file(filename, error_expected):
                 ast = parser.parse(program_text, trace=get_verbose(),
                                    error_expected=error_expected)
             if get_verbose():
-                print("abstract syntax tree:\n"+'\n'.join([str(s) for s in ast])+"\n\n")
+                print("abstract syntax tree:\n" \
+                      +'\n'.join([str(s) for s in ast])+"\n\n")
                 print("starting uniquify:\n" + '\n'.join([str(d) for d in ast]))
             uniquify_deduce(ast)
             if get_verbose():

test/should-error/all4.pf.err

@@ -2,9 +2,9 @@
 Could not prove that
 	P
 implies
-	not (P)
+	not P
 
 While trying to prove that
 	(all P:bool. P)
 implies
-	(all Q:bool. not (Q))
+	(all Q:bool. not Q)

test/should-error/all_intro_advice_partial.pf.err

@@ -1,10 +1,10 @@
 ./test/should-error/all_intro_advice_partial.pf:6.3-6.4: incomplete proof
 Goal:
-	(all y:bool, z:bool, w:bool. (all n:bool. (x or y or y or not (x))))
+	(all y:bool, z:bool, w:bool. (all n:bool. (x or y or y or not x)))
 Advice:
 	You can complete the proof with:
 		arbitrary y:bool
 	followed by a proof of:
-		(all z:bool, w:bool. (all n:bool. (x or y or y or not (x))))
+		(all z:bool, w:bool. (all n:bool. (x or y or y or not x)))
 Givens:
 

test/should-error/prefix_operator.pf.err

@@ -0,0 +1,10 @@
+./test/should-error/prefix_operator.pf:4.3-4.4: incomplete proof
+Goal:
+	not false
+Advice:
+	You can complete the proof with:
+		assume label: false
+	followed by a proof of:
+		false
+Givens:
+

test/should-error/sum_foldr.pf

@@ -0,0 +1,20 @@
+import List
+import Nat
+
+function sum(List<Nat>) -> Nat {
+  sum(empty) = 0
+  sum(node(n, ns)) = n + sum(ns)
+}
+
+
+theorem foldr_eq_sum : all ls : List<Nat>. sum(ls) = foldr(ls, 0, operator+)
+proof
+  induction List<Nat>
+  case empty {
+    suffices ? by definition sum
+    ?
+  }
+  case node(a, d) {
+    ?
+  }
+end

test/should-error/sum_foldr.pf.err

@@ -0,0 +1,14 @@
+./test/should-error/sum_foldr.pf:14.5-14.33: 
+suffices to prove:
+	0 = foldr([], 0, operator +)
+./test/should-error/sum_foldr.pf:15.5-15.6: incomplete proof
+Goal:
+	0 = foldr([], 0, operator +)
+Advice:
+	To prove this equality, one of these statements might help:
+		definition
+		rewrite
+		equations
+
+Givens:
+