From d809a960f99e339f0849c2c8a1fec76ceb3c3976 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 4 Nov 2023 15:53:57 -0700
Subject: [PATCH] feat: Goal continuation fails if target has goals

---
 Pantograph/Goal.lean | 4 +++-
 Test/Holes.lean      | 5 +++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index fd24232..3645087 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -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)
diff --git a/Test/Holes.lean b/Test/Holes.lean
index 8692c2a..b6647ef 100644
--- a/Test/Holes.lean
+++ b/Test/Holes.lean
@@ -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 ()