Pantograph/Goal.lean

@@ -64,11 +64,7 @@ structure GoalState where
   -- The root goal which is the search target
   root: MVarId
 
-  /--
+  -- Parent goals assigned to produce this state
-  Parent goals which became assigned or fragmented to produce this state.
-  Note that due to the existence of tactic fragments, parent goals do not
-  necessarily have an expression assignment.
-  -/
   parentMVars : List MVarId := []
 
   -- Any goal associated with a fragment has a partial tactic which has not
@@ -206,11 +202,8 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   return expr
 @[export pantograph_goal_state_parent_exprs]
-protected def GoalState.parentExprs (state : GoalState) : List (Except Fragment Expr) :=
+protected def GoalState.parentExprs (state : GoalState) : List Expr :=
-  state.parentMVars.map λ goal => match state.getMVarEAssignment goal with
+  state.parentMVars.map λ goal => state.getMVarEAssignment goal |>.get!
-    | .some e => .ok e
-    -- A parent goal which is not assigned must have a fragment
-    | .none => .error state.fragments[goal]!
 @[always_inline]
 protected def GoalState.hasUniqueParent (state : GoalState) : Bool :=
   state.parentMVars.length == 1
@@ -514,8 +507,7 @@ protected def GoalState.tryTacticM
     (state: GoalState) (site : Site)
     (tacticM: Elab.Tactic.TacticM Unit)
     (guardMVarErrors : Bool := false)
-    : Elab.TermElabM TacticResult := do
+    : Elab.TermElabM TacticResult :=
-  state.restoreElabM
   withCapturingError do
     state.step site tacticM guardMVarErrors
 
@@ -575,7 +567,6 @@ protected def GoalState.convEnter (state : GoalState) (site : Site) :
   let .some goal := state.actingGoal? site | throwNoGoals
   if let .some (.conv ..) := state.fragments[goal]? then
     return .invalidAction "Already in conv state"
