From 5ce6123de74af4823026771ce62cadd075a32771 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 8 Jan 2025 19:56:14 -0800
Subject: [PATCH 1/5] feat: Draft tactic

---
 Pantograph/Tactic/Assign.lean | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean
index 8a5b998..1607e83 100644
--- a/Pantograph/Tactic/Assign.lean
+++ b/Pantograph/Tactic/Assign.lean
@@ -27,5 +27,35 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
   goal.assign expr
   Elab.Tactic.replaceMainGoal nextGoals
 
+def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
+  Meta.transform src λ
+    | .app (.app (.const ``sorryAx ..) type) .. => do
+      let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
+      modify (mvar.mvarId! :: .)
+      pure $ .done mvar
+    | _ => pure .continue
+
+-- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals.
+def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do
+  goal.checkNotAssigned `Pantograph.Tactic.draft
+  let exprType ← Meta.inferType expr
+  let goalType ← goal.getType
+  unless ← Meta.isDefEq goalType exprType do
+    throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
+
+  let (expr', holes) ← sorryToHole expr |>.run []
+  goal.assign expr'
+  return holes.reverse
+
+def evalDraft : Elab.Tactic.Tactic := fun stx ↦ Elab.Tactic.withMainContext do
+  let target ← Elab.Tactic.getMainTarget
+  let goal ← Elab.Tactic.getMainGoal
+  let (expr, holeGoals) ← Elab.Tactic.elabTermWithHoles stx
+    (expectedType? := .some target)
+    (tagSuffix := .anonymous )
+    (allowNaturalHoles := true)
+  let draftGoals ← draft goal expr
+  Elab.Tactic.replaceMainGoal $ holeGoals ++ draftGoals
+
 
 end Pantograph.Tactic
-- 
2.44.1


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 2/5] 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
-- 
2.44.1


From 072d351f0406616592f0ef727a8120164b926ffc Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 8 Jan 2025 22:47:08 -0800
Subject: [PATCH 3/5] fix: Delete extraneous test

---
 Test/Proofs.lean | 27 ---------------------------
 1 file changed, 27 deletions(-)

diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index b1b770b..a26ec50 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -752,32 +752,6 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
   --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),
@@ -792,7 +766,6 @@ 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))
 
-- 
2.44.1


From aa066b8634a65a3036745c331022c576722acbab Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 8 Jan 2025 22:53:10 -0800
Subject: [PATCH 4/5] fix: Add test

---
 Test/Tactic/Assign.lean | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 Test/Tactic/Assign.lean

diff --git a/Test/Tactic/Assign.lean b/Test/Tactic/Assign.lean
new file mode 100644
index 0000000..e527bbb
--- /dev/null
+++ b/Test/Tactic/Assign.lean
@@ -0,0 +1,33 @@
+import Lean.Meta
+import Lean.Elab
+import LSpec
+import Test.Common
+
+open Lean
+
+namespace Pantograph.Test.Tactic.Assign
+
+def test_draft : TestT Elab.TermElabM Unit := do
+  let expr := "forall (p : Prop), (p ∨ p) ∨ p"
+  let skeleton := "by\nhave a : p ∨ p := sorry\nsorry"
+  let expr ← parseSentence expr
+  Meta.forallTelescope expr $ λ _ body => do
+    let skeleton' ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := skeleton)
+      (fileName := ← getFileName) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.evalDraft skeleton'
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = ["p ∨ p", "(p ∨ p) ∨ p"])
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("draft", test_draft),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Assign
-- 
2.44.1


From ebde7c9eed50d4cc29b235150cf5e4841f6dbc85 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 13 Jan 2025 10:20:36 -0800
Subject: [PATCH 5/5] feat: Prohibit coupling in drafting

---
 Pantograph/Frontend/Elab.lean | 5 +++++
 Pantograph/Tactic/Assign.lean | 4 +++-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 3da5fca..4ccb609 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -149,9 +149,14 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState
     match i.info with
     | .ofTermInfo termInfo  => do
       let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
+      if (← mvarId.getType).hasSorry then
+        throwError s!"Coupling is not allowed in drafting"
       return [(mvarId, stxByteRange termInfo.stx)]
     | .ofTacticInfo tacticInfo => do
       let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+      for mvarId in mvarIds do
+        if (← mvarId.getType).hasSorry then
+          throwError s!"Coupling is not allowed in drafting"
       let range := stxByteRange tacticInfo.stx
       return mvarIds.map (·, range)
     | _ => panic! "Invalid info"
diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean
index d1dbf0c..c87dd46 100644
--- a/Pantograph/Tactic/Assign.lean
+++ b/Pantograph/Tactic/Assign.lean
@@ -30,7 +30,9 @@ 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 type ← instantiateMVars type
+      if type.hasSorry then
+        throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
       let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
       modify (mvar.mvarId! :: .)
       pure $ .done mvar
-- 
2.44.1