Pantograph/Goal.lean

@@ -156,7 +156,6 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId)
 
 protected def GoalState.step (state: GoalState) (mvarId: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
   : Elab.TermElabM GoalState := do
-  state.restoreElabM
   unless (← getMCtx).decls.contains mvarId do
     throwError s!"MVarId is not in context: {mvarId.name}"
   mvarId.checkNotAssigned `GoalState.step
@@ -197,6 +196,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: El
 /-- Execute a string tactic on given state -/
 protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
     Elab.TermElabM TacticResult := do
+  state.restoreElabM
   let tactic ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := if state.isConv then `conv else `tactic)
@@ -223,45 +223,14 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
 protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.tryLet
   let type ← match Parser.runParserCategory
-    (env := state.env)
+    (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := type)
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  let binderName := binderName.toName
+  state.tryTacticM goalId $ Tactic.evalLet binderName.toName type
-  try
-    -- Implemented similarly to the intro tactic
-    let nextGoals: List MVarId ← goal.withContext do
-      let type ← Elab.Term.elabType (stx := type)
-      let lctx ← MonadLCtx.getLCtx
-
-      -- The branch goal inherits the same context, but with a different type
-      let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
-
-      let upstreamType := .letE binderName type mvarBranch (← goal.getType) false
-      let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
-        upstreamType (kind := MetavarKind.synthetic) (userName := (← goal.getTag))
-
-      goal.assign mvarUpstream
-
-      pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
-    return .success {
-      root := state.root,
-      savedState := {
-        term := ← MonadBacktrack.saveState,
-        tactic := { goals := nextGoals }
-      },
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
 
 /-- Enter conv tactic mode -/
 protected def GoalState.conv (state: GoalState) (goalId: Nat):

Pantograph/Library.lean

@@ -168,7 +168,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
     | .error error => return .parseError error
   runTermElabM do
     state.restoreElabM
-    state.tryTacticM goalId (Tactic.«have» binderName.toName type)
+    state.tryTacticM goalId $ Tactic.evalHave binderName.toName type
 @[export pantograph_goal_evaluate_m]
 protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do
   let expr ← match (← Compile.parseTermM expr) with

Pantograph/Tactic/Prograde.lean

@@ -19,29 +19,65 @@ def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
     pure [mvarUpstream.mvarId!]
   Elab.Tactic.setGoals nextGoals
 
-def «have» (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
+structure BranchResult where
+  fvarId?: Option FVarId := .none
+  main: MVarId
+  branch: MVarId
+
+def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.have
+  let lctx ← MonadLCtx.getLCtx
+  -- The branch goal inherits the same context, but with a different type
+  let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
+
+  -- Create the context for the `upstream` goal
+  let fvarId ← mkFreshFVarId
+  let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
+  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)
+          (← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
+        --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
+        mvarId.assign mvarUpstream
+        pure mvarUpstream
+
+  return {
+    fvarId? := .some fvarId,
+    main := mvarUpstream.mvarId!,
+    branch := mvarBranch.mvarId!,
+  }
+
+def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
   let nextGoals: List MVarId ← goal.withContext do
     let type ← Elab.Term.elabType (stx := type)
-    let lctx ← MonadLCtx.getLCtx
+    let result ← «have» goal binderName type
-
+    pure [result.branch, result.main]
-    -- The branch goal inherits the same context, but with a different type
-    let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
-
-    -- Create the context for the `upstream` goal
-    let fvarId ← mkFreshFVarId
-    let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
-    let fvar   := mkFVar fvarId
-    let mvarUpstream ←
-      withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
-        Meta.withNewLocalInstances #[fvar] 0 do
-          let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
-            (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
-          --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
-          goal.assign mvarUpstream
-          pure mvarUpstream
-
-    pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
   Elab.Tactic.setGoals nextGoals
 
+def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.let
+  let lctx ← MonadLCtx.getLCtx
+
+  -- The branch goal inherits the same context, but with a different type
+  let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
+
+  assert! ¬ type.hasLooseBVars
+  let upstreamType := .letE binderName type mvarBranch (← mvarId.getType) false
+  let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+    upstreamType (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
+  mvarId.assign mvarUpstream
+
+  return {
+    main := mvarUpstream.mvarId!,
+    branch := mvarBranch.mvarId!,
+  }
+
+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]
+
 end Pantograph.Tactic