Pantograph/Main.lean

41 lines
857 B
Plaintext
Raw Normal View History

2023-05-07 15:19:45 -07:00
import Pantograph
2023-05-09 16:39:24 -07:00
import Lean.Data.Json
2023-05-07 15:19:45 -07:00
2023-05-09 16:39:24 -07:00
namespace Pantograph
structure State where
keys: Array String
-- State monad
abbrev T (m: Type → Type) := StateT State m
end Pantograph
open Pantograph
def execute (command: String): T (Except String) Lean.Json := do
let state ← get
let obj ← Lean.Json.parse command
return "success"
-- Main IO functions
unsafe def getLines : IO String := do
match (← (← IO.getStdin).getLine) with
| "" => pure ""
| "\n" => pure "\n"
| line => pure <| line ++ (← getLines)
unsafe def loop : T IO Unit := do
let state ← get
let command ← getLines
if command == "" then return ()
match (execute command).run' <| state with
| .error e => IO.println s!"Could not parse json: {e}"
| .ok obj => IO.println <| toString <| obj
unsafe def main : IO Unit :=
StateT.run' loop ⟨#[]⟩