feat: Automatic mode (auto resume)

This commit is contained in:
Leni Aniva 2024-09-06 21:30:11 -07:00
parent 82d99ccf9b
commit 37473b3efb
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 32 additions and 5 deletions

View File

@ -20,6 +20,7 @@ structure State where
/-- Main state monad for executing commands -/ /-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.CoreM) abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
-- certain monadic features in `MainM` -- certain monadic features in `MainM`
abbrev CR α := Except Protocol.InteractionError α abbrev CR α := Except Protocol.InteractionError α
@ -145,7 +146,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
pure $ Except.error $ error pure $ Except.error $ error
match nextGoalState? with match nextGoalState? with
| .error error => return .error error | .error error => return .error error
| .ok (.success nextGoalState) => | .ok (.success nextGoalState) => do
let nextGoalState ← match state.options.automaticMode, args.conv? with
| true, .none => do
let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals"
pure result
| true, .some true => pure nextGoalState
| true, .some false => do
let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail"
let .ok result := nextGoalState.resume dormantGoals | throwError "Resuming known goals"
pure result
| false, _ => pure nextGoalState
let nextStateId := state.nextId let nextStateId := state.nextId
set { state with set { state with
goalStates := state.goalStates.insert state.nextId nextGoalState, goalStates := state.goalStates.insert state.nextId nextGoalState,

View File

@ -27,7 +27,8 @@ structure GoalState where
parentMVar?: Option MVarId parentMVar?: Option MVarId
-- Existence of this field shows that we are currently in `conv` mode. -- Existence of this field shows that we are currently in `conv` mode.
convMVar?: Option (MVarId × MVarId) := .none -- (convRhs, goal, dormant)
convMVar?: Option (MVarId × MVarId × List MVarId) := .none
-- Previous RHS for calc, so we don't have to repeat it every time -- Previous RHS for calc, so we don't have to repeat it every time
-- WARNING: If using `state with` outside of `calc`, this must be set to `.none` -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
calcPrevRhs?: Option (MVarId × Expr) := .none calcPrevRhs?: Option (MVarId × Expr) := .none
@ -97,6 +98,20 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
calcPrevRhs? := .none, calcPrevRhs? := .none,
} }
/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
@[export pantograph_goal_state_immediate_resume_parent]
protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
-- Prune parents solved goals
let mctx := state.mctx
let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
{
state with
savedState := {
state.savedState with
tactic := { goals := state.goals ++ parentGoals },
},
}
/-- /--
Brings into scope a list of goals Brings into scope a list of goals
-/ -/
@ -116,7 +131,6 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
term := state.savedState.term, term := state.savedState.term,
tactic := { goals := unassigned }, tactic := { goals := unassigned },
}, },
calcPrevRhs? := .none,
} }
/-- /--
Brings into scope all goals from `branch` Brings into scope all goals from `branch`
@ -244,11 +258,13 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
return (← MonadBacktrack.saveState, convMVar) return (← MonadBacktrack.saveState, convMVar)
try try
let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-- Other goals are now dormant
let otherGoals := state.goals.filter $ λ g => g != goal
return .success { return .success {
root := state.root, root := state.root,
savedState := nextSavedState savedState := nextSavedState
parentMVar? := .some goal, parentMVar? := .some goal,
convMVar? := .some (convRhs, goal), convMVar? := .some (convRhs, goal, otherGoals),
calcPrevRhs? := .none calcPrevRhs? := .none
} }
catch exception => catch exception =>
@ -257,7 +273,7 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/ /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
protected def GoalState.convExit (state: GoalState): protected def GoalState.convExit (state: GoalState):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
let (convRhs, convGoal) ← match state.convMVar? with let (convRhs, convGoal, _) ← match state.convMVar? with
| .some mvar => pure mvar | .some mvar => pure mvar
| .none => return .invalidAction "Not in conv state" | .none => return .invalidAction "Not in conv state"
let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do