Pantograph/Goal.lean

@@ -565,7 +565,7 @@ protected def GoalState.tryLet (state : GoalState) (site : Site) (binderName : S
 
 /-- Enter conv tactic mode -/
 @[export pantograph_goal_state_conv_enter_m]
-protected def GoalState.conv (state : GoalState) (site : Site) :
+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
@@ -578,13 +578,13 @@ protected def GoalState.conv (state : GoalState) (site : Site) :
         acc.insert goal fragment
     }
 
-/-- Exit from `conv` mode, and conclude all conversion tactic sentinels
+/-- Exit from a tactic fragment. -/
-descended from `goal`. -/
+@[export pantograph_goal_state_fragment_exit_m]
-@[export pantograph_goal_state_conv_exit_m]
+protected def GoalState.fragmentExit (state : GoalState) (site : Site):
-protected def GoalState.convExit (state : GoalState) (goal : MVarId):
       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 {
@@ -596,19 +596,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) (site : Site) (pred : String)
+protected def GoalState.calcEnter (state : GoalState) (site : Site)
   : Elab.TermElabM TacticResult := do
   let .some goal := state.actingGoal? site | throwNoGoals
-  let prevRhs? := state.calcPrevRhsOf? goal
+  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

@@ -158,26 +158,26 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bo
   }
 
 @[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

@@ -87,6 +87,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 +249,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

Pantograph/Tactic/Fragment.lean

@@ -33,8 +33,7 @@ protected def Fragment.map (fragment : Fragment) (mapExpr : Expr → CoreM Expr)
   | .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
   let goal ← Elab.Tactic.getMainGoal
   goal.checkNotAssigned `GoalState.conv

Repl.lean

@@ -108,6 +108,73 @@ structure CompilationUnit where
   messages : Array String
   newConstants : List Name
 
+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 }
+
 def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
   let options := (← getMainState).options
   let (fileName, file) ← match args.fileName?, args.file? with
@@ -225,7 +292,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 +356,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,72 +365,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 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 }
   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 })
@@ -387,7 +395,7 @@ 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)
@@ -399,7 +407,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/Proofs.lean

@@ -328,7 +328,7 @@ def test_conv: TestM Unit := do
     #[interiorGoal [] "a + b + c1 = b + a + c2"])
 
   let goalConv := state1.goals[0]!
-  let state2 ← match ← state1.conv (state1.get! 0) with
+  let state2 ← match ← state1.convEnter (state1.get! 0) with
     | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -399,7 +399,7 @@ def test_conv: TestM Unit := do
   addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[])
 
-  let state1_1 ← match ← state6.convExit goalConv with
+  let state1_1 ← match ← state6.fragmentExit goalConv with
     | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -441,7 +441,8 @@ def test_calc: TestM Unit := do
   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
+  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
@@ -466,7 +467,7 @@ def test_calc: TestM Unit := do
       addTest $ expectationFailure "continue" e
       return ()
   let pred := "_ = c + d"
-  let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
+  let state4 ← match ← state3.tacticOn 0 pred with
     | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString