Merge branch 'dev' into serial/delta

Pantograph/Delate.lean

@@ -454,7 +454,6 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
     dependentMVars?,
   }
 
-
 /-- Adapted from ppGoal -/
 def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
       : MetaM Protocol.Goal := do
@@ -520,7 +519,6 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
     return {
       name := goal.name.toString,
       userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
-      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
       target := (← serializeExpression options (← instantiate mvarDecl.type)),
       vars := vars.reverse.toArray
     }
@@ -530,17 +528,20 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
 
 protected def GoalState.serializeGoals
       (state: GoalState)
-      (parent: Option GoalState := .none)
       (options: @&Protocol.Options := {}):
     MetaM (Array Protocol.Goal):= do
   state.restoreMetaM
   let goals := state.goals.toArray
-  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
   goals.mapM fun goal => do
+    let fragment := match state.fragments[goal]? with
+      | .none => .tactic
+      | .some $ .calc .. => .calc
+      | .some $ .conv .. => .conv
+      | .some $ .convSentinel .. => .conv
     match state.mctx.findDecl? goal with
     | .some mvarDecl =>
-      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
+      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := .none)
-      pure serializedGoal
+      pure { serializedGoal with fragment }
     | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 
 /-- Print the metavariables in a readable format -/
@@ -606,7 +607,9 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
     userNameToString : Name → String
       | .anonymous => ""
       | other => s!"[{other}]"
-    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
+    parentHasMVar (mvarId: MVarId): Bool := match parent? with
+      | .some state => state.mctx.decls.contains mvarId
+      | .none => true
 
 initialize
   registerTraceClass `Pantograph.Delate

Pantograph/Goal.lean

@@ -10,22 +10,69 @@ import Lean
 namespace Pantograph
 open Lean
 
+/-- The acting area of a tactic -/
+inductive Site where
+  -- Dormant all other goals
+  | focus (goal : MVarId)
+  -- Move the goal to the first in the list
+  | prefer (goal : MVarId)
+  -- Execute as-is, no goals go dormant
+  | unfocus
+  deriving BEq, Inhabited
+
+instance : Coe MVarId Site where
+  coe := .focus
+instance : ToString Site where
+  toString
+    | .focus { name } => s!"[{name}]"
+    | .prefer { name } => s!"[{name},...]"
+    | .unfocus => "[*]"
+
+/-- Executes a `TacticM` on a site and return affected goals -/
+protected def Site.runTacticM (site : Site)
+  { m } [Monad m] [MonadLiftT Elab.Tactic.TacticM m] [MonadControlT Elab.Tactic.TacticM m] [MonadMCtx m] [MonadError m]
+  (f : m α) : m (α × List MVarId) :=
+  match site with
+  | .focus goal => do
+    Elab.Tactic.setGoals [goal]
+    let a ← f
+    return (a, [goal])
+  | .prefer goal => do
+    let before ← Elab.Tactic.getUnsolvedGoals
+    let otherGoals := before.filter (· != goal)
+    Elab.Tactic.setGoals (goal :: otherGoals)
+    let a ← f
+    let after ← Elab.Tactic.getUnsolvedGoals
+    let parents := before.filter (¬ after.contains ·)
+    Elab.Tactic.pruneSolvedGoals
+    return (a, parents)
+  | .unfocus => do
+    let before ← Elab.Tactic.getUnsolvedGoals
+    let a ← f
+    let after ← Elab.Tactic.getUnsolvedGoals
+    let parents := before.filter (¬ after.contains ·)
+    Elab.Tactic.pruneSolvedGoals
+    return (a, parents)
+
 /--
-Represents an interconnected set of metavariables, or a state in proof search
+Kernel view of the state of a proof
  -/
 structure GoalState where
+  -- Captured `TacticM` state
   savedState : Elab.Tactic.SavedState
 
-  -- The root hole which is the search target
+  -- The root goal which is the search target
   root: MVarId
 
-  -- Parent state metavariable source
+  -- Parent goals assigned to produce this state
-  parentMVar?: Option MVarId := .none
+  parentMVars : List MVarId := []
 
   -- Any goal associated with a fragment has a partial tactic which has not
   -- finished executing.
   fragments : FragmentMap := .empty
 
+def throwNoGoals { m α } [Monad m] [MonadError m] : m α := throwError "no goals to be solved"
+
 @[export pantograph_goal_state_create_m]
 protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
   -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
@@ -39,7 +86,6 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
   return {
     root := root.mvarId!,
     savedState,
-    parentMVar? := .none,
   }
 @[export pantograph_goal_state_create_from_mvars_m]
 protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do
@@ -48,10 +94,19 @@ protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): Met
   return {
     root,
     savedState,
-    parentMVar? := .none,
   }
+@[always_inline]
 protected def GoalState.goals (state: GoalState): List MVarId :=
   state.savedState.tactic.goals
+@[always_inline]
+protected def GoalState.mainGoal? (state : GoalState) : Option MVarId :=
+  state.goals.head?
+@[always_inline]
+protected def GoalState.actingGoal? (state : GoalState) (site : Site) : Option MVarId := do
+  match site with
+  | .focus goal | .prefer goal => return goal
+  | .unfocus => state.mainGoal?
+
 @[export pantograph_goal_state_goals]
 protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
 protected def GoalState.mctx (state: GoalState): MetavarContext :=
@@ -63,8 +118,10 @@ protected def GoalState.env (state: GoalState): Environment :=
 protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
   let mvarDecl ← state.mctx.findDecl? mvarId
   return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
+@[always_inline]
 protected def GoalState.metaState (state: GoalState): Meta.State :=
   state.savedState.term.meta.meta
+@[always_inline]
 protected def GoalState.coreState (state: GoalState): Core.SavedState :=
   state.savedState.term.meta.core
 
@@ -72,18 +129,18 @@ protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: Met
   mvarId.withContext m |>.run' (← read) state.metaState
 protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α :=
   Meta.mapMetaM <| state.withContext' mvarId
+/-- Uses context of the first parent -/
 protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext' state.parentMVar?.get!
+  Meta.mapMetaM <| state.withContext' state.parentMVars[0]!
 protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
   Meta.mapMetaM <| state.withContext' state.root
 
-private def GoalState.mvars (state: GoalState): SSet MVarId :=
+private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit :=
-  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
--- Restore the name generator and macro scopes of the core state
-protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := do
-  let savedCore := state.coreState
   modifyGetThe Core.State (fun st => ((),
-    { st with nextMacroScope := savedCore.nextMacroScope, ngen := savedCore.ngen }))
+    { st with nextMacroScope := state.nextMacroScope, ngen := state.ngen }))
+-- Restore the name generator and macro scopes of the core state
+protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
+  restoreCoreMExtra state.coreState
 protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := do
   state.restoreCoreMExtra
   state.savedState.term.meta.restore
@@ -94,40 +151,13 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
   state.restoreElabM
   Elab.Tactic.setGoals [goal]
 
-@[export pantograph_goal_state_focus]
-protected def GoalState.focus (state : GoalState) (goal : MVarId): Option GoalState := do
-  return {
-    state with
-    savedState := {
-      state.savedState with
-      tactic := { goals := [goal] },
-    },
-  }
-
-/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
-@[export pantograph_goal_state_immediate_resume]
-protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
-  -- Prune parents solved goals
-  let mctx := state.mctx
-  let parentGoals := parent.goals.filter λ goal =>
-    let isDuplicate := state.goals.contains goal
-    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
-    (¬ isDuplicate) && (¬ isSolved)
-  {
-    state with
-    savedState := {
-      state.savedState with
-      tactic := { goals := state.goals ++ parentGoals },
-    },
-  }
-
 /--
 Brings into scope a list of goals. User must ensure `goals` are distinct.
 -/
 @[export pantograph_goal_state_resume]
 protected def GoalState.resume (state : GoalState) (goals : List MVarId) : Except String GoalState := do
-  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
+  if ¬ (goals.all (state.mctx.decls.contains ·)) then
-    let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
+    let invalid_goals := goals.filter (λ goal => ¬ state.mctx.decls.contains goal) |>.map (·.name.toString)
     .error s!"Goals {invalid_goals} are not in scope"
   -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
   let unassigned := goals.filter λ goal =>
@@ -165,17 +195,21 @@ protected def GoalState.isSolved (goalState : GoalState) : Bool :=
     | .some e => ¬ e.hasExprMVar
     | .none => true
   goalState.goals.isEmpty && solvedRoot
-@[export pantograph_goal_state_parent_expr]
-protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
-  let parent ← goalState.parentMVar?
-  let expr := goalState.mctx.eAssignment.find! parent
-  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  return expr
 @[export pantograph_goal_state_get_mvar_e_assignment]
 protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do
   let expr ← goalState.mctx.eAssignment.find? mvarId
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   return expr
+@[export pantograph_goal_state_parent_exprs]
+protected def GoalState.parentExprs (state : GoalState) : List Expr :=
+  state.parentMVars.map λ goal => state.getMVarEAssignment goal |>.get!
+@[always_inline]
+protected def GoalState.hasUniqueParent (state : GoalState) : Bool :=
+  state.parentMVars.length == 1
+@[always_inline]
+protected def GoalState.parentExpr! (state : GoalState) : Expr :=
+  assert! state.parentMVars.length == 1
+  (state.getMVarEAssignment state.parentMVars[0]!).get!
 
 deriving instance BEq for DelayedMetavarAssignment
 
@@ -187,7 +221,8 @@ if conflicting assignments exist. We also assume the monotonicity property: In a
 chain of descending goal states, a mvar cannot be unassigned, and once assigned
 its assignment cannot change. -/
 @[export pantograph_goal_state_replay_m]
-protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM GoalState := do
+protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM GoalState :=
+  withTraceNode `Pantograph.GoalState.replay (fun _ => return m!"replay") do
   let srcNGen := src.coreState.ngen
   let srcNGen' := src'.coreState.ngen
   let dstNGen := dst.coreState.ngen
