From 85440e02783cbc4f1d514d07b88730805b3ba593 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 23 Aug 2023 13:00:11 -0700
Subject: [PATCH] Unify json and unknown error into command error

---
 Main.lean             |  2 +-
 Pantograph.lean       |  2 +-
 Test/Integration.lean | 14 ++++++++++++--
 3 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/Main.lean b/Main.lean
index 10fc6b0..99ec70b 100644
--- a/Main.lean
+++ b/Main.lean
@@ -13,7 +13,7 @@ unsafe def loop : MainM Unit := do
   if command.trim.length = 0 then return ()
   match parse_command command with
   | .error error =>
-    let error  := Lean.toJson ({ error := "json", desc := error }: Commands.InteractionError)
+    let error  := Lean.toJson ({ error := "command", desc := error }: Commands.InteractionError)
     -- Using `Lean.Json.compress` here to prevent newline
     IO.println error.compress
   | .ok command =>
diff --git a/Pantograph.lean b/Pantograph.lean
index e3501aa..d37f7ef 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -55,7 +55,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
   | "proof.printTree" => run proof_print_tree
   | cmd =>
     let error: Commands.InteractionError :=
-      { error := "unknown", desc := s!"Unknown command {cmd}" }
+      { error := "command", desc := s!"Unknown command {cmd}" }
     return Lean.toJson error
   where
   errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
diff --git a/Test/Integration.lean b/Test/Integration.lean
index ae73d82..83cdb70 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -41,7 +41,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
   catch ex =>
     return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
 
-def test_option_print : IO LSpec.TestSeq :=
+def test_option_modify : IO LSpec.TestSeq :=
   let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
   let sexp? := Option.some "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"
   let module? := Option.some "Init.Data.Nat.Basic"
@@ -66,11 +66,21 @@ def test_option_print : IO LSpec.TestSeq :=
      (Lean.toJson ({ options with printExprAST := true }:
       Commands.OptionsPrintResult))
   ]
+def test_malformed_command : IO LSpec.TestSeq :=
+  let invalid := "invalid"
+  subroutine_runner [
+    subroutine_step invalid
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       error := "command", desc := s!"Unknown command {invalid}"}:
+      Commands.InteractionError))
+  ]
 
 def test_integration: IO LSpec.TestSeq := do
 
   return LSpec.group "Integration" $
-    (LSpec.group "Option modify" (← test_option_print))
+    (LSpec.group "Option modify" (← test_option_modify)) ++
+    (LSpec.group "Malformed command" (← test_malformed_command))
 
 
 end Pantograph.Test