new feature: evaluate

Deduce.lark

@@ -176,6 +176,8 @@ ident: IDENT              -> ident
     | "enable" ident proof                               -> enable_def
     | "_rewrite" proof_list proof                         -> rewrite_goal
     | "rewrite" proof_list "in" proof                    -> rewrite_fact
+    | "evaluate"                                         -> eval_goal
+    | "evaluate" "in" proof                              -> eval_fact
     | "switch" term "{" switch_pf_case_list "}"          -> switch_proof
     | "switch" term "for" ident_list "{" switch_pf_case_list "}" -> switch_proof_for
     | "equations" equation equation_list                 -> equations_proof

abstract_syntax.py

@@ -1991,6 +1991,25 @@ def uniquify(self, env):
     for c in self.cases:
       c.uniquify(env)
 
+@dataclass
+class EvaluateGoal(Proof):
+
+  def __str__(self):
+    return 'evaluate'
+
+  def uniquify(self, env):
+    pass
+
+@dataclass
+class EvaluateFact(Proof):
+  subject: Proof
+
+  def __str__(self):
+    return 'evaluate ' + str(self.subject)
+
+  def uniquify(self, env):
+    self.subject.uniquify(env)
+
 @dataclass
 class ApplyDefs(Proof):
   definitions: List[Term]

parser.py

@@ -494,6 +494,11 @@ def parse_tree_to_ast(e, parent):
         body = parse_tree_to_ast(e.children[1], e)
         return ApplyDefsGoal(e.meta, [Var(e.meta, None, t, []) for t in definitions],
                              body)
+    elif e.data == 'eval_goal':
+        return EvaluateGoal(e.meta)
+    elif e.data == 'eval_fact':
+        subject = parse_tree_to_ast(e.children[0], e)
+        return EvaluateFact(e.meta, subject)
     elif e.data == 'apply_defs_goal_one':
         definition = parse_tree_to_ast(e.children[0], e)
         body = parse_tree_to_ast(e.children[1], e)

proof_checker.py

@@ -371,20 +371,29 @@ def check_proof(proof, env):
           ret = results[0]
       else:
           error(loc, 'expected some facts after `recall`')
-
+
+    case EvaluateFact(loc, subject):
+      formula = check_proof(subject, env)
+      set_reduce_all(True)
+      red_formula = formula.reduce(env)
+      set_reduce_all(False)
+      ret = red_formula
+
     case ApplyDefsFact(loc, definitions, subject):
       defs = [type_synth_term(d, env, None, []) for d in definitions]
       defs = [d.reduce(env) for d in defs]
       formula = check_proof(subject, env)
       new_formula = apply_definitions(loc, formula, defs, env)
       ret = new_formula
+
     case EnableDefs(loc, definitions, subject):
       defs = [type_synth_term(d, env, None, []) for d in definitions]
       defs = [d.reduce(env) for d in defs]
       old_defs = get_reduce_only()
       set_reduce_only(defs + old_defs)
       ret = check_proof(subject, env)
       set_reduce_only(old_defs)
+
     case RewriteFact(loc, subject, equation_proofs):
       formula = check_proof(subject, env)
       eqns = [check_proof(proof, env) for proof in equation_proofs]
@@ -1085,13 +1094,19 @@ def check_proof_of(proof, formula, env):
           check_implies(loc, claim_red, remove_mark(formula_red))
           check_proof_of(reason, claim_red, env)
 
+    case EvaluateGoal(loc):
+      set_reduce_all(True)
+      red_formula = formula.reduce(env)
+      set_reduce_all(False)
+      if red_formula != Bool(loc, None, True):
+          error(loc, 'the goal did not evaluate to `true`, but instead:\n\t' + str(red_formula))
+      return red_formula
+
     case ApplyDefs(loc, definitions):
       defs = [type_synth_term(d, env, None, []) for d in definitions]
       defs = [d.reduce(env) for d in defs]
       new_formula = apply_definitions(loc, formula, defs, env)
       if new_formula != Bool(loc, None, True):
-          # error(loc, 'failed to prove:\n\t' + str(formula) + '\nby\n\t' + str(proof) \
-          #       + '\nremains to prove:\n\t' + str(new_formula))
           error(loc, 'remains to prove:\n\t' + str(new_formula))
 
     case Rewrite(loc, equation_proofs):

rec_desc_parser.py

@@ -856,6 +856,16 @@ def parse_proof_hi(token_list, i):
     meta = meta_from_tokens(token, token)
     return (PTransitive(meta, eq1, eq2), i)
 
+  elif token.type == 'EVALUATE':
+    i = i + 1
+    if token_list[i].type == 'IN':
+        i = i + 1
+        subject, i = parse_proof(token_list, i)
+        return (EvaluateFact(meta_from_tokens(token, token_list[i-1]),
+                             subject), i)
+    else:
+        return (EvaluateGoal(meta_from_tokens(token, token_list[i-1])), i)
+
   else:
     for kw in proof_keywords:
         if edit_distance(token.value, kw) <= 2:

test/should-error/eval-goal2.pf

@@ -0,0 +1,6 @@
+import Nat
+
+theorem T: 1 + 2 + 3 = 2 + 2 + 1
+proof
+  evaluate
+end

test/should-error/eval-goal2.pf.err

@@ -0,0 +1,2 @@
+./test/should-error/eval-goal2.pf:5.3-5.11: the goal did not evaluate to `true`, but instead:
+	false

test/should-pass/eval-fact.pf

@@ -0,0 +1,8 @@
+import Nat
+
+theorem T: all x:Nat. if x = 1 + 2 + 3 then x = 6
+proof
+  arbitrary x:Nat
+  assume prem: x = 1 + 2 + 3
+  evaluate in prem
+end

test/should-pass/eval-goal.pf

@@ -0,0 +1,6 @@
+import Nat
+
+theorem T: 1 + 2 + 3 = 2 + 2 + 2
+proof
+  evaluate
+end