Move all json-string functions to Main.lean

This commit is contained in:
Leni Aniva 2023-08-22 09:54:37 -07:00
parent 96cbbf2551
commit a8cbb3be4f
2 changed files with 15 additions and 15 deletions

View File

@ -7,6 +7,21 @@ import Pantograph
-- Main IO functions -- Main IO functions
open Pantograph open Pantograph
/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
def parse_command (s: String): Except String Commands.Command := do
let s := s.trim
match s.get? 0 with
| .some '{' => -- Parse in Json mode
Lean.fromJson? (← Lean.Json.parse s)
| .some _ => -- Parse in line mode
let offset := s.posOf ' ' |> s.offsetOfPos
if offset = s.length then
return { cmd := s.take offset, payload := Lean.Json.null }
else
let payload ← s.drop offset |> Lean.Json.parse
return { cmd := s.take offset, payload := payload }
| .none => throw "Command is empty"
unsafe def loop : MainM Unit := do unsafe def loop : MainM Unit := do
let state ← get let state ← get
let command ← (← IO.getStdin).getLine let command ← (← IO.getStdin).getLine

View File

@ -20,21 +20,6 @@ abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
-- monadic features in `MainM` -- monadic features in `MainM`
abbrev CR α := Except Commands.InteractionError α abbrev CR α := Except Commands.InteractionError α
/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
def parse_command (s: String): Except String Commands.Command := do
let s := s.trim
match s.get? 0 with
| .some '{' => -- Parse in Json mode
Lean.fromJson? (← Lean.Json.parse s)
| .some _ => -- Parse in line mode
let offset := s.posOf ' ' |> s.offsetOfPos
if offset = s.length then
return { cmd := s.take offset, payload := Lean.Json.null }
else
let payload ← s.drop offset |> Lean.Json.parse
return { cmd := s.take offset, payload := payload }
| .none => throw "Command is empty"
def execute (command: Commands.Command): MainM Lean.Json := do def execute (command: Commands.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with match Lean.fromJson? command.payload with