diff --git a/Main.lean b/Main.lean index 50c8917..fc064f4 100644 --- a/Main.lean +++ b/Main.lean @@ -1,24 +1,41 @@ -import Pantograph import Lean.Data.Json +import Pantograph.Commands namespace Pantograph structure State where - keys: Array String + environments: Array String -- State monad abbrev T (m: Type → Type) := StateT State m +abbrev Subroutine := T (Except String) Lean.Json + +structure Command where + cmd: String + payload: Lean.Json + deriving Lean.FromJson + +--def create_environment (args: Create): Subroutine := do +-- let state ← get + end Pantograph open Pantograph - -def execute (command: String): T (Except String) Lean.Json := do +def execute (command: String): T (ExceptT String IO) Lean.Json := do let state ← get let obj ← Lean.Json.parse command - return "success" + let command: Command ← Lean.fromJson? obj + match command.cmd with + | "create" => + let create: Commands.Create ← Lean.fromJson? command.payload + return Lean.toJson create.imports + | "catalog" => + let catalog: Commands.Catalog ← Lean.fromJson? command.payload + return "catalog stub" + | cmd => throw s!"Unknown verb: {cmd}" -- Main IO functions @@ -32,7 +49,8 @@ unsafe def loop : T IO Unit := do let state ← get let command ← getLines if command == "" then return () - match (execute command).run' <| state with + let ret ← execute command + match ret with | .error e => IO.println s!"Could not parse json: {e}" | .ok obj => IO.println <| toString <| obj diff --git a/Pantograph.lean b/Pantograph.lean deleted file mode 100644 index e99d3a6..0000000 --- a/Pantograph.lean +++ /dev/null @@ -1 +0,0 @@ -def hello := "world" \ No newline at end of file diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean new file mode 100644 index 0000000..ae9de66 --- /dev/null +++ b/Pantograph/Commands.lean @@ -0,0 +1,13 @@ +-- All the command input/output structures are stored here +import Lean.Data.Json + +namespace Pantograph.Commands + +structure Create where + imports : List String + deriving Lean.FromJson +structure Catalog where + id: Nat + deriving Lean.FromJson + +end Pantograph.Commands