feat: Goal continuation fails if target has goals
This commit is contained in:
parent
db706070ad
commit
d809a960f9
|
@ -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)
|
||||
|
|
|
@ -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 ()
|
||||
|
||||
|
||||
|
|
Loading…
Reference in New Issue