From 5a297e8fef16adccdd71f4fd4ef0550e3d82ede1 Mon Sep 17 00:00:00 2001
From: Leni Ven <leniv@stanford.edu>
Date: Tue, 9 May 2023 22:51:19 -0700
Subject: [PATCH] Add README and catalog functions

---
 Main.lean                | 68 ++++++++++++++++++++++++++++++++--------
 Pantograph/Commands.lean | 10 ++++++
 README.md                | 21 +++++++++++++
 lakefile.lean            |  1 +
 4 files changed, 87 insertions(+), 13 deletions(-)
 create mode 100644 README.md

diff --git a/Main.lean b/Main.lean
index fc064f4..76523bf 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,42 +1,84 @@
 import Lean.Data.Json
-import Pantograph.Commands
+import Lean.Environment
 
+import Pantograph.Commands
 
 namespace Pantograph
 
+-- Utilities
+def option_expect (o: Option α) (error: String): Except String α :=
+  match o with
+  | .some value => return value
+  | .none => throw error
+
 structure State where
-  environments: Array String
+  environments: Array Lean.Environment
 
 -- State monad
 abbrev T (m: Type → Type) := StateT State m
-abbrev Subroutine := T (Except String) Lean.Json
+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
 
---def create_environment (args: Create): Subroutine := do
---  let state ← get
+namespace Commands
 
+def create (args: Create): Subroutine CreateResult := do
+  let state ← get
+  let id := nextId state
+  let env ← Lean.importModules
+    (imports := args.imports.map strTransform)
+    (opts := {})
+    (trustLevel := 1)
+  modify fun s => { environments := s.environments.push env }
+  return { id := id }
+  where strTransform (s: String): Lean.Import :=
+      let li := s.split (λ c => c == '.')
+      let name := li.foldl (λ pre segment => Lean.Name.str pre segment) Lean.Name.anonymous
+      { module := name, runtimeOnly := false }
 
+def catalog (args: Catalog): Subroutine CatalogResult := do
+  let state ← get
+  match state.environments.get? args.id with
+  | .some env =>
+    let names := env.constants.toList.map (λ ⟨x, _⟩ => toString x)
+    return { theorems := names }
+  | .none => throw s!"Invalid environment id {args.id}"
+
+unsafe def clear: Subroutine ClearResult := do
+  let state ← get
+  for env in state.environments do
+    env.freeRegions
+  return { n := state.environments.size }
+
+end Commands
 end Pantograph
 
 open Pantograph
 
-def execute (command: String): T (ExceptT String IO) Lean.Json := do
-  let state ← get
+unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do
   let obj ← Lean.Json.parse command
   let command: Command ← Lean.fromJson? obj
   match command.cmd with
   | "create" =>
-    let create: Commands.Create ← Lean.fromJson? command.payload
-    return Lean.toJson create.imports
+    let args: Commands.Create ← Lean.fromJson? command.payload
+    let ret ← Commands.create args
+    return Lean.toJson ret
   | "catalog" =>
-    let catalog: Commands.Catalog ← Lean.fromJson? command.payload
-    return "catalog stub"
+    let args: Commands.Catalog ← Lean.fromJson? command.payload
+    let ret ← Commands.catalog args
+    return Lean.toJson ret
+  | "clear" =>
+    -- Delete all the environments
+    let ret ← Commands.clear
+    return Lean.toJson ret
   | cmd => throw s!"Unknown verb: {cmd}"
 
+
 -- Main IO functions
 
 unsafe def getLines : IO String := do
@@ -46,13 +88,13 @@ unsafe def getLines : IO String := do
   | line => pure <| line ++ (← getLines)
 
 unsafe def loop : T IO Unit := do
-  let state ← get
   let command ← getLines
   if command == "" then return ()
   let ret ← execute command
   match ret with
-  | .error e => IO.println s!"Could not parse json: {e}"
+  | .error e => IO.println s!"Error: {e}"
   | .ok obj => IO.println <| toString <| obj
+  loop
 
 unsafe def main : IO Unit :=
   StateT.run' loop ⟨#[]⟩
diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean
index ae9de66..14059d7 100644
--- a/Pantograph/Commands.lean
+++ b/Pantograph/Commands.lean
@@ -10,4 +10,14 @@ structure Catalog where
   id: Nat
   deriving Lean.FromJson
 
+structure CreateResult where
+  id: Nat
+  deriving Lean.ToJson
+structure CatalogResult where
+  theorems: List String
+  deriving Lean.ToJson
+structure ClearResult where
+  n: Nat -- Number of environments reset
+  deriving Lean.ToJson
+
 end Pantograph.Commands
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..f890444
--- /dev/null
+++ b/README.md
@@ -0,0 +1,21 @@
+# Pantograph
+
+An interaction system for Lean 4.
+
+## Installation
+
+Install `elan` and `lean4`. Then, execute
+``` sh
+lake build
+```
+
+## Usage
+
+Before usage, put the packages that you wish the REPL to use into a directory
+and build them. Put this directory into the variable `$LEAN_PATH`. Then
+``` 
+$ build/bin/Pantograph
+{"cmd": "create", "payload": {"imports": ["Mathlib.Analysis.Seminorm"]}}
+```
+
+
diff --git a/lakefile.lean b/lakefile.lean
index 546a324..f5d3fc2 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -16,4 +16,5 @@ lean_lib Pantograph {
 @[default_target]
 lean_exe pantograph {
   root := `Main
+  supportInterpreter := true
 }