aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

fix: Capture nested tactic failure #135

Merged
aniva merged 6 commits from bug/nested-tactic-failure into dev 2024-12-07 18:51:26 -08:00
Conversation 1 Commits 6 Files Changed 7 +10 -3
1 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 929311a042 - Show all commits

13
Pantograph/Goal.lean
View File

@ -202,12 +202,19 @@ inductive TacticResult where
-- The given action cannot be executed in the state -- The given action cannot be executed in the state
| invalidAction (message: String) | invalidAction (message: String)
/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/ /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit): protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
try try
let nextState ← state.step goal tacticM let nextState ← state.step goal tacticM
let newMessages ← (← getThe Core.State).messages.toList.drop (state.coreState.messages.toList.length) |>.mapM λ m => m.toString
-- Check if error messages have been generated in the core.
let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length
|>.filterMapM λ m => do
if m.severity == .error then
return .some $ ← m.toString
else
return .none
if ¬ newMessages.isEmpty then if ¬ newMessages.isEmpty then
return .failure newMessages.toArray return .failure newMessages.toArray
return .success nextState return .success nextState
@ -357,7 +364,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}" throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
if let some prevRhs := calcPrevRhs? then if let some prevRhs := calcPrevRhs? then
unless ← Meta.isDefEqGuarded lhs prevRhs do unless ← Meta.isDefEqGuarded lhs prevRhs do
throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- " throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}"
-- Creates a mvar to represent the proof that the calc tactic solves the -- Creates a mvar to represent the proof that the calc tactic solves the
-- current branch -- current branch