From 9a957bce35b419b5baa9cfb157951a07b1987efe Mon Sep 17 00:00:00 2001
From: Leni Ven <leniv@stanford.edu>
Date: Tue, 9 May 2023 16:39:24 -0700
Subject: [PATCH] Add REPL

---
 Main.lean | 40 ++++++++++++++++++++++++++++++++++++++--
 1 file changed, 38 insertions(+), 2 deletions(-)

diff --git a/Main.lean b/Main.lean
index 30cb991..50c8917 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,4 +1,40 @@
 import Pantograph
+import Lean.Data.Json
 
-def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
+
+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 ⟨#[]⟩