aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 2 Packages Projects Releases Wiki Activity

fix(goal): Restore elaboration monad

This commit is contained in:
Leni Aniva 2025-06-30 14:52:38 -07:00
parent 2a87ed2e46
commit 8857b88d9a
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Pantograph/Goal.lean
View File

@ -507,7 +507,8 @@ protected def GoalState.tryTacticM
(state: GoalState) (site : Site) (state: GoalState) (site : Site)
(tacticM: Elab.Tactic.TacticM Unit) (tacticM: Elab.Tactic.TacticM Unit)
(guardMVarErrors : Bool := false) (guardMVarErrors : Bool := false)
: Elab.TermElabM TacticResult := : Elab.TermElabM TacticResult := do
state.restoreElabM
withCapturingError do withCapturingError do
state.step site tacticM guardMVarErrors state.step site tacticM guardMVarErrors
@ -567,6 +568,7 @@ protected def GoalState.convEnter (state : GoalState) (site : Site) :
let .some goal := state.actingGoal? site | throwNoGoals let .some goal := state.actingGoal? site | throwNoGoals
if let .some (.conv ..) := state.fragments[goal]? then if let .some (.conv ..) := state.fragments[goal]? then
return .invalidAction "Already in conv state" return .invalidAction "Already in conv state"
state.restoreElabM
withCapturingError do withCapturingError do
let (fragments, state') ← state.step' site Fragment.enterConv let (fragments, state') ← state.step' site Fragment.enterConv
return { return {
@ -582,6 +584,7 @@ protected def GoalState.fragmentExit (state : GoalState) (site : Site):
let .some goal := state.actingGoal? site | throwNoGoals let .some goal := state.actingGoal? site | throwNoGoals
let .some fragment := state.fragments[goal]? | let .some fragment := state.fragments[goal]? |
return .invalidAction "Goal does not have a fragment" return .invalidAction "Goal does not have a fragment"
state.restoreElabM
withCapturingError do withCapturingError do
let (fragments, state') ← state.step' goal (fragment.exit goal state.fragments) let (fragments, state') ← state.step' goal (fragment.exit goal state.fragments)
return { return {
@ -599,6 +602,7 @@ protected def GoalState.calcEnter (state : GoalState) (site : Site)
let .some goal := state.actingGoal? site | throwNoGoals let .some goal := state.actingGoal? site | throwNoGoals
if let .some _ := state.fragments[goal]? then if let .some _ := state.fragments[goal]? then
return .invalidAction "Goal already has a fragment" return .invalidAction "Goal already has a fragment"
state.restoreElabM
withCapturingError do withCapturingError do
let fragment := Fragment.enterCalc let fragment := Fragment.enterCalc
let fragments := state.fragments.insert goal fragment let fragments := state.fragments.insert goal fragment