-  state.restoreElabM
   withCapturingError do
     let (fragments, state') ← state.step' site Fragment.enterConv
     return {
@@ -591,7 +582,6 @@ protected def GoalState.fragmentExit (state : GoalState) (site : Site):
   let .some goal := state.actingGoal? site | throwNoGoals
   let .some fragment := state.fragments[goal]? |
     return .invalidAction "Goal does not have a fragment"
-  state.restoreElabM
   withCapturingError do
     let (fragments, state') ← state.step' goal (fragment.exit goal state.fragments)
     return {
@@ -609,7 +599,6 @@ protected def GoalState.calcEnter (state : GoalState) (site : Site)
   let .some goal := state.actingGoal? site | throwNoGoals
   if let .some _ := state.fragments[goal]? then
     return .invalidAction "Goal already has a fragment"
-  state.restoreElabM
   withCapturingError do
     let fragment := Fragment.enterCalc
     let fragments := state.fragments.insert goal fragment

Pantograph/Library.lean

@@ -132,9 +132,8 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bo
       pure .none
   let parentExprs? ← if parentExprs then
       .some <$> state.parentMVars.mapM λ parent => parent.withContext do
-        let val? := state.getMVarEAssignment parent
+        let val := state.getMVarEAssignment parent |>.get!
-        val?.mapM λ val => do
+        serializeExpression options (← instantiateAll val)
-          serializeExpression options (← instantiateAll val)
     else
       pure .none
   let goals ← if goals then

Pantograph/Protocol.lean

@@ -325,7 +325,7 @@ structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
-  parentExprs?: Option (List (Option Expression)) := .none
+  parentExprs?: Option (List Expression) := .none
   goals: Array Goal := #[]
   extraMVars: Array Expression := #[]
 

Repl.lean

@@ -147,15 +147,10 @@ def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult :=
   match nextGoalState? with
   | .error error => Protocol.throw error
   | .ok (.success nextGoalState messages) => do
-    let env ← getEnv
     let nextStateId ← newGoalState nextGoalState
     let parentExprs := nextGoalState.parentExprs
-    let hasSorry := parentExprs.any λ
+    let hasSorry := parentExprs.any (·.hasSorry)
-      | .ok e => e.hasSorry
+    let hasUnsafe := parentExprs.any ((← getEnv).hasUnsafe ·)
-      | .error _ => false
-    let hasUnsafe := parentExprs.any λ
-      | .ok e => env.hasUnsafe e
-      | .error _ => false
     let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run'
     return {
       nextStateId? := .some nextStateId,

Test/Integration.lean

@@ -91,7 +91,7 @@ def test_tactic : Test := do
   step "goal.print" ({ stateId := 1, parentExprs? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
    ({
      root? := .some { pp? := "fun x => ?m.11"},
-     parentExprs? := .some [.some { pp? := .some "fun x => ?m.11" }],
+     parentExprs? := .some [{ pp? := .some "fun x => ?m.11" }],
    }: Protocol.GoalPrintResult)
   step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
    ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult)
@@ -164,48 +164,6 @@ def test_automatic_mode (automatic: Bool): Test := do
   step "goal.tactic" ({ stateId := 2, tactic? := .some "apply Or.inr" }: Protocol.GoalTactic)
    ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult)
 
-def test_conv_calc : Test := do
-  step "options.set" ({automaticMode? := .some false}: Protocol.OptionsSet)
-   ({}: Protocol.OptionsSetResult)
-  step "goal.start" ({ expr := "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b"} : Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.163" }: Protocol.GoalStartResult)
-  let vars := #[
-    { name := "_uniq.164", userName := "a", type? := .some { pp? := .some "Nat" }},
-    { name := "_uniq.167", userName := "b", type? := .some { pp? := .some "Nat" }},
-    { name := "_uniq.170", userName := "h", type? := .some { pp? := .some "b = 2" }},
-  ]
-  let goal : Protocol.Goal := {
-    vars,
-    name := "_uniq.171",
-    target := { pp? := "1 + a + 1 = a + b" },
-  }
-  step "goal.tactic" ({ stateId := 0, tactic? := .some "intro a b h" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 1, goals? := #[goal], }: Protocol.GoalTacticResult)
-  step "goal.tactic" ({ stateId := 1, mode? := .some "calc" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 2, goals? := #[{ goal with fragment := .calc }], }: Protocol.GoalTacticResult)
-  let goalCalc : Protocol.Goal := {
-    vars,
-    name := "_uniq.363",
-    userName? := .some "calc",
-    target := { pp? := "1 + a + 1 = a + 1 + 1" },
-  }
-  let goalMain : Protocol.Goal := {
-    vars,
-    name := "_uniq.382",
-    fragment := .calc,
-    target := { pp? := "a + 1 + 1 = a + b" },
-  }
-  step "goal.tactic" ({ stateId := 2, tactic? := .some "1 + a + 1 = a + 1 + 1" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 3, goals? := #[goalCalc, goalMain], }: Protocol.GoalTacticResult)
-  let goalConv : Protocol.Goal := {
-    goalCalc with
-    fragment := .conv,
-    userName? := .none,
-    name := "_uniq.450",
-  }
-  step "goal.tactic" ({ stateId := 3, mode? := .some "conv" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 4, goals? := #[goalConv], }: Protocol.GoalTacticResult)
-
 def test_env_add_inspect : Test := do
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
@@ -385,7 +343,6 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("Tactic Timeout", test_tactic_timeout),
     ("Manual Mode", test_automatic_mode false),
     ("Automatic Mode", test_automatic_mode true),
-    ("Conv-Calc", test_conv_calc),
     ("env.add env.inspect", test_env_add_inspect),
     ("frontend.process invocation", test_frontend_process),
     ("frontend.process sorry", test_frontend_process_sorry),

Test/Serial.lean

@@ -84,7 +84,7 @@ def test_pickling_env_extensions : TestM Unit := do
     let goal := state.goals[0]!
     let type ← goal.withContext do
       let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable!
-      instantiateMVars type
+      pure type
     let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | unreachable!
     let parentExpr := state1.parentExpr!
     checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma)