Separate max and imax in sort level

Reviewed-on: #11

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
@@ -133,7 +134,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
     match expr? with
     | .error error => return .error error
     | .ok expr =>
-      let tree ← ProofTree.create (str_to_name <| args.name.getD "Untitled") expr
+      let tree ← ProofTree.create expr
       -- Put the new tree in the environment
       let nextTreeId := state.proofTrees.size
       set { state with proofTrees := state.proofTrees.push tree }

Pantograph/Commands.lean

@@ -128,7 +128,6 @@ structure OptionsPrint where
 abbrev OptionsPrintResult := Options
 
 structure ProofStart where
-  name: Option String     -- Identifier of the proof
   -- Only one of the fields below may be populated.
   expr: Option String     -- Proof expression
   copyFrom: Option String -- Theorem name
@@ -140,7 +139,7 @@ structure ProofTactic where
   -- Identifiers for tree, state, and goal
   treeId: Nat
   stateId: Nat
-  goalId: Option Nat
+  goalId: Option Nat -- Defaults to 0
   tactic: String
   deriving Lean.FromJson
 structure ProofTacticResult where

Pantograph/Serial.lean

@@ -83,16 +83,20 @@ def serialize_sort_level_ast (level: Level): String :=
   let u_str := match u with
     | .zero => "0"
     | .succ _ => panic! "getLevelOffset should not return .succ"
-    | .max v w | .imax v w =>
+    | .max v w =>
       let v := serialize_sort_level_ast v
       let w := serialize_sort_level_ast w
-      s!"(max {v} {w})"
+      s!"(:max {v} {w})"
+    | .imax v w =>
+      let v := serialize_sort_level_ast v
+      let w := serialize_sort_level_ast w
+      s!"(:imax {v} {w})"
     | .param name =>
       let name := name_to_ast name
       s!"{name}"
     | .mvar id =>
       let name := name_to_ast id.name
-      s!"(:mvar {name})"
+      s!"(:mv {name})"
   match k, u with
   | 0, _ => u_str
   | _, .zero => s!"{k}"

Pantograph/Tactic.lean

@@ -30,21 +30,17 @@ structure ProofState where
   parent : Option Nat := none
   parentGoalId : Nat  := 0
 structure ProofTree where
-  -- All parameters needed to run a `TermElabM` monad
-  name: Name
-
   -- Set of proof states
   states : Array ProofState := #[]
 
 abbrev M := Elab.TermElabM
 
-def ProofTree.create (name: Name) (expr: Expr): M ProofTree := do
+def ProofTree.create (expr: Expr): M ProofTree := do
   let expr ← instantiateMVars expr
   let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic))
   let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
   let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
   return {
-    name := name,
     states := #[{
       savedState := savedState,
       goals := [goal.mvarId!]

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:

Test/Integration.lean

@@ -5,10 +5,12 @@ import Pantograph
 namespace Pantograph.Test
 open Pantograph
 
-def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
+def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
     (expected: Lean.Json): MainM LSpec.TestSeq := do
   let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
-  return LSpec.test s!"{cmd}" (toString result = toString expected)
+  return LSpec.test name (toString result = toString expected)
+def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
+    (expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected
 
 def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
   -- Setup the environment for execution
@@ -69,10 +71,15 @@ def test_option_modify : IO LSpec.TestSeq :=
 def test_malformed_command : IO LSpec.TestSeq :=
   let invalid := "invalid"
   subroutine_runner [
-    subroutine_step invalid
+    subroutine_named_step "Invalid command" invalid
       [("name", .str "Nat.add_one")]
      (Lean.toJson ({
        error := "command", desc := s!"Unknown command {invalid}"}:
+      Commands.InteractionError)),
+    subroutine_named_step "JSON Deserialization" "expr.echo"
+      [(invalid, .str "Random garbage data")]
+     (Lean.toJson ({
+       error := "command", desc := s!"Unable to parse json: Pantograph.Commands.ExprEcho.expr: String expected"}:
       Commands.InteractionError))
   ]
 

Test/Proofs.lean

@@ -22,7 +22,6 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
     match cInfo? with
     | .some cInfo =>
       let state ← ProofTree.create
-        (name := str_to_name "TestExample")
         (expr := cInfo.type)
       return (testSeq, Option.some state)
     | .none =>
@@ -43,7 +42,6 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
         return (testSeq, Option.none)
       | .ok expr =>
         let state ← ProofTree.create
-          (name := str_to_name "TestExample")
           (expr := expr)
         return (testSeq, Option.some state)