improve handling of PTuple in check_proof_of

error.py

@@ -49,6 +49,12 @@ def warning(location, msg):
 def error(location, msg):
   raise Exception(error_header(location) + msg)
 
+class IncompleteProof(Exception):
+  pass
+
+def incomplete_error(location, msg):
+  raise IncompleteProof(error_header(location) + msg)
+
 def last_error(location, msg):
   e = Exception(error_header(location) + msg)
   e.last = True

proof_checker.py

@@ -19,7 +19,7 @@
 #    and run the print and assert statements.
 
 from abstract_syntax import *
-from error import error, warning, error_header, get_verbose, set_verbose
+from error import error, incomplete_error, warning, error_header, get_verbose, set_verbose, IncompleteProof
 
 imported_modules = set()
 checked_modules = set()
@@ -410,7 +410,7 @@ def check_proof(proof, env):
       ret = new_formula
 
     case PHole(loc):
-      error(loc, 'unfinished proof')
+      incomplete_error(loc, 'unfinished proof')
 
     case PSorry(loc):
       error(loc, "can't use sorry in context with unkown goal")
@@ -908,9 +908,9 @@ def check_proof_of(proof, formula, env):
     print('\t' + str(proof))
   match proof:
     case PHole(loc):
-      error(loc, 'incomplete proof\nGoal:\n\t' + str(formula) + '\n'\
-            + proof_advice(formula, env) + '\n' \
-            + 'Givens:\n' + env.proofs_str())
+      incomplete_error(loc, 'incomplete proof\nGoal:\n\t' + str(formula) + '\n'\
+                       + proof_advice(formula, env) + '\n' \
+                       + 'Givens:\n' + env.proofs_str())
 
     case PSorry(loc):
       warning(loc, 'unfinished proof')
@@ -1171,17 +1171,26 @@ def check_proof_of(proof, formula, env):
         check_proof_of(reason, imp, env)
         check_proof_of(rest, claim_red, env)
 
-    # Want something like the following to help with interactive proof development, but
-    # it need to be smarter than the following. -Jeremy
-    # case PTuple(loc, pfs):
-    #   match formula:
-    #     case And(loc, frms):
-    #       for (frm,pf) in zip(frms, pfs):
-    #         print('PTuple\n\tfrm: ' + str(frm) + '\n\t' + str(pf))
-    #         check_proof_of(pf, frm, env)
-    #     case _:
-    #       error(loc, 'the comma proof operator is for logical and, not ' + str(formula))
-
+    case PTuple(loc, pfs):
+      try:
+        match formula:
+          case And(loc2, tyof2, frms):
+            if len(frms) == len(pfs):
+              for (frm,pf) in zip(frms, pfs):
+                check_proof_of(pf, frm, env)
+            else:
+              error(loc, 'expected ' + str(len(frms)) + ' proofs but only got '\
+                    + str(len(pfs)))
+          case _:
+            error(loc, 'comma proves logical-and, not ' + str(formula))
+      except IncompleteProof as ex:
+        raise ex
+      except Exception as ex:
+        form = check_proof(proof, env)
+        form_red = form.reduce(env)
+        formula_red = formula.reduce(env)
+        check_implies(proof.location, form_red, remove_mark(formula_red))
+
     case Cases(loc, subject, cases):
       sub_frm = check_proof(subject, env)
       match sub_frm:

test/should-error/inst-type-square-bracket.pf.err

@@ -1,5 +1,5 @@
 ./test/should-error/inst-type-square-bracket.pf:8.3-8.12: to instantiate:
-	prem : (all T:type. (all xs:List<T>. map(xs, λx:T{x}) = xs))
+	prem : (all T:type. (all xs:List<T>. map(xs, fun x:T{x}) = xs))
 with type arguments, instead write:
 	prem<Nat>
 

test/should-error/inst_type_forget.pf.err

@@ -1,3 +1,3 @@
 ./test/should-error/inst_type_forget.pf:8.3-8.22: In instantiation of
-	prem : (all T:type. (all xs:List<T>. map(xs, λx:T{x}) = xs))
+	prem : (all T:type. (all xs:List<T>. map(xs, fun x:T{x}) = xs))
 expected a type argument, but was given 'node(1, [])'

test/should-error/lambda_synth.pf.err

@@ -1,2 +1,2 @@
-./test/should-error/lambda_synth.pf:3.15-3.31: Cannot synthesize a type for λh,w{h * w}.
+./test/should-error/lambda_synth.pf:3.15-3.31: Cannot synthesize a type for fun h,w{h * w}.
 Add type annotations to the parameters.