From 25a7025c254102da74ad89343801719769bc62b4 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 23 Jun 2024 15:01:51 -0700
Subject: [PATCH] feat: Evaluation tactic

---
 Pantograph/Goal.lean            | 12 ++++++++++++
 Pantograph/Tactic.lean          |  2 +-
 Pantograph/Tactic/Prograde.lean | 22 ++++++++++++++++++++++
 3 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 Pantograph/Tactic/Prograde.lean

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 46888e7..ebe29fb 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -302,6 +302,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
           Meta.withNewLocalInstances #[fvar] 0 do
             let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
               (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
+            -- FIXME: May be redundant?
             let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
             goal.assign expr
             pure mvarUpstream
@@ -537,5 +538,16 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: Strin
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.execute goalId (tacticM := Tactic.noConfuse recursor)
+protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) :
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let expr ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := expr)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.execute goalId (tacticM := Tactic.tacticEval binderName expr)
 
 end Pantograph
diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean
index 225ad31..094d1f8 100644
--- a/Pantograph/Tactic.lean
+++ b/Pantograph/Tactic.lean
@@ -1,4 +1,4 @@
-
 import Pantograph.Tactic.Congruence
 import Pantograph.Tactic.MotivatedApply
 import Pantograph.Tactic.NoConfuse
+import Pantograph.Tactic.Prograde
diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean
new file mode 100644
index 0000000..f37a1e5
--- /dev/null
+++ b/Pantograph/Tactic/Prograde.lean
@@ -0,0 +1,22 @@
+/- Prograde (forward) reasoning tactics -/
+
+import Lean
+open Lean
+
+namespace Pantograph.Tactic
+
+def tacticEval (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let nextGoals ← goal.withContext do
+    let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
+    let type ← Meta.inferType expr
+
+    let mvarUpstream ← Meta.withLetDecl binderName type expr λ _ => do
+      let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+        (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
+      goal.assign mvarUpstream
+      pure mvarUpstream
+    pure [mvarUpstream.mvarId!]
+  Elab.Tactic.setGoals nextGoals
+
+end Pantograph.Tactic