@@ -211,6 +246,8 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
       else
         id
     | id => id
+  let mapMVar : MVarId → MVarId
+    | { name } => ⟨mapId name⟩
   let rec mapLevel : Level → Level
     | .succ x => .succ (mapLevel x)
     | .max l1 l2 => .max (mapLevel l1) (mapLevel l2)
@@ -224,7 +261,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
   let mapDelayedAssignment (d : DelayedMetavarAssignment) : CoreM DelayedMetavarAssignment := do
     let { mvarIdPending, fvars } := d
     return {
-      mvarIdPending := ⟨mapId mvarIdPending.name⟩,
+      mvarIdPending := mapMVar mvarIdPending,
       fvars := ← fvars.mapM mapExpr,
     }
   let mapLocalDecl (ldecl : LocalDecl) : CoreM LocalDecl := do
@@ -305,6 +342,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
     }
   }
   let m : MetaM Meta.SavedState := Meta.withMCtx mctx do
+    restoreCoreMExtra savedMeta.core
     savedMeta.restore
 
     for (lmvarId, l') in src'.mctx.lAssignment do
@@ -336,7 +374,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
         throwError "Conflicting assignment of expr metavariable (d != d) {mvarId.name}"
 
     Meta.saveState
-  let goals :=dst.savedState.tactic.goals ++
+  let goals := dst.savedState.tactic.goals ++
     src'.savedState.tactic.goals.map (⟨mapId ·.name⟩)
   let fragments ← src'.fragments.foldM (init := dst.fragments) λ acc mvarId' fragment' => do
     let mvarId := ⟨mapId mvarId'.name⟩
@@ -355,18 +393,21 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
         meta := ← m.run',
       },
     },
+    parentMVars := dst.parentMVars ++ src.parentMVars.map mapMVar,
     fragments,
   }
 
 --- Tactic execution functions ---
 
--- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
+/--
+These descendants serve as "seed" mvars. If a MVarError's mvar is related to one
+of these seed mvars, it means an error has occurred when a tactic was executing
+on `src`. `evalTactic`, will not capture these mvars, so we need to manually
+find them and save them into the goal list. See the rationales document for the
+inspiration of this function.
+-/
 private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
-  -- These descendants serve as "seed" mvars. If a MVarError's mvar is related
+  -- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
-  -- to one of these seed mvars, it means an error has occurred when a tactic
-  -- was executing on `src`. `evalTactic`, will not capture these mvars, so we
-  -- need to manually find them and save them into the goal list.
-
   let descendants ←  Meta.getMVars (.mvar src)
   --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
   let mut alreadyVisited : MVarIdSet := {}
@@ -381,6 +422,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
         result := mvarDeps.foldl (·.insert ·) result
   return result.toList
 
+/-- Merger of two unique lists -/
 private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
   let li2' := li2.filter (¬ li1.contains ·)
   li1 ++ li2'
@@ -390,28 +432,29 @@ Set `guardMVarErrors` to true to capture mvar errors. Lean will not
 automatically collect mvars from text tactics (vide
 `test_tactic_failure_synthesize_placeholder`)
 -/
-protected def GoalState.step' { α } (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM α) (guardMVarErrors : Bool := false)
+protected def GoalState.step' { α } (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM α) (guardMVarErrors : Bool := false)
   : Elab.TermElabM (α × GoalState) := do
