From 51edc701fe18806cdc3f4860d9ef442a1c9abcf4 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 24 Aug 2023 23:12:18 -0700
Subject: [PATCH] Add test cases for command error categories

---
 Test/Integration.lean | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/Test/Integration.lean b/Test/Integration.lean
index 83cdb70..ab31110 100644
--- a/Test/Integration.lean
+++ b/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))
   ]