Merge pull request 'feat: Draft tactic' (#153) from goal/tactic-draft into dev

Reviewed-on: #153

Pantograph/Frontend/Elab.lean

@@ -156,9 +156,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"

Pantograph/Tactic/Assign.lean

@@ -27,5 +27,38 @@ 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 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
+    | _ => 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

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),

Test/Proofs.lean

@@ -751,6 +751,7 @@ 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 suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("identity", test_identity),

Test/Tactic.lean

@@ -1,3 +1,4 @@
+import Test.Tactic.Assign
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse

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