-  unless (← getMCtx).decls.contains goal do
+  let ((a, parentMVars), { goals }) ← site.runTacticM tacticM
-    throwError s!"Goal is not in context: {goal.name}"
+    |>.run { elaborator := .anonymous }
-  goal.checkNotAssigned `GoalState.step
+    |>.run state.savedState.tactic
-  let (a, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
   let nextElabState ← MonadBacktrack.saveState
   --Elab.Term.synthesizeSyntheticMVarsNoPostponing
 
   let goals ← if guardMVarErrors then
-      pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
+      parentMVars.foldlM (init := goals) λ goals parent => do
+        let errors ← collectAllErroredMVars parent
+        return mergeMVarLists goals errors
     else
       pure goals
   let state' := {
     state with
     savedState := { term := nextElabState, tactic := { goals }, },
-    parentMVar? := .some goal,
+    parentMVars,
   }
   return (a, state')
-protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
+protected def GoalState.step (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
   : Elab.TermElabM GoalState :=
-  Prod.snd <$> GoalState.step' state goal tacticM guardMVarErrors
+  Prod.snd <$> GoalState.step' state site tacticM guardMVarErrors
 
 /-- Response for executing a tactic -/
 inductive TacticResult where
@@ -424,21 +467,21 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message : String)
 
-private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Bool × Array String) := do
+private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × Array String) := do
   let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength
   let hasErrors := newMessages.any (·.severity == .error)
   let newMessages ← newMessages.mapM λ m => m.toString
   Core.resetMessageLog
   return (hasErrors, newMessages.toArray)
 
+/-- Execute a `TermElabM` producing a goal state, capturing the error and turn it into a `TacticResult` -/
 def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do
-  -- FIXME: Maybe message log should be empty
+  assert! (← Core.getMessageLog).toList.isEmpty
-  let prevMessageLength := (← Core.getMessageLog).toList.length
   try
     let state ← elabM
 
     -- Check if error messages have been generated in the core.
-    let (hasError, newMessages) ← dumpMessageLog prevMessageLength
+    let (hasError, newMessages) ← dumpMessageLog
     if hasError then
       return .failure newMessages
     else
@@ -446,62 +489,58 @@ def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM
   catch exception =>
     match exception with
     | .internal _ =>
-      let (_, messages) ← dumpMessageLog prevMessageLength
+      let (_, messages) ← dumpMessageLog
       return .failure messages
     | _ => return .failure #[← exception.toMessageData.toString]
 
 /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM
-    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+    (state: GoalState) (site : Site)
+    (tacticM: Elab.Tactic.TacticM Unit)
     (guardMVarErrors : Bool := false)
-    : Elab.TermElabM TacticResult := do
+    : Elab.TermElabM TacticResult :=
   withCapturingError do
-    state.step goal tacticM guardMVarErrors
+    state.step site tacticM guardMVarErrors
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
 @[export pantograph_goal_state_try_tactic_m]
-protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
+protected def GoalState.tryTactic (state: GoalState) (site : Site) (tactic: String):
     Elab.TermElabM TacticResult := do
   state.restoreElabM
-  /-
+  let .some goal := state.actingGoal? site | throwNoGoals
   if let .some fragment := state.fragments[goal]? then
     return ← withCapturingError do
-      let (moreFragments, state') ← state.step' goal (fragment.step goal tactic)
+      let (fragments, state') ← state.step' site do
-      let fragments := moreFragments.fold (init := state.fragments.erase goal) λ acc mvarId f =>
+        fragment.step goal tactic $ state.fragments.erase goal
-        acc.insert mvarId f
+      return { state' with fragments }
-      return { state' with fragments } -/
-
-  let catName := match isLHSGoal? (← goal.getType) with
-    | .some _ => `conv
-    | .none => `tactic
   -- Normal tactic without fragment
   let tactic ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
+    (env := ← getEnv)
-    (catName := catName)
+    (catName := `tactic)
     (input := tactic)
     (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
   let tacticM := Elab.Tactic.evalTactic tactic
   withCapturingError do
-    state.step goal tacticM (guardMVarErrors := true)
+    state.step site tacticM (guardMVarErrors := true)
 
 -- Specialized Tactics
 
-protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
+protected def GoalState.tryAssign (state : GoalState) (site : Site) (expr : String)
-      Elab.TermElabM TacticResult := do
+    : Elab.TermElabM TacticResult := do
   state.restoreElabM
   let expr ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
+    (env := ← getEnv)
     (catName := `term)
     (input := expr)
     (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goal $ Tactic.evalAssign expr
+  state.tryTacticM site $ Tactic.evalAssign expr
 
-protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
+protected def GoalState.tryLet (state : GoalState) (site : Site) (binderName : String) (type : String)
-      Elab.TermElabM TacticResult := do
+    : Elab.TermElabM TacticResult := do
   state.restoreElabM
   let type ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
@@ -510,28 +549,30 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St
     (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goal $ Tactic.evalLet binderName.toName type
+  state.tryTacticM site $ Tactic.evalLet binderName.toName type
 
 /-- Enter conv tactic mode -/
 @[export pantograph_goal_state_conv_enter_m]
-protected def GoalState.conv (state : GoalState) (goal : MVarId) :
+protected def GoalState.convEnter (state : GoalState) (site : Site) :
       Elab.TermElabM TacticResult := do
+  let .some goal := state.actingGoal? site | throwNoGoals
   if let .some (.conv ..) := state.fragments[goal]? then
     return .invalidAction "Already in conv state"
-  goal.checkNotAssigned `GoalState.conv
   withCapturingError do
-    let (fragment, state') ← state.step' goal Fragment.enterConv
+    let (fragments, state') ← state.step' site Fragment.enterConv
     return {
       state' with
-      fragments := state'.fragments.insert goal fragment
+      fragments := fragments.fold (init := state'.fragments) λ acc goal fragment =>
+        acc.insert goal fragment
     }
 
-/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
+/-- Exit from a tactic fragment. -/
-@[export pantograph_goal_state_conv_exit_m]
+@[export pantograph_goal_state_fragment_exit_m]
-protected def GoalState.convExit (state : GoalState) (goal : MVarId):
+protected def GoalState.fragmentExit (state : GoalState) (site : Site):
       Elab.TermElabM TacticResult := do
-  let .some fragment@(.conv ..) := state.fragments[goal]? |
+  let .some goal := state.actingGoal? site | throwNoGoals
-    return .invalidAction "Not in conv state"
+  let .some fragment := state.fragments[goal]? |
+    return .invalidAction "Goal does not have a fragment"
   withCapturingError do
     let (fragments, state') ← state.step' goal (fragment.exit goal state.fragments)
     return {
@@ -543,18 +584,17 @@ protected def GoalState.calcPrevRhsOf? (state : GoalState) (goal : MVarId) : Opt
   let .some (.calc prevRhs?) := state.fragments[goal]? | .none
   prevRhs?
 
-@[export pantograph_goal_state_try_calc_m]
+@[export pantograph_goal_state_calc_enter_m]
-protected def GoalState.tryCalc (state : GoalState) (goal : MVarId) (pred : String)
+protected def GoalState.calcEnter (state : GoalState) (site : Site)
   : Elab.TermElabM TacticResult := do
-  let prevRhs? := state.calcPrevRhsOf? goal
+  let .some goal := state.actingGoal? site | throwNoGoals
+  if let .some _ := state.fragments[goal]? then
+    return .invalidAction "Goal already has a fragment"
   withCapturingError do
-    let (moreFragments, state') ← state.step' goal do
+    let fragment := Fragment.enterCalc
-      let fragment := Fragment.calc prevRhs?
+    let fragments := state.fragments.insert goal fragment
-      fragment.step goal pred
-    let fragments := moreFragments.fold (init := state.fragments.erase goal) λ acc mvarId f =>
-      acc.insert mvarId f
     return {
-      state' with
+      state with
       fragments,
     }
 

Pantograph/Library.lean

@@ -117,10 +117,10 @@ def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState :
 
 @[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
-  runMetaM <| state.serializeGoals (parent := .none) options
+  runMetaM <| state.serializeGoals options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
+def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
   : CoreM Protocol.GoalPrintResult := runMetaM do
   state.restoreMetaM
 
@@ -130,9 +130,10 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
         serializeExpression options (← instantiateAll expr)
     else
       pure .none
-  let parent? ← if parentExpr then
+  let parentExprs? ← if parentExprs then
-      state.parentExpr?.mapM λ expr => state.withParentContext do
+      .some <$> state.parentMVars.mapM λ parent => parent.withContext do
-        serializeExpression options (← instantiateAll expr)
+        let val := state.getMVarEAssignment parent |>.get!
+        serializeExpression options (← instantiateAll val)
     else
       pure .none
   let goals ← if goals then
@@ -148,7 +149,7 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
   let env ← getEnv
   return {
     root?,
-    parent?,
+    parentExprs?,
     goals,
     extraMVars,
     rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false,
@@ -157,26 +158,26 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
   }
 
 @[export pantograph_goal_have_m]
-protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryHave (state: GoalState) (site : Site) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
   let type ← match (← parseTermM type) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.restoreElabM
-  state.tryTacticM goal $ Tactic.evalHave binderName.toName type
+  state.tryTacticM site $ Tactic.evalHave binderName.toName type
 @[export pantograph_goal_try_define_m]
-protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryDefine (state: GoalState) (site : Site) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.restoreElabM
-  state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
+  state.tryTacticM site $ Tactic.evalDefine binderName.toName expr
 @[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryDraft (state: GoalState) (site : Site) (expr: String): Elab.TermElabM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.restoreElabM
-  state.tryTacticM goal (Tactic.evalDraft expr)
+  state.tryTacticM site $ Tactic.evalDraft expr
 
 -- Cancel the token after a timeout.
 @[export pantograph_run_cancel_token_with_timeout_m]

Pantograph/Protocol.lean

@@ -60,16 +60,21 @@ structure Variable where
   type?: Option Expression  := .none
   value?: Option Expression := .none
   deriving Lean.ToJson
+inductive Fragment where
+  | tactic
+  | conv
+  | calc
+  deriving BEq, DecidableEq, Repr, Lean.ToJson
 structure Goal where
-  name: String := ""
   /-- Name of the metavariable -/
-  userName?: Option String  := .none
+  name : String := ""
-  /-- Is the goal in conversion mode -/
+  /-- User-facing name -/
-  isConversion: Bool        := false
+  userName? : Option String  := .none
+  fragment : Fragment := .tactic
   /-- target expression type -/
-  target: Expression
+  target : Expression
   /-- Variables -/
-  vars: Array Variable      := #[]
+  vars : Array Variable      := #[]
   deriving Lean.ToJson
 
 
@@ -87,6 +92,7 @@ structure InteractionError where
   deriving Lean.ToJson
 
 def errorIndex (desc: String): InteractionError := { error := "index", desc }
+def errorOperation (desc: String): InteractionError := { error := "operation", desc }
 def errorExpr (desc: String): InteractionError := { error := "expr", desc }
 
 
@@ -248,17 +254,17 @@ structure GoalStartResult where
   root: String
   deriving Lean.ToJson
 structure GoalTactic where
-  -- Identifiers for tree, state, and goal
   stateId: Nat
-  goalId: Nat := 0
+  -- If omitted, act on the first goal
+  goalId?: Option Nat := .none
+  -- If set to true, goal will not go dormant. Defaults to `automaticMode`
+  autoResume?: Option Bool := .none
   -- One of the fields here must be filled
   tactic?: Option String := .none
+  mode?: Option String := .none -- Changes the current category to {"tactic", "calc", "conv"}
   expr?: Option String := .none
   have?: Option String := .none
   let?: Option String := .none
-  calc?: Option String := .none
-  -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
-  conv?: Option Bool := .none
   draft?: Option String := .none
 
   -- In case of the `have` tactic, the new free variable name is provided here
@@ -308,8 +314,8 @@ structure GoalPrint where
 
   -- Print root?
   rootExpr?: Option Bool := .some False
-  -- Print the parent expr?
+  -- Print the parent expressions
-  parentExpr?: Option Bool := .some False
+  parentExprs?: Option Bool := .some False
   -- Print goals?
   goals?: Option Bool := .some False
   -- Print values of extra mvars?
@@ -319,7 +325,7 @@ structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
-  parent?: Option Expression := .none
+  parentExprs?: Option (List Expression) := .none
   goals: Array Goal := #[]
   extraMVars: Array Expression := #[]
 

Pantograph/Serial.lean

@@ -128,7 +128,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background
       tactic
     }
     root,
-    parentMVar?,
+    parentMVars,
     fragments,
   } := goalState
   pickle path (
@@ -140,7 +140,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background
     tactic,
 
     root,
-    parentMVar?,
+    parentMVars,
     fragments,
   )
 
@@ -156,7 +156,7 @@ def goalStateUnpickle (path : System.FilePath) (background? : Option Environment
     tactic,
 
     root,
-    parentMVar?,
+    parentMVars,
     fragments,
   ), region) ← Pantograph.unpickle (
     DistilledEnvironment ×
@@ -167,7 +167,7 @@ def goalStateUnpickle (path : System.FilePath) (background? : Option Environment
     Elab.Tactic.State ×
 
     MVarId ×
-    Option MVarId ×
+    List MVarId ×
     FragmentMap
   ) path
   let env ← resurrectEnvironment distilledEnv background?
@@ -187,7 +187,7 @@ def goalStateUnpickle (path : System.FilePath) (background? : Option Environment
       tactic,
     },
     root,
-    parentMVar?,
+    parentMVars,
     fragments,
   }
   return (goalState, region)

Pantograph/Tactic/Fragment.lean

@@ -4,6 +4,13 @@ Here, a unified system handles all fragments.
 
 Inside a tactic fragment, the parser category may be different. An incomplete
 fragmented tactic may not be elaboratable..
+
+In line with continuation/resumption paradigms, the exit function of a fragment
+tactic is responsible for resuming incomplete goals with fragments. For example,
+when a conversion tactic finishes, the sentinels should resume the root of the
+conversion tactic goal. The user cannot be expected to execute this resumption,
+since the root is automatically dormanted at the entry of the conversion tactic
+mode.
 -/
 import Lean.Meta
 import Lean.Elab
@@ -14,59 +21,79 @@ namespace Pantograph
 
 inductive Fragment where
   | calc (prevRhs? : Option Expr)
-  | conv (rhs : MVarId) (dormant : List MVarId)
+  | conv (rhs : MVarId)
-  deriving BEq
+  -- This goal is spawned from a `conv`
+  | convSentinel (parent : MVarId)
+  deriving BEq, Inhabited
+
 abbrev FragmentMap := Std.HashMap MVarId Fragment
 def FragmentMap.empty : FragmentMap := Std.HashMap.emptyWithCapacity 2
+protected def FragmentMap.filter (map : FragmentMap) (pred : MVarId → Fragment → Bool) : FragmentMap :=
+  map.fold (init := FragmentMap.empty) λ acc mvarId fragment =>
+    if pred mvarId fragment then
+      acc.insert mvarId fragment
+    else
+      acc
 
 protected def Fragment.map (fragment : Fragment) (mapExpr : Expr → CoreM Expr) : CoreM Fragment :=
-  let mapMVarId (mvarId : MVarId) : CoreM MVarId :=
+  let mapMVar (mvarId : MVarId) : CoreM MVarId :=
     return (← mapExpr (.mvar mvarId)) |>.mvarId!
   match fragment with
   | .calc prevRhs? => return .calc (← prevRhs?.mapM mapExpr)
-  | .conv rhs dormant => do
+  | .conv rhs => do
-    let rhs' ← mapMVarId rhs
+    let rhs' ← mapMVar rhs
-    let dormant' ← dormant.mapM mapMVarId
+    return .conv rhs'
-    return .conv rhs' dormant'
+  | .convSentinel parent => do
+    return .convSentinel (← mapMVar parent)
 
-protected def Fragment.enterCalc : Elab.Tactic.TacticM Fragment := do
+protected def Fragment.enterCalc : Fragment := .calc .none
-  return .calc .none
+protected def Fragment.enterConv : Elab.Tactic.TacticM FragmentMap := do
-protected def Fragment.enterConv : Elab.Tactic.TacticM Fragment := do
   let goal ← Elab.Tactic.getMainGoal
-  let rhs ← goal.withContext do
+  goal.checkNotAssigned `GoalState.conv
-    let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
+  let (rhs, newGoal) ← goal.withContext do
-    Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
+    let target ← instantiateMVars (← goal.getType)
-    pure rhs.mvarId!
+    let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor target
-  let otherGoals := (← Elab.Tactic.getGoals).filter (· != goal)
+    pure (rhs.mvarId!, newGoal.mvarId!)
-  return conv rhs otherGoals
+  Elab.Tactic.replaceMainGoal [newGoal]
+  return FragmentMap.empty
+    |>.insert goal (.conv rhs)
+    |>.insert newGoal (.convSentinel goal)
 
-protected def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : FragmentMap)
+protected partial def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : FragmentMap)
   : Elab.Tactic.TacticM FragmentMap :=
   match fragment with
   | .calc .. => do
     Elab.Tactic.setGoals [goal]
     return fragments.erase goal
-  | .conv rhs otherGoals => do
+  | .conv rhs => do
-    -- FIXME: Only process the goals that are descendants of `goal`
+    let goals := (← Elab.Tactic.getGoals).filter λ descendant =>
-    let goals := (← Elab.Tactic.getGoals).filter λ goal => true
+      match fragments[descendant]? with
-      --match fragments[goal]? with
+      | .some s => (.convSentinel goal) == s
-      --| .some f => fragment == f
+      | _ => false -- Not a conv goal from this
-      --| .none => false -- Not a conv goal from this
     -- Close all existing goals with `refl`
     for mvarId in goals do
       liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
-    Elab.Tactic.pruneSolvedGoals
     unless (← goals.filterM (·.isAssignedOrDelayedAssigned)).isEmpty do
       throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (goals)}"
 
-    Elab.Tactic.setGoals $ [goal] ++ otherGoals
+    -- Ensure the meta tactic runs on `goal` even if its dormant by forcing resumption
+    Elab.Tactic.setGoals $ goal :: (← Elab.Tactic.getGoals)
     let targetNew ← instantiateMVars (.mvar rhs)
     let proof ← instantiateMVars (.mvar goal)
 
     Elab.Tactic.liftMetaTactic1 (·.replaceTargetEq targetNew proof)
-    return fragments.erase goal
 
-protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String)
+    -- Try to solve maiinline by rfl
+    let mvarId ← Elab.Tactic.getMainGoal
+    liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
+    Elab.Tactic.pruneSolvedGoals
+    return fragments.filter λ mvarId fragment =>
+      !(mvarId == goal || fragment == .convSentinel goal)
+  | .convSentinel parent =>
+    let parentFragment := fragments[parent]!
+    parentFragment.exit parent (fragments.erase goal)
+
+protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String) (map : FragmentMap)
   : Elab.Tactic.TacticM FragmentMap := goal.withContext do
   assert! ¬ (← goal.isAssigned)
   match fragment with
@@ -121,9 +148,41 @@ protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String)
     let goals := [ mvarBranch ] ++ remainder?.toList
     Elab.Tactic.setGoals goals
     match remainder? with
-    | .some goal => return FragmentMap.empty.insert goal $ .calc (.some rhs)
+    | .some goal => return map.erase goal |>.insert goal $ .calc (.some rhs)
-    | .none => return .empty
+    | .none => return map
   | .conv .. => do
     throwError "Direct operation on conversion tactic parent goal is not allowed"
+  | fragment@(.convSentinel parent) => do
+    assert! isLHSGoal? (← goal.getType) |>.isSome
+    let tactic ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `conv)
+      (input := s)
+      (fileName := ← getFileName) with
+      | .ok stx => pure $ stx
+      | .error error => throwError error
+    let oldGoals ← Elab.Tactic.getGoals
+    -- Label newly generated goals as conv sentinels
+    Elab.Tactic.evalTactic tactic
+    let newConvGoals ← (← Elab.Tactic.getUnsolvedGoals).filterM λ g => do
+      -- conv tactic might generate non-conv goals
+      if oldGoals.contains g then
+        return false
+      return isLHSGoal? (← g.getType) |>.isSome
+    -- Conclude the conv by exiting the parent fragment if new goals is empty
+    if newConvGoals.isEmpty then
+      let hasSiblingFragment := map.fold (init := false) λ flag _ fragment =>
+        if flag then
+          true
+        else match fragment with
+          | .convSentinel parent' => parent == parent'
+          | _ => false
+      if ¬ hasSiblingFragment then
+        -- This fragment must exist since we have conv goals
+        let parentFragment := map[parent]!
+        -- All descendants exhausted. Exit from the parent conv.
+        return ← parentFragment.exit parent map
+    return newConvGoals.foldl (init := map) λ acc g =>
+      acc.insert g fragment
 
 end Pantograph

Repl.lean

@@ -97,6 +97,77 @@ def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name
   }
   runCoreM $ termElabM.run' context state |>.run'
 
+section Goal
+
+def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
+  let state ← getMainState
+  let .some goalState := state.goalStates[args.stateId]? |
+    Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.stateId}"
+  let unshielded := args.autoResume?.getD state.options.automaticMode
+  let site ← match args.goalId?, unshielded with
+    | .some goalId, true => do
+      let .some goal := goalState.goals[goalId]? |
+        Protocol.throw $ Protocol.errorIndex s!"Invalid goal index {goalId}"
+      pure (.prefer goal)
+    | .some goalId, false => do
+      let .some goal := goalState.goals[goalId]? |
+        Protocol.throw $ Protocol.errorIndex s!"Invalid goal index {goalId}"
+      pure (.focus goal)
+    | .none, true => pure .unfocus
+    | .none, false => do
+      let .some goal := goalState.mainGoal? |
+        Protocol.throw $ Protocol.errorIndex s!"No goals to be solved"
+      pure (.focus goal)
+  let nextGoalState?: Except _ TacticResult ← liftTermElabM do
+    -- NOTE: Should probably use a macro to handle this...
+    match args.tactic?, args.mode?, args.expr?, args.have?, args.let?, args.draft?  with
+    | .some tactic, .none, .none, .none, .none, .none => do
+      pure $ Except.ok $ ← goalState.tryTactic site tactic
+    | .none, .some mode, .none, .none, .none, .none => match mode with
+      | "tactic" => do -- Exit from the current fragment
+        pure $ Except.ok $ ← goalState.fragmentExit site
+      | "conv" => do
+        pure $ Except.ok $ ← goalState.convEnter site
+      | "calc" => do
+        pure $ Except.ok $ ← goalState.calcEnter site
+      | _ => pure $ .error $ Protocol.errorOperation s!"Invalid mode {mode}"
+    | .none, .none, .some expr, .none, .none, .none => do
+      pure $ Except.ok $ ← goalState.tryAssign site expr
+    | .none, .none, .none, .some type, .none, .none => do
+      let binderName := args.binderName?.getD ""
+      pure $ Except.ok $ ← goalState.tryHave site binderName type
+    | .none, .none, .none, .none, .some type, .none => do
+      let binderName := args.binderName?.getD ""
+      pure $ Except.ok $ ← goalState.tryLet site binderName type
+    | .none, .none, .none, .none, .none, .some draft => do
+      pure $ Except.ok $ ← goalState.tryDraft site draft
+    | _, _, _, _, _, _ =>
+      pure $ .error $ Protocol.errorOperation
+        "Exactly one of {tactic, mode, expr, have, let, draft} must be supplied"
+  match nextGoalState? with
+  | .error error => Protocol.throw error
+  | .ok (.success nextGoalState messages) => do
+    let nextStateId ← newGoalState nextGoalState
+    let parentExprs := nextGoalState.parentExprs
+    let hasSorry := parentExprs.any (·.hasSorry)
+    let hasUnsafe := parentExprs.any ((← getEnv).hasUnsafe ·)
+    let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run'
+    return {
+      nextStateId? := .some nextStateId,
+      goals? := .some goals,
+      messages? := .some messages,
+      hasSorry,
+      hasUnsafe,
+    }
+  | .ok (.parseError message) =>
+    return { messages? := .none, parseError? := .some message }
+  | .ok (.invalidAction message) =>
+    Protocol.throw $ errorI "invalid" message
+  | .ok (.failure messages) =>
+    return { messages? := .some messages }
+
+end Goal
+
 section Frontend
 
 structure CompilationUnit where
@@ -225,7 +296,6 @@ def execute (command: Protocol.Command): MainM Json := do
     return toJson error
   where
   errorCommand := errorI "command"
-  errorIndex := errorI "index"
   errorIO := errorI "io"
   -- Command Functions
   reset (_: Protocol.Reset): EMainM Protocol.StatResult := do
@@ -290,7 +360,7 @@ def execute (command: Protocol.Command): MainM Json := do
       | .some expr, .none => goalStartExpr expr |>.run
       | .none, .some copyFrom => do
         (match (← getEnv).find? <| copyFrom.toName with
-        | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
+        | .none => return .error <| Protocol.errorIndex s!"Symbol not found: {copyFrom}"
         | .some cInfo => return .ok (← GoalState.create cInfo.type))
       | _, _ =>
         return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied"
@@ -299,70 +369,14 @@ def execute (command: Protocol.Command): MainM Json := do
     | .ok goalState =>
       let stateId ← newGoalState goalState
       return { stateId, root := goalState.root.name.toString }
-  goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
-    let state ← getMainState
-    let .some goalState := state.goalStates[args.stateId]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
-    -- FIXME: Allow proper conversion tactic exit even in automatic mode
-    let .some goal := goalState.goals[args.goalId]? |
-      Protocol.throw $ errorIndex s!"Invalid goal index {args.goalId}"
-    let nextGoalState?: Except _ TacticResult ← liftTermElabM do
-      -- NOTE: Should probably use a macro to handle this...
-      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft?  with
-      | .some tactic, .none, .none, .none, .none, .none, .none => do
-        pure <| Except.ok <| ← goalState.tryTactic goal tactic
-      | .none, .some expr, .none, .none, .none, .none, .none => do
-        pure <| Except.ok <| ← goalState.tryAssign goal expr
-      | .none, .none, .some type, .none, .none, .none, .none => do
-        let binderName := args.binderName?.getD ""
-        pure <| Except.ok <| ← goalState.tryHave goal binderName type
-      | .none, .none, .none, .some type, .none, .none, .none => do
-        let binderName := args.binderName?.getD ""
-        pure <| Except.ok <| ← goalState.tryLet goal binderName type
-      | .none, .none, .none, .none, .some pred, .none, .none => do
-        pure <| Except.ok <| ← goalState.tryCalc goal pred
-      | .none, .none, .none, .none, .none, .some true, .none => do
-        pure <| Except.ok <| ← goalState.conv goal
-      | .none, .none, .none, .none, .none, .some false, .none => do
-        pure <| Except.ok <| ← goalState.convExit goal
-      | .none, .none, .none, .none, .none, .none, .some draft => do
-        pure <| Except.ok <| ← goalState.tryDraft goal draft
-      | _, _, _, _, _, _, _ =>
-        let error := errorI "arguments" "Exactly one of {tactic, expr, have, let, calc, conv, draft} must be supplied"
-        pure $ .error error
-    match nextGoalState? with
-    | .error error => Protocol.throw error
-    | .ok (.success nextGoalState messages) => do
-      let nextGoalState ← match state.options.automaticMode, args.conv? with
-        | true, .none => do
-          pure $ nextGoalState.immediateResume goalState
-        | true, .some true => pure nextGoalState
-        | true, .some false => pure nextGoalState
-        | false, _ => pure nextGoalState
-      let nextStateId ← newGoalState nextGoalState
-      let parentExpr := nextGoalState.parentExpr?.get!
-      let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
-      return {
-        nextStateId? := .some nextStateId,
-        goals? := .some goals,
-        messages? := .some messages,
-        hasSorry := parentExpr.hasSorry,
-        hasUnsafe := (← getEnv).hasUnsafe parentExpr,
-      }
-    | .ok (.parseError message) =>
-      return { messages? := .none, parseError? := .some message }
-    | .ok (.invalidAction message) =>
-      Protocol.throw $ errorI "invalid" message
-    | .ok (.failure messages) =>
-      return { messages? := .some messages }
   goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
     let state ← getMainState
     let .some target := state.goalStates[args.target]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.target}"
+      Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.target}"
     let nextGoalState? : GoalState  ← match args.branch?, args.goals? with
       | .some branchId, .none => do
         match state.goalStates[branchId]? with
-        | .none => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
+        | .none => Protocol.throw $ Protocol.errorIndex s!"Invalid state index {branchId}"
         | .some branch => pure $ target.continue branch
       | .none, .some goals =>
         let goals := goals.toList.map (λ n => { name := n.toName })
@@ -385,11 +399,11 @@ def execute (command: Protocol.Command): MainM Json := do
   goal_print (args: Protocol.GoalPrint): EMainM Protocol.GoalPrintResult := do
     let state ← getMainState
     let .some goalState := state.goalStates[args.stateId]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
+      Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.stateId}"
     let result ← liftMetaM <| goalPrint
         goalState
         (rootExpr := args.rootExpr?.getD False)
-        (parentExpr := args.parentExpr?.getD False)
+        (parentExprs := args.parentExprs?.getD False)
         (goals := args.goals?.getD False)
         (extraMVars := args.extraMVars?.getD #[])
         (options := state.options)
@@ -397,7 +411,7 @@ def execute (command: Protocol.Command): MainM Json := do
   goal_save (args: Protocol.GoalSave): EMainM Protocol.GoalSaveResult := do
     let state ← getMainState
     let .some goalState := state.goalStates[args.id]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.id}"
+      Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.id}"
     goalStatePickle goalState args.path
     return {}
   goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do

