feat: Goal continuation fails if target has goals

This commit is contained in:
Leni Aniva 2023-11-04 15:53:57 -07:00
parent 97d658cfc5
commit 4be9dbc84a
2 changed files with 8 additions and 1 deletions

View File

@ -192,7 +192,9 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
Brings into scope all goals from `branch`
-/
protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
if target.root != branch.root then
if !target.goals.isEmpty then
.error s!"Target state has unresolved goals"
else if target.root != branch.root then
.error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
else
target.resume (goals := branch.goals)

View File

@ -133,6 +133,7 @@ def test_proposition_generation: TestM Unit := do
return ()
addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
#[])
addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
return ()
@ -175,6 +176,10 @@ def test_partial_continuation: TestM Unit := do
match state0.resume coupled_goals with
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
| .ok _ => addTest $ assertUnreachable "(continuation failure)"
-- Continuation should fail if some goals have not been solved
match state2.continue state1 with
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Target state has unresolved goals")
| .ok _ => addTest $ assertUnreachable "(continuation failure)"
return ()