From c4a1ccad13927ca463881cadea96725b8660ab97 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 20 May 2023 14:04:09 -0700
Subject: [PATCH] Add expression IO stub for constant types

---
 Main.lean                | 54 +++++++++++++++++++++++++++-------------
 Pantograph/Commands.lean | 10 +++++++-
 Pantograph/IO.lean       |  3 +++
 README.md                |  1 +
 4 files changed, 50 insertions(+), 18 deletions(-)

diff --git a/Main.lean b/Main.lean
index e104e8d..62a3d78 100644
--- a/Main.lean
+++ b/Main.lean
@@ -2,10 +2,27 @@ import Lean.Data.Json
 import Lean.Environment
 
 import Pantograph.Commands
+import Pantograph.IO
 import Pantograph.Symbols
 
 namespace Pantograph
 
+/-- Stores state of the REPL -/
+structure State where
+  environments: Array Lean.Environment
+
+-- State monad
+abbrev T (m: Type → Type) := StateT State m
+abbrev Subroutine α := ExceptT String (T IO) α
+
+def nextId (s: State): Nat := s.environments.size
+
+def State.getEnv (state: State) (id: Nat): Except String Lean.Environment :=
+  match state.environments.get? id with
+  | .some env => return env
+  | .none => throw s!"Invalid environment id {id}"
+
+
 -- Utilities
 def option_expect (o: Option α) (error: String): Except String α :=
   match o with
@@ -17,7 +34,6 @@ structure Command where
   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
@@ -34,14 +50,6 @@ def parse_command (s: String): Except String Command := do
   | .none => throw "Command is empty"
 
 
-structure State where
-  environments: Array Lean.Environment
-
--- State monad
-abbrev T (m: Type → Type) := StateT State m
-abbrev Subroutine α := ExceptT String (T IO) α
-
-def nextId (s: State): Nat := s.environments.size
 
 open Commands
 
@@ -60,6 +68,10 @@ unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do
     -- Delete all the environments
     let ret ← clear
     return Lean.toJson ret
+  | "inspect" =>
+    let args: Commands.Inspect ← Lean.fromJson? command.payload
+    let ret ← inspect args
+    return Lean.toJson ret
   | "proof.trace" =>
     let args: Commands.ProofTrace ← Lean.fromJson? command.payload
     let ret ← proof_trace args
@@ -82,19 +94,27 @@ unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do
       filtered_symbols := num_filtered_symbols }
   catalog (args: Catalog): Subroutine CatalogResult := do
     let state ← get
-    match state.environments.get? args.id with
-    | .some env =>
-      let names := env.constants.fold (init := []) (λ es name info =>
-        match to_filtered_symbol name info with
-        | .some x => x::es
-        | .none => es)
-      return { theorems := names }
-    | .none => throw s!"Invalid environment id {args.id}"
+    let env ← state.getEnv args.id
+    let names := env.constants.fold (init := []) (λ es name info =>
+      match to_filtered_symbol name info with
+      | .some x => x::es
+      | .none => es)
+    return { theorems := names }
   clear: Subroutine ClearResult := do
     let state ← get
     for env in state.environments do
       env.freeRegions
     return { n := state.environments.size }
+  inspect (args: Inspect): Subroutine InspectResult := do
+    let state ← get
+    let env ← state.getEnv args.id
+    let info? := env.find? <| strToName args.symbol
+    let info ← match info? with
+      | none => throw s!"Symbol not found: {args.symbol}"
+      | some info => pure info.toConstantVal
+    -- Now print the type expression
+    let format := IO.exprToStr env info.type
+    return { type := format }
   proof_trace (args: ProofTrace): Subroutine ProofTraceResult := do
     -- Step 1: Create tactic state
     -- Step 2: Execute tactic
diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean
index d6b62f3..5561f68 100644
--- a/Pantograph/Commands.lean
+++ b/Pantograph/Commands.lean
@@ -4,7 +4,7 @@ import Lean.Data.Json
 namespace Pantograph.Commands
 
 structure Create where
-  imports : List String
+  imports : List String  := []
   deriving Lean.FromJson
 structure CreateResult where
   id: Nat
@@ -23,6 +23,14 @@ structure ClearResult where
   n: Nat -- Number of environments reset
   deriving Lean.ToJson
 
+structure Inspect where
+  id: Nat -- Environment id
+  symbol: String
+  deriving Lean.FromJson
+structure InspectResult where
+  type: String
+  deriving Lean.ToJson
+
 structure ProofTrace where
   id: Nat -- Environment id
   deriving Lean.FromJson
diff --git a/Pantograph/IO.lean b/Pantograph/IO.lean
index d0bf946..ae02e62 100644
--- a/Pantograph/IO.lean
+++ b/Pantograph/IO.lean
@@ -8,6 +8,9 @@ Expression IO
 namespace Pantograph.IO
 
 
+def exprToStr (env: Lean.Environment) (e: Lean.Expr): String :=
+  let format := Lean.Meta.ppExpr e
+  "stub"
 
 
 end Pantograph.IO
diff --git a/README.md b/README.md
index 21ca367..71b62e7 100644
--- a/README.md
+++ b/README.md
@@ -27,6 +27,7 @@ result of a command execution. The command can be passed in one of two formats
 command { ... }
 { "cmd": command, "payload": ... }
 ```
+The list of available commands can be found in `Pantograph/Commands.lean`
 
 Example: (~5k symbols)
 ```