Test/Integration.lean

@@ -88,10 +88,10 @@ def test_tactic : Test := do
    ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult)
   step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
    ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
-  step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
+  step "goal.print" ({ stateId := 1, parentExprs? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
    ({
      root? := .some { pp? := "fun x => ?m.11"},
-     parent? := .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)

Test/Main.lean

@@ -55,6 +55,7 @@ def main (args: List String) := do
     ("Delate", Delate.suite),
     ("Serial", Serial.suite),
     ("Tactic/Assign", Tactic.Assign.suite),
+    ("Tactic/Fragment", Tactic.Fragment.suite),
     ("Tactic/Prograde", Tactic.Prograde.suite),
     ("Tactic/Special", Tactic.Special.suite),
   ]

Test/Proofs.lean

@@ -32,7 +32,7 @@ def startProof (start: Start): TestM (Option GoalState) := do
     let expr ← parseSentence expr
     return .some $ ← GoalState.create (expr := expr)
 
-def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
+private def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
     (userName?: Option String := .none): Protocol.Goal :=
   {
     name,
@@ -43,7 +43,7 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S
       type? := .some { pp? := .some x.snd },
     })).toArray
   }
-def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+private def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
     Protocol.Goal :=
   {
     userName?,
@@ -53,7 +53,7 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
       type? := .some { pp? := .some x.snd },
     })).toArray
   }
