From 736e68639fed25fea192575f2661acf1e9e126f2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 7 Nov 2023 13:07:50 -0800
Subject: [PATCH] fix: New goal state not inserted correctly

---
 Pantograph.lean       |  8 +++++---
 Test/Integration.lean | 19 +++++++++++++++++--
 2 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index 0ae8192..2532d75 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -54,7 +54,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
     let state ← get
     let nGoals := state.goalStates.size
-    set { state with goalStates := Lean.HashMap.empty }
+    set { state with nextId := 0, goalStates := Lean.HashMap.empty }
     return .ok { nGoals }
   stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
     let state ← get
@@ -163,8 +163,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       | .error error => return .error error
       | .ok (.success nextGoalState) =>
         let nextStateId := state.nextId
-        let goalStates := state.goalStates.insert state.nextId goalState
-        set { state with goalStates, nextId := state.nextId + 1 }
+        set { state with
+          goalStates := state.goalStates.insert state.nextId nextGoalState,
+          nextId := state.nextId + 1,
+        }
         let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
         return .ok {
           nextStateId? := .some nextStateId,
diff --git a/Test/Integration.lean b/Test/Integration.lean
index d8570b0..65c2da6 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -83,11 +83,19 @@ def test_malformed_command : IO LSpec.TestSeq :=
       Protocol.InteractionError))
   ]
 def test_tactic : IO LSpec.TestSeq :=
-  let goal: Protocol.Goal := {
+  let goal1: Protocol.Goal := {
     name := "_uniq.10",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
     vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
   }
+  let goal2: Protocol.Goal := {
+    name := "_uniq.13",
+    target := { pp? := .some "x ∨ y → y ∨ x" },
+    vars := #[
+      { name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
+      { name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
+    ],
+  }
   subroutine_runner [
     subroutine_step "goal.start"
       [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
@@ -97,7 +105,14 @@ def test_tactic : IO LSpec.TestSeq :=
       [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      (Lean.toJson ({
        nextStateId? := .some 1,
-       goals? := #[goal],
+       goals? := #[goal1],
+     }:
+      Protocol.GoalTacticResult)),
+    subroutine_step "goal.tactic"
+      [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
+     (Lean.toJson ({
+       nextStateId? := .some 2,
+       goals? := #[goal2],
      }:
       Protocol.GoalTacticResult))
   ]