aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

Unify json and unknown error into command error

This commit is contained in:
Leni Aniva 2023-08-23 13:00:11 -07:00
parent 96cbbf2551
commit 0c330c8778
3 changed files with 14 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Main.lean
View File

@ -13,7 +13,7 @@ unsafe def loop : MainM Unit := do
if command.trim.length = 0 then return () if command.trim.length = 0 then return ()
match parse_command command with match parse_command command with
| .error error => | .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 -- Using `Lean.Json.compress` here to prevent newline
IO.println error.compress IO.println error.compress
| .ok command => | .ok command =>

2
Pantograph.lean
View File

@ -55,7 +55,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
| "proof.printTree" => run proof_print_tree | "proof.printTree" => run proof_print_tree
| cmd => | cmd =>
let error: Commands.InteractionError := let error: Commands.InteractionError :=
{ error := "unknown", desc := s!"Unknown command {cmd}" } { error := "command", desc := s!"Unknown command {cmd}" }
return Lean.toJson error return Lean.toJson error
where where
errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc } errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }

14
Test/Integration.lean
View File

@ -41,7 +41,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
catch ex => catch ex =>
return LSpec.check s!"Uncaught IO exception: {ex.toString}" false 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 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 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" 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 }: (Lean.toJson ({ options with printExprAST := true }:
Commands.OptionsPrintResult)) 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 def test_integration: IO LSpec.TestSeq := do
return LSpec.group "Integration" $ 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 end Pantograph.Test