-def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
+private def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
   let coreContext: Lean.Core.Context ← createCoreContext #[]
@@ -77,7 +77,7 @@ def test_identity: TestM Unit := do
   addTest $ LSpec.check "intro" ((← state1.serializeGoals (options := ← read)).map (·.name) =
     #[inner])
   let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr!)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
 
 -- Individual test cases
@@ -117,41 +117,6 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
   addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
 
   return ()
-def test_delta_variable: TestM Unit := do
-  let options: Protocol.Options := { noRepeat := true }
-  let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
-  addTest $ LSpec.check "Start goal" state?.isSome
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
-    #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
-  let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
-    #[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
-  return ()
-  where
--- Like `buildGoal` but allow certain variables to be elided.
-  buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
-    {
-      target := { pp? := .some target},
-      vars := (nameType.map fun x => ({
-        userName := x.fst,
-        type? := x.snd.map (λ type => { pp? := type }),
-      })).toArray
-    }
 
 example (w x y z : Nat) (p : Nat → Prop)
         (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
@@ -212,8 +177,8 @@ def test_or_comm: TestM Unit := do
     | .none => do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
-  addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
+  checkTrue "(0 parent)" state0.parentMVars.isEmpty
-  addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
+  checkTrue "(0 root)" state0.rootExpr?.isNone
 
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
@@ -237,11 +202,11 @@ def test_or_comm: TestM Unit := do
         { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
       ]
     }])
