feat: Add goal.continue command

This commit is contained in:
Leni Aniva 2023-11-04 15:51:09 -07:00
parent 333355a85d
commit 97d658cfc5
2 changed files with 40 additions and 0 deletions

View File

@ -38,6 +38,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| "options.print" => run options_print | "options.print" => run options_print
| "goal.start" => run goal_start | "goal.start" => run goal_start
| "goal.tactic" => run goal_tactic | "goal.tactic" => run goal_tactic
| "goal.continue" => run goal_continue
| "goal.delete" => run goal_delete | "goal.delete" => run goal_delete
| "goal.print" => run goal_print | "goal.print" => run goal_print
| cmd => | cmd =>
@ -170,6 +171,30 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .error $ errorIndex s!"Invalid goal id index {goalId}" return .error $ errorIndex s!"Invalid goal id index {goalId}"
| .ok (.failure messages) => | .ok (.failure messages) =>
return .ok { tacticErrors? := .some messages } return .ok { tacticErrors? := .some messages }
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
let state ← get
match state.goalStates.get? args.target with
| .none => return .error $ errorIndex s!"Invalid state index {args.target}"
| .some target => do
let nextState? ← match args.branch?, args.goals? with
| .some branchId, .none => do
match state.goalStates.get? branchId with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .none, .some goals =>
let goals := goals.map (λ name => { name := str_to_name name })
pure $ target.resume goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
match nextState? with
| .error error => return .ok { error? := .some error }
| .ok nextGoalState =>
let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
set { state with goalStates }
let goals ← nextGoalState.serializeGoals (parent := .some target) (options := state.options)
return .ok {
nextStateId? := .some nextStateId,
goals? := .some goals,
}
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
let state ← get let state ← get
let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates

View File

@ -163,6 +163,21 @@ structure GoalTacticResult where
-- Existence of this field shows the tactic parsing has failed -- Existence of this field shows the tactic parsing has failed
parseError?: Option String := .none parseError?: Option String := .none
deriving Lean.ToJson deriving Lean.ToJson
structure GoalContinue where
-- State from which the continuation acquires the context
target: Nat
-- One of the following must be supplied
-- The state which is an ancestor of `target` where goals will be extracted from
branch?: Option Nat := .none
-- Or, the particular goals that should be brought back into scope
goals?: Option (List String) := .none
deriving Lean.FromJson
structure GoalContinueResult where
error?: Option String := .none
nextStateId?: Option Nat := .none
goals?: Option (Array Goal) := .none
deriving Lean.ToJson
-- Remove goal states -- Remove goal states
structure GoalDelete where structure GoalDelete where