Suffices terminst advice

abstract_syntax.py

@@ -891,9 +891,21 @@ def reduce(self, env):
     return ret
 
   def substitute(self, sub):
-    ret = Call(self.location, self.typeof, self.rator.substitute(sub),
-                [arg.substitute(sub) for arg in self.args],
-                self.infix)
+    # TODO: factor out this internal helper function
+    def annot_terminsts(l):
+      if isinstance(l, TermInst):
+        l.inferred = False
+      return l
+
+    fun = self.rator.substitute(sub)
+    if isinstance(fun, TermInst):
+      ret = Call(self.location, self.typeof, fun,
+                    [annot_terminsts(arg.substitute(sub)) for arg in self.args],
+                    self.infix)
+    else:
+      ret = Call(self.location, self.typeof, fun,
+                    [arg.substitute(sub) for arg in self.args],
+                    self.infix)
     if hasattr(self, 'type_args'):
       ret.type_args = self.type_args
     return ret

proof_checker.py

@@ -1251,12 +1251,7 @@ def check_proof_of(proof, formula, env):
 
             trm = pattern_to_term(indcase.pattern)
             new_trm = type_check_term(trm, typ, body_env, None, [])
-            # The following type synthesis step is because the term may get
-            # inserted into a synthesis context, and if its
-            # a TermInst, it needs to be marked as not-inferred so that it
-            # gets printed. -Jeremy
-            newer_trm = type_synth_term(new_trm, body_env, None, [])
-            pre_goal = instantiate(loc, formula, newer_trm)
+            pre_goal = instantiate(loc, formula, new_trm)
             goal = check_formula(pre_goal, body_env)
 
             for ((x,frm1),frm2) in zip(indcase.induction_hypotheses, induction_hypotheses):
@@ -1349,7 +1344,7 @@ def check_proof_of(proof, formula, env):
                                                                constr_params))
 
                 new_subject_case = type_check_term(subject_case, ty, body_env, None, [])
-                new_subject_case = type_synth_term(new_subject_case, body_env, None, [])
+                # new_subject_case = type_synth_term(new_subject_case, body_env, None, [])
 
                 assumptions = [(label,check_formula(asm, body_env) if asm else None) for (label,asm) in scase.assumptions]
                 if len(assumptions) == 1:

test/should-error/suffices_terminst1.pf

@@ -0,0 +1,8 @@
+import List
+import Nat
+
+theorem l1 : length(node(1, empty)) = 1
+proof
+  suffices ? by definition length 
+  ?
+end

test/should-error/suffices_terminst1.pf.err

@@ -0,0 +1,14 @@
+./test/should-error/suffices_terminst1.pf:6.3-6.34: 
+suffices to prove:
+	1 + length(@[]<Nat>) = 1
+./test/should-error/suffices_terminst1.pf:7.3-7.4: incomplete proof
+Goal:
+	1 + length(@[]<Nat>) = 1
+Advice:
+	To prove this equality, one of these statements might help:
+		definition
+		rewrite
+		equations
+
+Givens:
+

test/should-error/suffices_terminst2.pf

@@ -0,0 +1,8 @@
+import List
+import Nat
+
+theorem l1 : length(node(1, node(2, empty))) = 2
+proof
+  suffices ? by definition length 
+  ?
+end

test/should-error/suffices_terminst2.pf.err

@@ -0,0 +1,14 @@
+./test/should-error/suffices_terminst2.pf:6.3-6.34: 
+suffices to prove:
+	1 + length([2]) = 2
+./test/should-error/suffices_terminst2.pf:7.3-7.4: incomplete proof
+Goal:
+	1 + length([2]) = 2
+Advice:
+	To prove this equality, one of these statements might help:
+		definition
+		rewrite
+		equations
+
+Givens:
+