-  checkTrue "(1 parent)" state1.parentExpr?.isSome
+  checkTrue "(1 parent)" state1.hasUniqueParent
   checkTrue "(1 root)" $ ¬ state1.isSolved
 
   let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr!)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
   let tactic := "cases h"
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
@@ -256,11 +221,11 @@ def test_or_comm: TestM Unit := do
   let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
     #[caseL, caseR])
-  checkTrue "(2 parent exists)" state2.parentExpr?.isSome
+  checkTrue "(2 parent exists)" state2.hasUniqueParent
   checkTrue "(2 root)" $ ¬ state2.isSolved
 
   let state2parent ← state2.withParentContext do
-    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr!)
   let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
   let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
   let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
@@ -276,7 +241,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   let state3_1parent ← state3_1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr!)
   let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
   addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
@@ -286,7 +251,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
+  let state4_1parent ← instantiateAll state4_1.parentExpr!
   addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
   checkTrue "(4_1 root)" $ ¬ state4_1.isSolved
   let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
@@ -336,194 +301,6 @@ def test_or_comm: TestM Unit := do
       ]
     }
 
-example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
-  intro a b c1 c2 h
-  conv =>
-    lhs
-    congr
-    . rw [Nat.add_comm]
-    . rfl
-  exact h
-
-def test_conv: TestM Unit := do
-  let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  let tactic := "intro a b c1 c2 h"
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[interiorGoal [] "a + b + c1 = b + a + c2"])
-
-  let goalConv := state1.goals[0]!
-  let state2 ← match ← state1.conv (state1.get! 0) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
-
-  let convTactic := "rhs"
-  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
-
-  let convTactic := "lhs"
-  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
-
-  let convTactic := "congr"
-  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
-      { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
-    ])
-
-  let convTactic := "rw [Nat.add_comm]"
-  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
-
-  let convTactic := "rfl"
-  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state4_1 ← match state6_1.continue state4 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ expectationFailure "continue" e
-      return ()
-
-  let convTactic := "rfl"
-  let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state1_1 ← match ← state6.convExit goalConv with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-
-  let tactic := "exact h"
-  let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  where
-    h := "b + a + c1 = b + a + c2"
-    interiorGoal (free: List (String × String)) (target: String) :=
-      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
-      buildGoal free target
-
-example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
-  intro a b c d h1 h2
-  calc a + b = b + c := by apply h1
-    _ = c + d := by apply h2
-
-def test_calc: TestM Unit := do
-  let state? ← startProof (.expr "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-  let tactic := "intro a b c d h1 h2"
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[interiorGoal [] "a + b = c + d"])
-  let pred := "a + b = b + c"
-  let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      interiorGoal [] "a + b = b + c" (.some "calc"),
-      interiorGoal [] "b + c = c + d"
-    ])
-  addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
-  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
-
-  let tactic := "apply h1"
-  let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  let state3 ← match state2m.continue state2 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ expectationFailure "continue" e
-      return ()
-  let pred := "_ = c + d"
-  let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      interiorGoal [] "b + c = c + d" (.some "calc")
-    ])
-  addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
-  let tactic := "apply h2"
-  let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
-  where
-    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
-      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
-        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
-      buildGoal free target userName?
-
 def test_tactic_failure_unresolved_goals : TestM Unit := do
   let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
   let state0 ← match state? with
