From 22202af24e2367de5c51190997d4caf724c617bb Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 May 2023 14:56:43 -0700
Subject: [PATCH] Add option id handling with ?

---
 Main.lean                | 12 +++++-------
 Pantograph/Commands.lean |  2 +-
 Pantograph/Meta.lean     |  2 +-
 Test/Proofs.lean         |  2 +-
 4 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/Main.lean b/Main.lean
index e1e87e6..fcb2190 100644
--- a/Main.lean
+++ b/Main.lean
@@ -20,8 +20,6 @@ structure State where
 -- State monad
 abbrev Subroutine := ReaderT Context (StateT State IO)
 
-def nextId (s: State): Nat := s.environments.size
-
 def State.getEnv (state: State) (id: Nat): Except String Lean.Environment :=
   match state.environments.get? id with
   | .some env => return env
@@ -92,7 +90,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
   errorIndex (s: String) := Lean.toJson ({ error := "index", desc := s }: InteractionError)
   create (args: Create): Subroutine Lean.Json := do
     let state ← get
-    let id := nextId state
+    let id := state.environments.size
     let env ← Lean.importModules
       (imports := args.imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
       (opts := {})
@@ -172,9 +170,9 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
     | .error error => return error
     | .ok tree =>
       -- Put the new tree in the environment
-      let nextId := state.proofTrees.size
+      let nextTreeId := state.proofTrees.size
       set { state with proofTrees := state.proofTrees.push tree }
-      return Lean.toJson ({ treeId := nextId }: ProofStartResult)
+      return Lean.toJson ({ treeId := nextTreeId }: ProofStartResult)
   proof_tactic (args: ProofTactic): Subroutine Lean.Json := do
     let state ← get
     match state.proofTrees.get? args.treeId with
@@ -186,9 +184,9 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
         (tactic := args.tactic) |>.run tree
       match result with
       | .invalid message => return Lean.toJson <| errorIndex message
-      | .success nextId goals =>
+      | .success nextId? goals =>
         set { state with proofTrees := state.proofTrees.set! args.treeId nextTree }
-        return Lean.toJson ({ nextId := nextId, goals := goals }: ProofTacticResultSuccess)
+        return Lean.toJson ({ nextId? := nextId?, goals := goals }: ProofTacticResultSuccess)
       | .failure messages =>
         return Lean.toJson ({ errorMessages := messages }: ProofTacticResultFailure)
   proof_print_tree (args: ProofPrintTree): Subroutine Lean.Json := do
diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean
index 5bdf4fd..d90715a 100644
--- a/Pantograph/Commands.lean
+++ b/Pantograph/Commands.lean
@@ -68,7 +68,7 @@ structure ProofTactic where
   deriving Lean.FromJson
 structure ProofTacticResultSuccess where
   goals: Array String
-  nextId: Option Nat
+  nextId?: Option Nat
   deriving Lean.ToJson
 structure ProofTacticResultFailure where
   errorMessages: Array String -- Error messages generated by tactic
diff --git a/Pantograph/Meta.lean b/Pantograph/Meta.lean
index 486f937..e0216a6 100644
--- a/Pantograph/Meta.lean
+++ b/Pantograph/Meta.lean
@@ -136,7 +136,7 @@ inductive TacticResult where
   -- Invalid id
   | invalid (message: String): TacticResult
   -- Goes to next state
-  | success (nextId: Option Nat) (goals: Array String)
+  | success (nextId?: Option Nat) (goals: Array String)
   -- Fails with messages
   | failure (messages: Array String)
 
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index f145a27..f422dc4 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -120,7 +120,7 @@ def proof_or_comm: IO LSpec.TestSeq := do
   ]
 
 def test_proofs : IO LSpec.TestSeq := do
-  return LSpec.group "proofs" $
+  return LSpec.group "Proofs" $
     (LSpec.group "Nat.add_comm" $ (← proof_nat_add_comm)) ++
     (LSpec.group "Nat.add_comm manual" $ (← proof_nat_add_comm_manual)) ++
     (LSpec.group "Or.comm" $ (← proof_or_comm))