Pantograph/Goal.lean

@@ -169,30 +169,34 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
       return .failure #[← exception.toMessageData.toString]
   tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
 
-/-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/
+/--
-protected def GoalState.continue (target: GoalState) (graftee: GoalState) (goals: Option (List MVarId) := .none): Except String GoalState :=
+Brings into scope a list of goals
-  let goals := match goals with
+-/
-    | .some goals => goals
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
-    | .none => target.goals
+  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
-  if target.root != graftee.root then
+    .error s!"Goals not in scope"
-    .error s!"Roots of two continued goal states do not match: {target.root.name} != {graftee.root.name}"
-  -- Ensure goals are not dangling
-  else if ¬ (goals.all (λ goal => graftee.mvars.contains goal)) then
-    .error s!"Some goals in target are not present in the graftee"
   else
     -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
     let unassigned := goals.filter (λ goal =>
-      let mctx := graftee.mctx
+      let mctx := state.mctx
       ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
     .ok {
+      state with
       savedState := {
-        term := graftee.savedState.term,
+        term := state.savedState.term,
         tactic := { goals := unassigned },
       },
-      root := target.root,
-      newMVars := graftee.newMVars,
     }
 
+/--
+Brings into scope all goals from `branch`
+-/
+protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  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)
+
 protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
   let expr := goalState.mctx.eAssignment.find! goalState.root
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)

Test/Holes.lean

@@ -85,7 +85,7 @@ def test_m_couple: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
-  let state1b ← match state1.continue state2 with
+  let state1b ← match state2.continue state1 with
     | .error msg => do
       addTest $ assertUnreachable $ msg
       return ()
@@ -136,6 +136,47 @@ def test_proposition_generation: TestM Unit := do
   addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
   return ()
 
+def test_partial_continuation: TestM Unit := do
+  let state? ← startProof "(2: Nat) ≤ 5"
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
+
+  let state2 ← match ← state1.execute (goalId := 2) (tactic := "apply Nat.succ") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "apply Nat.succ" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "Nat"])
+
+  -- Execute a partial continuation
+  let coupled_goals := state1.goals ++ state2.goals
+  let state1b ← match state2.resume (goals := coupled_goals) with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+
+  -- Continuation should fail if the state does not exist:
+  match state0.resume coupled_goals with
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
+  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
+  return ()
+
 
 def suite: IO LSpec.TestSeq := do
   let env: Lean.Environment ← Lean.importModules
@@ -144,7 +185,8 @@ def suite: IO LSpec.TestSeq := do
     (trustLevel := 1)
   let tests := [
     ("2 < 5", test_m_couple),
-    ("Proposition Generation", test_proposition_generation)
+    ("Proposition Generation", test_proposition_generation),
+    ("Partial Continuation", test_partial_continuation)
   ]
   let tests ← tests.foldlM (fun acc tests => do
     let (name, tests) := tests

Test/Proofs.lean

@@ -253,7 +253,7 @@ def proof_or_comm: TestM Unit := do
   addTest $ LSpec.check "  assumption" state4_2.goals.isEmpty
   addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
   -- Ensure the proof can continue from `state4_2`.
-  let state2b ← match state2.continue state4_2 with
+  let state2b ← match state4_2.continue state2 with
     | .error msg => do
       addTest $ assertUnreachable $ msg
       return ()