@@ -600,11 +377,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("identity", test_identity),
     ("Nat.add_comm", test_nat_add_comm false),
     ("Nat.add_comm manual", test_nat_add_comm true),
-    ("Nat.add_comm delta", test_delta_variable),
     ("arithmetic", test_arith),
     ("Or.comm", test_or_comm),
-    ("conv", test_conv),
-    ("calc", test_calc),
     ("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals),
     ("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder),
     ("deconstruct", test_deconstruct),

Test/Serial.lean

@@ -87,12 +87,12 @@ def test_pickling_env_extensions : TestM Unit := do
       let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable!
       pure (type, value)
     let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable!
-    let parentExpr := state1.parentExpr?.get!
+    let parentExpr := state1.parentExpr!
     checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
     goalStatePickle state1 statePath
   let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
     let (state1, _) ← goalStateUnpickle statePath (← getEnv)
-    let parentExpr := state1.parentExpr?.get!
+    let parentExpr := state1.parentExpr!
     checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
 
   return ()

Test/Tactic.lean

@@ -1,3 +1,4 @@
 import Test.Tactic.Assign
+import Test.Tactic.Fragment
 import Test.Tactic.Prograde
 import Test.Tactic.Special

Test/Tactic/Fragment.lean

@@ -0,0 +1,312 @@
+import Pantograph.Goal
+import Test.Common
+
+open Lean
+
+namespace Pantograph.Test.Tactic.Fragment
+
+private def buildGoal (nameType: List (String × String)) (target: String):
+    Protocol.Goal :=
+  {
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      userName := x.fst,
+      type? := .some { pp? := .some x.snd },
+    })).toArray
+  }
+
+abbrev TestM := TestT $ Elab.TermElabM
+
+example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
+  intro a b c1 c2 h
+  conv =>
+    lhs
+    congr
+    . rw [Nat.add_comm]
+    . rfl
+  exact h
+
+def test_conv_simple: TestM Unit := do
+  let rootTarget ← parseSentence "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2"
+  let state0 ← GoalState.create rootTarget
+
+  let tactic := "intro a b c1 c2 h"
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
+    #[interiorGoal [] "a + b + c1 = b + a + c2"])
+
+  let goalConv := state1.goals[0]!
+  let state2 ← match ← state1.convEnter (state1.get! 0) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with fragment := .conv }])
+
+  let convTactic := "rhs"
+  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a + c2" with fragment := .conv }])
+
+  let convTactic := "lhs"
+  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1" with fragment := .conv }])
+
+  let convTactic := "congr"
+  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals).map (·.devolatilize) =
+    #[
+      { interiorGoal [] "a + b" with fragment := .conv, userName? := .some "a" },
+      { interiorGoal [] "c1" with fragment := .conv, userName? := .some "a" }
+    ])
+
+  let convTactic := "rw [Nat.add_comm]"
+  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a" with fragment := .conv, userName? := .some "a" }])
+
+  let convTactic := "rfl"
+  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let state4_1 ← match state6_1.continue state4 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+
+  let convTactic := "rfl"
+  let state1_1 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state1_1.serializeGoals).map (·.devolatilize) =
+    #[interiorGoal [] "b + a + c1 = b + a + c2"])
+  checkEq "(fragments)" state1_1.fragments.size 0
+
+  /-
+  let state1_1 ← match ← state6.fragmentExit goalConv with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  -/
+
+  let tactic := "exact h"
+  let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← stateF.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  where
+    h := "b + a + c1 = b + a + c2"
+    interiorGoal (free: List (String × String)) (target: String) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
+      buildGoal free target
+
+example (p : Prop) (x y z : Nat) : p → (p → x = y) → x + z = y + z ∧ p := by
+  intro hp hi
+  apply And.intro
+  conv =>
+    rhs
+    arg 1
+    rw [←hi]
+    rfl
+    tactic => exact hp
+  exact hp
+
+def test_conv_unshielded : TestM Unit := do
+  let rootTarget ← parseSentence "∀ (p : Prop) (x y z : Nat), p → (p → x = y) → x + z = y + z ∧ p"
+  let state ← GoalState.create rootTarget
+  let tactic := "intro p x y z hp hi"
+  let .success state _ ← state.tacticOn 0 tactic | fail "intro failed"
+  let tactic := "apply And.intro"
+  let .success state _ ← state.tacticOn 0 tactic | fail "apply failed"
+  let .success state _ ← state.convEnter (.prefer state.goals[0]!) | fail "Cannot enter conversion tactic mode"
+  let .success state _ ← state.tryTactic .unfocus "rhs" | fail "rhs failed"
+  let tactic := "arg 1"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      { interiorGoal [] "y" with fragment := .conv },
+      { interiorGoal [] "p" with userName? := "right", },
+    ]
+  let tactic := "rw [←hi]"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" state.goals.length 3
+  let tactic := "rfl"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      interiorGoal [] "p",
+      { interiorGoal [] "p" with userName? := "right", },
+    ]
+  checkEq "(n goals)" state.goals.length 2
+  checkEq "(fragments)" state.fragments.size 0
+  let tactic := "exact hp"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  let tactic := "exact hp"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  let root? := state.rootExpr?
+  checkTrue "root" root?.isSome
+  where
+  interiorGoal (free: List (String × String)) (target: String) :=
+    let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free
+    buildGoal free target
+
+example : ∀ (x y z w : Nat), y = z → x + z = w → x + y = w := by
+  intro x y z w hyz hxzw
+  conv =>
+    lhs
+    arg 2
+    rw [hyz]
+    rfl
+  exact hxzw
+
+def test_conv_unfinished : TestM Unit := do
+  let rootTarget ← parseSentence "∀ (x y z w : Nat), y = z → x + z = w → x + y = w"
+  let state ← GoalState.create rootTarget
+  let tactic := "intro x y z w hyz hxzw"
+  let .success state _ ← state.tacticOn 0 tactic | fail "intro failed"
+  let convParent := state.goals[0]!
+  let .success state _ ← state.convEnter (.prefer convParent) | fail "Cannot enter conversion tactic mode"
+  let .success state _ ← state.tryTactic .unfocus "lhs" | fail "rhs failed"
+  let tactic := "arg 2"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      { interiorGoal [] "y" with fragment := .conv },
+    ]
+  let tactic := "rw [hyz]"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      { interiorGoal [] "z" with fragment := .conv },
+    ]
+  checkTrue "  (fragment)" $ state.fragments.contains state.mainGoal?.get!
+  checkTrue "  (fragment parent)" $ state.fragments.contains convParent
+  checkTrue "  (main goal)" state.mainGoal?.isSome
+  let tactic := "rfl"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      interiorGoal [] "x + z = w",
+    ]
+  checkEq "(fragments)" state.fragments.size 0
+  checkEq s!"  {tactic}" state.goals.length 1
+  let tactic := "exact hxzw"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  let root? := state.rootExpr?
+  checkTrue "root" root?.isSome
+  where
+  interiorGoal (free: List (String × String)) (target: String) :=
+    let free := [("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("w", "Nat"), ("hyz", "y = z"), ("hxzw", "x + z = w")] ++ free
+    buildGoal free target
+
+example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
+  intro a b c d h1 h2
+  calc a + b = b + c := by apply h1
+    _ = c + d := by apply h2
+
+def test_calc: TestM Unit := do
+  let rootTarget ← parseSentence "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d"
+  let state0 ← GoalState.create rootTarget
+  let tactic := "intro a b c d h1 h2"
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
+    #[interiorGoal [] "a + b = c + d"])
+  let pred := "a + b = b + c"
+  let .success state1 _ ← state1.calcEnter state1.mainGoal?.get! | fail "Could not enter calc"
+  let state2 ← match ← state1.tacticOn 0 pred with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[
+      { interiorGoal [] "a + b = b + c" with userName? := .some "calc" },
+      { interiorGoal [] "b + c = c + d" with fragment := .calc },
+    ])
+  addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
+  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
+
+  let tactic := "apply h1"
+  let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state3 ← match state2m.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+  let pred := "_ = c + d"
+  let state4 ← match ← state3.tacticOn 0 pred with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals).map (·.devolatilize) =
+    #[
+      { interiorGoal [] "b + c = c + d" with userName? := .some "calc" },
+    ])
+  addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
+  let tactic := "apply h2"
+  let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  checkEq "(fragments)" state4m.fragments.size 0
+  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
+  where
+    interiorGoal (free: List (String × String)) (target: String) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
+        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
+      buildGoal free target
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("conv simple", test_conv_simple),
+    ("conv unshielded", test_conv_unshielded),
+    ("conv unfinished", test_conv_unfinished),
+    ("calc", test_calc),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Fragment

