From 95d26a2f50c2f397bbc91e16c768ae02b3418b5b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 24 Aug 2023 22:51:40 -0700
Subject: [PATCH] Classify JSON error as command error

Also add documentation for this
---
 Pantograph.lean |  5 +++--
 README.md       | 19 +++++++++++++++++--
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index 8a8e91a..18ead6b 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -27,7 +27,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
       match (← comm args) with
       | .ok result =>  return Lean.toJson result
       | .error ierror => return Lean.toJson ierror
-    | .error error => pure $ error
+    | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
   match command.cmd with
   | "reset"           => run reset
   | "expr.echo"       => run expr_echo
@@ -40,10 +40,11 @@ def execute (command: Commands.Command): MainM Lean.Json := do
   | "proof.printTree" => run proof_print_tree
   | cmd =>
     let error: Commands.InteractionError :=
-      { error := "command", desc := s!"Unknown command {cmd}" }
+      errorCommand s!"Unknown command {cmd}"
     return Lean.toJson error
   where
   errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
+  errorCommand := errorI "command"
   errorIndex := errorI "index"
   -- Command Functions
   reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do
diff --git a/README.md b/README.md
index f413d31..82d3db3 100644
--- a/README.md
+++ b/README.md
@@ -27,7 +27,7 @@ build/bin/pantograph MODULES|LEAN_OPTIONS
 ```
 
 The REPL loop accepts commands as single-line JSON inputs and outputs either an
-`Error:` (indicating malformed command) or a json return value indicating the
+`Error:` (indicating malformed command) or a JSON return value indicating the
 result of a command execution.  The command can be passed in one of two formats
 ```
 command { ... }
@@ -64,7 +64,7 @@ where the application of `assumption` should lead to a failure.
 
 ## Commands
 
-See `Pantograph/Commands.lean` for a description of the parameters and return values in Json.
+See `Pantograph/Commands.lean` for a description of the parameters and return values in JSON.
 - `reset`: Delete all cached expressions and proof trees
 - `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
 - `lib.catalog`: Display a list of all safe Lean symbols in the current context
@@ -78,6 +78,21 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
 - `proof.tactic {"treeId": <id>, "stateId": <id>, "goalId": <id>, "tactic": string}`: Execute a tactic on a given proof state
 - `proof.printTree {"treeId": <id>}`: Print the topological structure of a proof tree
 
+## Errors
+
+When an error pertaining to the execution of a command happens, the returning JSON structure is
+
+``` json
+{ error: "type", desc: "description" }
+```
+Common error forms:
+* `command`: Indicates malformed command structure which results from either
+  invalid command or a malformed JSON structure that cannot be fed to an
+  individual command.
+* `index`: Indicates an invariant maintained by the output of one command and
+  input of another is broken. For example, attempting to query a symbol not
+  existing in the library or indexing into a non-existent proof state.
+
 ## Troubleshooting
 
 If lean encounters stack overflow problems when printing catalog, execute this before running lean: