feat: Expose GoalState functions #94

Merged
aniva merged 5 commits from lib/export into dev 2024-09-08 12:10:47 -07:00
3 changed files with 8 additions and 13 deletions
Showing only changes of commit 02556f3c79 - Show all commits

View File

@ -164,7 +164,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .some branchId, .none => do | .some branchId, .none => do
match state.goalStates.find? branchId with match state.goalStates.find? branchId with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}" | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ goalContinue target branch | .some branch => pure $ target.continue branch
| .none, .some goals => | .none, .some goals =>
pure $ goalResume target goals pure $ goalResume target goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"

View File

@ -39,15 +39,15 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
--Elab.Term.synthesizeSyntheticMVarsNoPostponing --Elab.Term.synthesizeSyntheticMVarsNoPostponing
--let expr ← instantiateMVars expr --let expr ← instantiateMVars expr
let goal ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous) let root ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
let root := goal.mvarId! let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root.mvarId!]}
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
return { return {
root, root := root.mvarId!,
savedState, savedState,
parentMVar? := .none, parentMVar? := .none,
} }
@[export pantograph_goal_state_is_conv]
protected def GoalState.isConv (state: GoalState): Bool := protected def GoalState.isConv (state: GoalState): Bool :=
state.convMVar?.isSome state.convMVar?.isSome
protected def GoalState.goals (state: GoalState): List MVarId := protected def GoalState.goals (state: GoalState): List MVarId :=
@ -56,6 +56,7 @@ protected def GoalState.goals (state: GoalState): List MVarId :=
protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
protected def GoalState.mctx (state: GoalState): MetavarContext := protected def GoalState.mctx (state: GoalState): MetavarContext :=
state.savedState.term.meta.meta.mctx state.savedState.term.meta.meta.mctx
@[export pantograph_goal_state_env]
protected def GoalState.env (state: GoalState): Environment := protected def GoalState.env (state: GoalState): Environment :=
state.savedState.term.meta.core.env state.savedState.term.meta.core.env
@ -85,7 +86,7 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
state.savedState.restore state.savedState.restore
Elab.Tactic.setGoals [goal] Elab.Tactic.setGoals [goal]
@[export pantograph_goal_state_focus]
protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
let goal ← state.savedState.tactic.goals.get? goalId let goal ← state.savedState.tactic.goals.get? goalId
return { return {
@ -121,6 +122,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
/-- /--
Brings into scope all goals from `branch` Brings into scope all goals from `branch`
-/ -/
@[export pantograph_goal_state_continue]
protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState := protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
if !target.goals.isEmpty then if !target.goals.isEmpty then
.error s!"Target state has unresolved goals" .error s!"Target state has unresolved goals"

View File

@ -134,10 +134,6 @@ def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR Goal
def goalResume (target: GoalState) (goals: Array String): Except String GoalState := def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
target.resume (goals.map (λ n => { name := n.toName }) |>.toList) target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
@[export pantograph_goal_continue]
def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
target.continue branch
@[export pantograph_goal_serialize_m] @[export pantograph_goal_serialize_m]
def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) := def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options runMetaM <| state.serializeGoals (parent := .none) options
@ -189,8 +185,5 @@ def goalConvExit (state: GoalState): CoreM TacticResult :=
@[export pantograph_goal_calc_m] @[export pantograph_goal_calc_m]
def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult := def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult :=
runTermElabM <| state.tryCalc goalId pred runTermElabM <| state.tryCalc goalId pred
@[export pantograph_goal_focus]
def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
state.focus goalId
end Pantograph end Pantograph