Pantograph/Tactic/Prograde.lean

@@ -5,22 +5,25 @@ open Lean
 
 namespace Pantograph.Tactic
 
+private def mkUpstreamMVar (goal: MVarId) : MetaM Expr := do
+  Meta.mkFreshExprSyntheticOpaqueMVar (← goal.getType) (tag := ← goal.getTag)
+
+
 /-- Introduces a fvar to the current mvar -/
 def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
   mvarId.checkNotAssigned `Pantograph.Tactic.define
   let type ← Meta.inferType expr
 
   Meta.withLetDecl binderName type expr λ fvar => do
-    let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+    let mvarUpstream ← mkUpstreamMVar mvarId
-      (← mvarId.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
+    mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
-    mvarId.assign mvarUpstream
     pure (fvar.fvarId!, mvarUpstream.mvarId!)
 
 def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
   let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
   let (_, mvarId) ← define goal binderName expr
-  Elab.Tactic.setGoals [mvarId]
+  Elab.Tactic.replaceMainGoal [mvarId]
 
 structure BranchResult where
   fvarId?: Option FVarId := .none
@@ -39,10 +42,9 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
   let mvarUpstream ←
     withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
       Meta.withNewLocalInstances #[.fvar fvarId] 0 do
-        let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+        let mvarUpstream ← mkUpstreamMVar mvarId
-          (← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
         --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
-        mvarId.assign mvarUpstream
+        mvarId.assign $ ← Meta.mkLambdaFVars #[.fvar fvarId] mvarUpstream
         pure mvarUpstream
 
   return {
@@ -57,7 +59,7 @@ def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
     let type ← Elab.Term.elabType (stx := type)
     let result ← «have» goal binderName type
     pure [result.branch, result.main]
-  Elab.Tactic.setGoals nextGoals
+  Elab.Tactic.replaceMainGoal nextGoals
 
 def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
   mvarId.checkNotAssigned `Pantograph.Tactic.let
@@ -68,9 +70,8 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult
 
   assert! ¬ type.hasLooseBVars
   let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
-    let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+    let mvarUpstream ← mkUpstreamMVar mvarId
-      (type := ← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
+    mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
-    mvarId.assign $ .letE binderName type fvar mvarUpstream (nonDep := false)
     pure mvarUpstream
 
   return {
@@ -82,6 +83,6 @@ def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
   let type ← goal.withContext $ Elab.Term.elabType (stx := type)
   let result ← «let» goal binderName type
-  Elab.Tactic.setGoals [result.branch, result.main]
+  Elab.Tactic.replaceMainGoal [result.branch, result.main]
 
 end Pantograph.Tactic

Test/Common.lean

@@ -94,15 +94,22 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 
+def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do
+  let .ok stx := Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := s)
+    (fileName := filename) | panic! s!"Failed to parse {s}"
+  return stx
 def parseSentence (s: String): Elab.TermElabM Expr := do
-  let recursor ← match Parser.runParserCategory
+  let stx ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := s)
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
-  Elab.Term.elabTerm (stx := recursor) .none
+  Elab.Term.elabTerm (stx := stx) .none
 
 def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }

Test/Tactic/Prograde.lean

@@ -7,7 +7,7 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.Prograde
 
-def test_eval : TestT Elab.TermElabM Unit := do
+def test_define : TestT Elab.TermElabM Unit := do
   let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
   let expr ← parseSentence expr
   Meta.forallTelescope expr $ λ _ body => do
@@ -48,9 +48,10 @@ def test_eval : TestT Elab.TermElabM Unit := do
       ],
       target,
     })
-    addTest $ LSpec.test "assign" ((← getExprMVarAssignment? goal.mvarId!) == .some (.mvar newGoal))
+    let .some e ← getExprMVarAssignment? goal.mvarId! | panic! "Tactic must assign"
+    addTest $ LSpec.test "assign" e.isLet
 
-def test_proof_eval : TestT Elab.TermElabM Unit := do
+def test_define_proof : TestT Elab.TermElabM Unit := do
   let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
@@ -103,7 +104,38 @@ def test_proof_eval : TestT Elab.TermElabM Unit := do
 
   addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
 
-def test_proof_have : TestT Elab.TermElabM Unit := do
+def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
+  intro p x
+  apply x.fst
+  exact 5
+
+def test_define_root_expr : TestT Elab.TermElabM Unit := do
+  --let rootExpr ← parseSentence "Nat"
+  --let state0 ← GoalState.create rootExpr
+  --let .success state1 ← state0.tryTactic (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
+  --let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
+  --addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
+  let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "intro p x"
+  let .success state1 ← state0.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let binderName := `binder
+  let value := "x.fst"
+  let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
+  let tacticM := Tactic.evalDefine binderName expr
+  let .success state2 ← state1.tryTacticM (goalId := 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
+  let tactic := s!"apply {binderName}"
+  let .success state3 ← state2.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let tactic := s!"exact 5"
+  let .success state4 ← state3.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
+  addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")
+
+--set_option pp.all true
+--#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
+--def test_define_root_expr : TestT Elab.TermElabM Unit := do
+
+def test_have_proof : TestT Elab.TermElabM Unit := do
   let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
@@ -160,7 +192,8 @@ def test_proof_have : TestT Elab.TermElabM Unit := do
   addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
     #[])
 
-  addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
+  let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
+  addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p q h y => Or.inl y")
 
 def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
   let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
@@ -256,9 +289,10 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("eval", test_eval),
+    ("define", test_define),
-    ("Proof eval", test_proof_eval),
+    ("define proof", test_define_proof),
-    ("Proof have", test_proof_have),
+    ("define root expr", test_define_root_expr),
+    ("have proof", test_have_proof),
     ("let via assign", test_let false),
     ("let via tryLet", test_let true),
   ] |>.map (λ (name, t) => (name, runTestTermElabM env t))