From cb46b47a60cbe06a3b26efd261f9a07a6fe76326 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 8 Jan 2025 22:23:30 -0800
Subject: [PATCH] test: Draft tactic test

---
 Pantograph/Tactic/Assign.lean |  3 ++-
 Test/Main.lean                |  1 +
 Test/Proofs.lean              | 28 ++++++++++++++++++++++++++++
 Test/Tactic.lean              |  1 +
 4 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean
index 1607e83..d1dbf0c 100644
--- a/Pantograph/Tactic/Assign.lean
+++ b/Pantograph/Tactic/Assign.lean
@@ -30,6 +30,7 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
 def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
   Meta.transform src λ
     | .app (.app (.const ``sorryAx ..) type) .. => do
+      -- FIXME: Handle cases of coupled goals
       let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
       modify (mvar.mvarId! :: .)
       pure $ .done mvar
@@ -52,7 +53,7 @@ def evalDraft : Elab.Tactic.Tactic := fun stx ↦ Elab.Tactic.withMainContext do
   let goal ← Elab.Tactic.getMainGoal
   let (expr, holeGoals) ← Elab.Tactic.elabTermWithHoles stx
     (expectedType? := .some target)
-    (tagSuffix := .anonymous )
+    (tagSuffix := .anonymous)
     (allowNaturalHoles := true)
   let draftGoals ← draft goal expr
   Elab.Tactic.replaceMainGoal $ holeGoals ++ draftGoals
diff --git a/Test/Main.lean b/Test/Main.lean
index 6bf410e..18dc9e3 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -53,6 +53,7 @@ def main (args: List String) := do
     ("Proofs", Proofs.suite env_default),
     ("Delate", Delate.suite env_default),
     ("Serial", Serial.suite env_default),
+    ("Tactic/Assign", Tactic.Assign.suite env_default),
     ("Tactic/Congruence", Tactic.Congruence.suite env_default),
     ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
     ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index a6b5487..b1b770b 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -751,6 +751,33 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
   --let message := s!"<Pantograph>:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
   --checkEq s!"{tactic} fails" messages #[message]
 
+
+def test_draft_tactic : TestM Unit := do
+  let state? ← startProof (.expr "∀ (p : Prop), p")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro p"
+  let state1 ← match ← state0.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  let payload := "by\nhave q : Or p p := sorry\nsorry"
+  let state2 ← match ← state1.tryAssign (state1.goals.get! 0) payload with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  checkEq payload ((← state2.serializeGoals).map (·.devolatilize))  #[
+    buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r"
+  ]
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("identity", test_identity),
@@ -765,6 +792,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Nat.zero_add alt", test_nat_zero_add_alt),
     ("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals),
     ("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder),
+    ("draft", test_draft_tactic),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 
diff --git a/Test/Tactic.lean b/Test/Tactic.lean
index 3cb0e40..6b3e8fd 100644
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@@ -1,3 +1,4 @@
+import Test.Tactic.Assign
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse