From 65da39440d2d7801976db0a3e4fbd29fdfd7d59a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 20 May 2023 13:03:12 -0700
Subject: [PATCH] Add alternative command input format and IO stub

---
 Examples/ExprIO.lean | 25 +++++++++++++++++++++++++
 Examples/Proof.lean  | 10 +++-------
 Main.lean            | 29 ++++++++++++++++++++++-------
 Pantograph/IO.lean   | 13 +++++++++++++
 README.md            | 17 ++++++++++++-----
 lakefile.lean        |  6 ++++++
 6 files changed, 81 insertions(+), 19 deletions(-)
 create mode 100644 Examples/ExprIO.lean
 create mode 100644 Pantograph/IO.lean

diff --git a/Examples/ExprIO.lean b/Examples/ExprIO.lean
new file mode 100644
index 0000000..efc8522
--- /dev/null
+++ b/Examples/ExprIO.lean
@@ -0,0 +1,25 @@
+import Lean
+
+def strToName (s: String): Lean.Name :=
+  (s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous
+
+unsafe def main (args: List String): IO Unit := do
+  Lean.enableInitializersExecution
+  Lean.initSearchPath (← Lean.findSysroot)
+  let imports := ["Init"]
+  let env: Lean.Environment ← Lean.importModules
+    (imports := imports.map (λ str => { module := strToName str, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+
+  let expr := args.head?.getD "a + b"
+
+  match Lean.Parser.runParserCategory
+    (env := env)
+    (catName := `term)
+    (input := expr)
+    (fileName := "<stdin>") with
+  | Except.error error => IO.println s!"{error}"
+  | Except.ok (syn: Lean.Syntax) =>
+    let reprint := Lean.Syntax.reprint syn |>.get!
+    IO.println reprint
diff --git a/Examples/Proof.lean b/Examples/Proof.lean
index c4e18f1..51530d0 100644
--- a/Examples/Proof.lean
+++ b/Examples/Proof.lean
@@ -17,9 +17,9 @@ def execute_proof (env: Lean.Environment): IO Unit := do
     let tactic := "intro n m"
     let (state, response) ← execute_tactic state tactic
     IO.println s! "Executed {tactic}  Errors: {response.errors}  Goals: {response.goals}"
-    --let tactic := "assumption" -- should fail
-    --let (_, response) ← execute_tactic state tactic
-    --IO.println s! "Executed {tactic}  Errors: {response.errors}  Goals: {response.goals}"
+    let tactic := "assumption" -- should fail
+    let (_, response) ← execute_tactic state tactic
+    IO.println s! "Executed {tactic}  Errors: {response.errors}  Goals: {response.goals}"
     let tactic := "rw [Nat.add_comm]"
     let (state, response) ← execute_tactic state tactic
     IO.println s! "Executed {tactic}  Errors: {response.errors}  Goals: {response.goals}"
@@ -34,7 +34,3 @@ unsafe def main : IO Unit := do
     (opts := {})
     (trustLevel := 1)
   execute_proof env
-
-example : ∀ (n m : Nat), n + m = m + n := by
-  intros n m
-  rw [Nat.add_comm]
diff --git a/Main.lean b/Main.lean
index 9daf2f5..e104e8d 100644
--- a/Main.lean
+++ b/Main.lean
@@ -12,6 +12,27 @@ def option_expect (o: Option α) (error: String): Except String α :=
   | .some value => return value
   | .none => throw error
 
+structure Command where
+  cmd: String
+  payload: Lean.Json
+  deriving Lean.FromJson
+
+
+/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
+def parse_command (s: String): Except String 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"
+
 
 structure State where
   environments: Array Lean.Environment
@@ -22,16 +43,10 @@ abbrev Subroutine α := ExceptT String (T IO) α
 
 def nextId (s: State): Nat := s.environments.size
 
-structure Command where
-  cmd: String
-  payload: Lean.Json
-  deriving Lean.FromJson
-
 open Commands
 
 unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do
-  let obj ← Lean.Json.parse command
-  let command: Command ← Lean.fromJson? obj
+  let command: Command ← parse_command command
   match command.cmd with
   | "create" =>
     let args: Commands.Create ← Lean.fromJson? command.payload
diff --git a/Pantograph/IO.lean b/Pantograph/IO.lean
new file mode 100644
index 0000000..d0bf946
--- /dev/null
+++ b/Pantograph/IO.lean
@@ -0,0 +1,13 @@
+import Lean
+
+/-
+Expression IO
+-/
+
+
+namespace Pantograph.IO
+
+
+
+
+end Pantograph.IO
diff --git a/README.md b/README.md
index 2cee1a0..21ca367 100644
--- a/README.md
+++ b/README.md
@@ -19,19 +19,26 @@ lake build mathlib
 
 ## Usage
 
-The binary must be run inside a `lake env` environment.
+The binary must be run inside a `lake env` environment. i.e. `lake env
+build/bin/pantograph`. The REPL loop accepts commands and outputs either an
+`Error:` (indicating malformed command) or a json return value indicating the
+result of a command execution. The command can be passed in one of two formats
+```
+command { ... }
+{ "cmd": command, "payload": ... }
+```
 
 Example: (~5k symbols)
 ```
 $ lake env build/bin/Pantograph
-{"cmd": "create", "payload": {"imports": ["Init"]}}
-{"cmd": "catalog", "payload": {"id": 0}}
+create {"imports": ["Init"]}
+catalog {"id": 0}
 ```
 Example with `mathlib` (~90k symbols)
 ```
 $ lake env build/bin/Pantograph
-{"cmd": "create", "payload": {"imports": ["Mathlib.Analysis.Seminorm"]}}
-{"cmd": "catalog", "payload": {"id": 0}}
+create {"imports": ["Mathlib.Analysis.Seminorm"]}
+catalog {"id": 0}
 ```
 
 
diff --git a/lakefile.lean b/lakefile.lean
index a642187..a49f77a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -23,3 +23,9 @@ lean_exe examples_proof {
   -- Somehow solves the native symbol not found problem
   supportInterpreter := true
 }
+
+lean_exe examples_expr_io {
+  root := `Examples.ExprIO
+  -- Somehow solves the native symbol not found problem
+  supportInterpreter := true
+}