From db706070ad56bdbdcadf8d119259868258b18e20 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 4 Nov 2023 15:51:09 -0700
Subject: [PATCH] feat: Add goal.continue command

---
 Pantograph.lean          | 25 +++++++++++++++++++++++++
 Pantograph/Protocol.lean | 15 +++++++++++++++
 2 files changed, 40 insertions(+)

diff --git a/Pantograph.lean b/Pantograph.lean
index 00782d5..0984db8 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -38,6 +38,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   | "options.print"  => run options_print
   | "goal.start"     => run goal_start
   | "goal.tactic"    => run goal_tactic
+  | "goal.continue"  => run goal_continue
   | "goal.delete"    => run goal_delete
   | "goal.print"    => run goal_print
   | cmd =>
@@ -170,6 +171,30 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         return .error $ errorIndex s!"Invalid goal id index {goalId}"
       | .ok (.failure messages) =>
         return .ok { tacticErrors? := .some messages }
+  goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
+    let state ← get
+    match state.goalStates.get? args.target with
+    | .none => return .error $ errorIndex s!"Invalid state index {args.target}"
+    | .some target => do
+      let nextState? ← match args.branch?, args.goals? with
+        | .some branchId, .none => do
+          match state.goalStates.get? branchId with
+          | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
+          | .some branch => pure $ target.continue branch
+        | .none, .some goals =>
+          let goals := goals.map (λ name => { name := str_to_name name })
+          pure $ target.resume goals
+        | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
+      match nextState? with
+      | .error error => return .ok { error? := .some error }
+      | .ok nextGoalState =>
+        let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
+        set { state with goalStates }
+        let goals ← nextGoalState.serializeGoals (parent := .some target) (options := state.options)
+        return .ok {
+          nextStateId? := .some nextStateId,
+          goals? := .some goals,
+        }
   goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
     let state ← get
     let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index fd790bb..2469a6c 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -163,6 +163,21 @@ structure GoalTacticResult where
   -- Existence of this field shows the tactic parsing has failed
   parseError?: Option String := .none
   deriving Lean.ToJson
+structure GoalContinue where
+  -- State from which the continuation acquires the context
+  target: Nat
+
+  -- One of the following must be supplied
+  -- The state which is an ancestor of `target` where goals will be extracted from
+  branch?: Option Nat := .none
+  -- Or, the particular goals that should be brought back into scope
+  goals?: Option (List String) := .none
+  deriving Lean.FromJson
+structure GoalContinueResult where
+  error?: Option String := .none
+  nextStateId?: Option Nat := .none
+  goals?: Option (Array Goal) := .none
+  deriving Lean.ToJson
 
 -- Remove goal states
 structure GoalDelete where