From 5adf21ae0a33d0c496538a422b6894336136f0b7 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Sat, 13 Jan 2024 17:48:00 +1100
Subject: [PATCH] feat: report sorries in tactic mode

---
 REPL/JSON.lean                      | 14 ++++++++++++--
 REPL/Main.lean                      | 20 +++++++++++++++++++-
 REPL/Snapshots.lean                 |  6 ++++++
 test/tactic_mode_sorry.expected.out | 14 ++++++++++++++
 test/tactic_mode_sorry.in           |  3 +++
 5 files changed, 54 insertions(+), 3 deletions(-)
 create mode 100644 test/tactic_mode_sorry.expected.out
 create mode 100644 test/tactic_mode_sorry.in

diff --git a/REPL/JSON.lean b/REPL/JSON.lean
index ad0a0e3..bf3e5bf 100644
--- a/REPL/JSON.lean
+++ b/REPL/JSON.lean
@@ -68,7 +68,15 @@ structure Sorry where
   You can use the `ProofStep` instruction to run a tactic at this state.
   -/
   proofState : Option Nat
-deriving ToJson, FromJson
+deriving FromJson
+
+instance : ToJson Sorry where
+  toJson r := Json.mkObj <| .join [
+    [("goal", r.goal)],
+    [("proofState", toJson r.proofState)],
+    if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [],
+    if r.endPos.line ≠ 0 then [("endPos", toJson r.endPos)] else [],
+  ]
 
 /-- Construct the JSON representation of a Lean sorry. -/
 def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry :=
@@ -124,13 +132,15 @@ structure ProofStepResponse where
   proofState : Nat
   goals : List String
   messages : List Message := []
+  sorries : List Sorry := []
 deriving ToJson, FromJson
 
 instance : ToJson ProofStepResponse where
   toJson r := Json.mkObj <| .join [
     [("proofState", r.proofState)],
     [("goals", toJson r.goals)],
-    Json.nonemptyList "messages" r.messages
+    Json.nonemptyList "messages" r.messages,
+    Json.nonemptyList "sorries" r.sorries
   ]
 
 /-- Json wrapper for an error. -/
diff --git a/REPL/Main.lean b/REPL/Main.lean
index 2940d07..9900f61 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -128,8 +128,26 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
     M m ProofStepResponse := do
   let messages := proofState.newMessages old?
   let messages ← messages.mapM fun m => Message.of m
+  let trees := proofState.newInfoTrees old?
+  let trees := match old? with
+  | some old =>
+    let ctx : ContextInfo :=
+    { env := old.coreState.env
+      ngen := old.coreState.ngen
+      fileMap := old.coreContext.fileMap
+      options := old.coreContext.options
+      currNamespace := old.coreContext.currNamespace
+      openDecls := old.coreContext.openDecls
+      mctx := old.metaState.mctx }
+    trees.map fun t => InfoTree.context ctx t
+  | none => trees
+  let sorries ← sorries trees
   let id ← recordProofSnapshot proofState
-  return { proofState := id, goals := (← proofState.ppGoals).map fun s => s!"{s}", messages }
+  return {
+    proofState := id
+    goals := (← proofState.ppGoals).map fun s => s!"{s}"
+    messages
+    sorries }
 
 /-- Pickle an `CommandSnapshot`, generating a JSON response. -/
 def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do
diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index fddd6da..0228797 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -118,6 +118,12 @@ def newMessages (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : Li
   | none => new.coreState.messages.msgs.toList
   | some old => new.coreState.messages.msgs.toList.drop (old.coreState.messages.msgs.size)
 
+/-- New info trees in a `ProofSnapshot`, relative to an optional previous `ProofSnapshot`. -/
+def newInfoTrees (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : List InfoTree :=
+  match old? with
+  | none => new.coreState.infoState.trees.toList
+  | some old => new.coreState.infoState.trees.toList.drop (old.coreState.infoState.trees.size)
+
 /-- Run a `CoreM` monadic function in the current `ProofSnapshot`, updating the `Core.State`. -/
 def runCoreM (p : ProofSnapshot) (t : CoreM α) : IO (α × ProofSnapshot) := do
   let (a, coreState) ← (Lean.Core.CoreM.toIO · p.coreContext p.coreState) do t
diff --git a/test/tactic_mode_sorry.expected.out b/test/tactic_mode_sorry.expected.out
new file mode 100644
index 0000000..d0135f4
--- /dev/null
+++ b/test/tactic_mode_sorry.expected.out
@@ -0,0 +1,14 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 18},
+   "goal": "⊢ Nat",
+   "endPos": {"line": 1, "column": 23}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 5},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"sorries": [{"proofState": 1, "goal": "⊢ Nat"}], "proofState": 2, "goals": []}
+
diff --git a/test/tactic_mode_sorry.in b/test/tactic_mode_sorry.in
new file mode 100644
index 0000000..32465b9
--- /dev/null
+++ b/test/tactic_mode_sorry.in
@@ -0,0 +1,3 @@
+{"cmd": "def f : Nat := by sorry"}
+
+{"proofState": 0, "tactic": "sorry"}