From 85440e02783cbc4f1d514d07b88730805b3ba593 Mon Sep 17 00:00:00 2001 From: Leni Aniva 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