From 4f5ffc1ffbc00a0b21fe0f12514a75fc925701b3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 15 Jan 2025 21:02:04 -0800
Subject: [PATCH 1/3] feat: Protocol for module access

---
 Pantograph/Protocol.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 62f3f69..c73e791 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -112,6 +112,24 @@ structure ExprEchoResult where
   type: Expression
   deriving Lean.ToJson
 
+-- Describe the current state of the environment
+structure EnvDescribe where
+  deriving Lean.FromJson
+structure EnvDescribeResult where
+  imports : Array String
+  modules : Array String
+  deriving Lean.ToJson
+
+-- Describe a module
+structure EnvModule where
+  module : String
+  deriving Lean.FromJson
+structure EnvModuleResult where
+  imports: Array String
+  constNames: Array String
+  extraConstNames: Array String
+  deriving Lean.ToJson
+
 -- Print all symbols in environment
 structure EnvCatalog where
   deriving Lean.FromJson
-- 
2.44.1


From c9f524b9aea1c475dc3085bd109fbd7ea9f4187a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 15 Jan 2025 21:20:05 -0800
Subject: [PATCH 2/3] feat: Implement `env.describe` and `env.module_read`

---
 Pantograph/Environment.lean | 16 ++++++++++++++++
 Pantograph/Protocol.lean    |  4 ++--
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index c48414a..6bd3f76 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -43,6 +43,22 @@ def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
   if isNameInternal n || info.isUnsafe
   then Option.none
   else Option.some <| toCompactSymbolName n info
+def describe (_: Protocol.EnvDescribe): CoreM Protocol.EnvDescribeResult := do
+  let env ← Lean.MonadEnv.getEnv
+  return {
+    imports := env.header.imports.map toString,
+    modules := env.header.moduleNames.map (·.toString),
+  }
+def moduleRead (args: Protocol.EnvModuleRead): CoreM (Protocol.CR Protocol.EnvModuleReadResult) := do
+  let env ← Lean.MonadEnv.getEnv
+  let .some i := env.header.moduleNames.findIdx? (· == args.module.toName) |
+    return .error $ Protocol.errorIndex s!"Module not found {args.module}"
+  let data := env.header.moduleData[i]!
+  return .ok {
+    imports := data.imports.map toString,
+    constNames := data.constNames.map (·.toString),
+    extraConstNames := data.extraConstNames.map (·.toString),
+  }
 def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
   let env ← Lean.MonadEnv.getEnv
   let names := env.constants.fold (init := #[]) (λ acc name info =>
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index c73e791..cab288c 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -121,10 +121,10 @@ structure EnvDescribeResult where
   deriving Lean.ToJson
 
 -- Describe a module
-structure EnvModule where
+structure EnvModuleRead where
   module : String
   deriving Lean.FromJson
-structure EnvModuleResult where
+structure EnvModuleReadResult where
   imports: Array String
   constNames: Array String
   extraConstNames: Array String
-- 
2.44.1


From bc4bf47c8b8c5e9c8d39ef7675fca7c7b942e152 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 15 Jan 2025 21:23:37 -0800
Subject: [PATCH 3/3] feat: Implement repl interfaces

---
 Repl.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Repl.lean b/Repl.lean
index 1fd8266..aebb738 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -48,6 +48,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     | "reset"         => run reset
     | "stat"          => run stat
     | "expr.echo"     => run expr_echo
+    | "env.describe"  => run env_describe
+    | "env.module_read" => run env_module_read
     | "env.catalog"   => run env_catalog
     | "env.inspect"   => run env_inspect
     | "env.add"       => run env_add
@@ -85,6 +87,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let nGoals := state.goalStates.size
     return .ok { nGoals }
+  env_describe (args: Protocol.EnvDescribe): MainM (CR Protocol.EnvDescribeResult) := do
+    let result ← Environment.describe args
+    return .ok result
+  env_module_read (args: Protocol.EnvModuleRead): MainM (CR Protocol.EnvModuleReadResult) := do
+    Environment.moduleRead args
   env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
     let result ← Environment.catalog args
     return .ok result
-- 
2.44.1