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

feat: Prevent crash during rootExpr call

This commit is contained in:
Leni Aniva 2024-01-30 17:22:20 -08:00
parent 6d22841a27
commit 5720c72515
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Pantograph/Goal.lean
View File

@ -210,8 +210,8 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
else else
target.resume (goals := branch.goals) target.resume (goals := branch.goals)
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
let expr := goalState.mctx.eAssignment.find! goalState.root let expr ← goalState.mctx.eAssignment.find? goalState.root
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
if expr.hasMVar then if expr.hasMVar then
-- Must not assert that the goal state is empty here. We could be in a branch goal. -- Must not assert that the goal state is empty here. We could be in a branch goal.
@ -219,7 +219,7 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
.none .none
else else
assert! goalState.goals.isEmpty assert! goalState.goals.isEmpty
.some expr return expr
protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
let parent ← goalState.parentMVar let parent ← goalState.parentMVar
let expr := goalState.mctx.eAssignment.find! parent let expr := goalState.mctx.eAssignment.find! parent

6
Test/Proofs.lean
View File

@ -210,6 +210,8 @@ def proof_or_comm: TestM Unit := do
| .none => do | .none => do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
| .success state => pure state | .success state => pure state
@ -218,6 +220,8 @@ def proof_or_comm: TestM Unit := do
return () return ()
addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]) #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
| .success state => pure state | .success state => pure state
| other => do | other => do
@ -225,6 +229,8 @@ def proof_or_comm: TestM Unit := do
return () return ()
addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[branchGoal "inl" "p", branchGoal "inr" "q"]) #[branchGoal "inl" "p", branchGoal "inr" "q"])
addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state | .success state => pure state