From e282d9f7815e8ea616da07185ae55062527831b4 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 25 Jun 2024 11:03:08 -0400
Subject: [PATCH] test: Evaluation tactic

---
 Pantograph/Goal.lean            |  2 +-
 Pantograph/Serial.lean          |  2 +-
 Pantograph/Tactic/Prograde.lean |  2 +-
 Test/Common.lean                | 11 +++++++++
 Test/Main.lean                  |  1 +
 Test/Tactic.lean                |  1 +
 Test/Tactic/Prograde.lean       | 42 +++++++++++++++++++++++++++++++++
 7 files changed, 58 insertions(+), 3 deletions(-)
 create mode 100644 Test/Tactic/Prograde.lean

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index ebe29fb..db73a48 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -548,6 +548,6 @@ protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Na
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.tacticEval binderName expr)
+  state.execute goalId (tacticM := Tactic.evaluate binderName expr)
 
 end Pantograph
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 159b78e..5f08186 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -202,7 +202,7 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
   }
 
 /-- Adapted from ppGoal -/
-def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
       : MetaM Protocol.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean
index f37a1e5..81dd28c 100644
--- a/Pantograph/Tactic/Prograde.lean
+++ b/Pantograph/Tactic/Prograde.lean
@@ -5,7 +5,7 @@ open Lean
 
 namespace Pantograph.Tactic
 
-def tacticEval (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
+def evaluate (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)
diff --git a/Test/Common.lean b/Test/Common.lean
index c656309..e4e1d4c 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -8,6 +8,17 @@ open Lean
 
 namespace Pantograph
 
+deriving instance Repr for Expr
+-- Use strict equality check for expressions
+--instance : BEq Expr := ⟨Expr.equal⟩
+instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) :=
+  if h : Expr.equal x y then
+    .isTrue h
+  else
+    .isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'"
+
+def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
+
 -- Auxiliary functions
 namespace Protocol
 def Goal.devolatilizeVars (goal: Goal): Goal :=
diff --git a/Test/Main.lean b/Test/Main.lean
index 31042c5..89c757a 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -52,6 +52,7 @@ def main (args: List String) := do
     ("Tactic/Congruence", Tactic.Congruence.suite env_default),
     ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
     ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
+    ("Tactic/Prograde", Tactic.Prograde.suite env_default),
   ]
   let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
   LSpec.lspecIO (← runTestGroup name_filter tests)
diff --git a/Test/Tactic.lean b/Test/Tactic.lean
index 5863ec0..3cb0e40 100644
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@@ -1,3 +1,4 @@
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse
+import Test.Tactic.Prograde
diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean
new file mode 100644
index 0000000..863aca5
--- /dev/null
+++ b/Test/Tactic/Prograde.lean
@@ -0,0 +1,42 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.Prograde
+
+def test_eval (env: Environment): IO LSpec.TestSeq :=
+  let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.forallTelescope expr $ λ _ body => do
+      let e ← match Parser.runParserCategory
+        (env := ← MonadEnv.getEnv)
+        (catName := `term)
+        (input := "Or.inl h")
+        (fileName := filename) with
+        | .ok syn => pure syn
+        | .error error => throwError "Failed to parse: {error}"
+      let mut tests := LSpec.TestSeq.done
+      -- Apply the tactic
+      let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let target: Expr := mkAnd
+        (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
+        (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
+      let test := LSpec.test "goals before" ((← goal.mvarId!.getType) == target)
+      tests := tests ++ test
+      let tactic := Tactic.evaluate `h2 e
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar tactic goal.mvarId!
+        pure $ LSpec.test "goals after" ((← newGoals.head!.getType) == target)
+      tests := tests ++ test
+      return tests
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("eval", test_eval env),
+  ]
+
+end Pantograph.Test.Tactic.Prograde