doc/repl.md

@@ -13,7 +13,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   only the values of definitions are printed.
 * `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
   current environment to/from a file
-* `env.module_read { "module": <name }`: Reads a list of symbols from a module
+* `env.module_read { "module": <name> }`: Reads a list of symbols from a module
 * `env.describe {}`: Describes the imports and modules in the current environment
 * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
   have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
@@ -28,16 +28,19 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
 * `options.print`: Display the current set of options
 * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
   Start a new proof from a given expression or symbol
-* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
+* `goal.tactic {"stateId": <id>, ["goalId": <id>], ["autoResume": <bool>], ...}`:
-  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
+  Execute a tactic string on a given goal site. The tactic is supplied as additional
-  - `{ "tactic": <tactic> }`: Execute an ordinary tactic
+  key-value pairs in one of the following formats:
-  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
+  - `{ "tactic": <tactic> }`: Executes a tactic in the current mode
-  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
+  - `{ "mode": <mode> }`: Enter a different tactic mode. The permitted values
-  - `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
+    are `tactic` (default), `conv`, `calc`. In case of `calc`, each step must
     be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
     to the previous `rhs`.
-  - `{ "conv": <bool> }`: Enter or exit conversion tactic mode.
+  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
-  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
+  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
+  - `{ "let": <expr>, "binderName": <name> }`: Execute `let` and creates a branch goal
+  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into
+    goals. Coupling is not allowed.
   If the `goals` field does not exist, the tactic execution has failed. Read
   `messages` to find the reason.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: