From 7b59937853fd70fdf8842b00e3fe470fc127e1d6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 25 Nov 2023 15:07:56 -0800
Subject: [PATCH] feat: Read dependencies of library symbols

---
 Pantograph.lean          | 2 ++
 Pantograph/Protocol.lean | 4 ++++
 2 files changed, 6 insertions(+)

diff --git a/Pantograph.lean b/Pantograph.lean
index f456e81..2f712e7 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -85,6 +85,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       return .ok {
         type := ← serialize_expression state.options info.type,
         value? := ← value?.mapM (λ v => serialize_expression state.options v),
+        typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
+        valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
         module? := module?
       }
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index c01228d..95c0236 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -113,11 +113,15 @@ structure LibInspect where
   -- If true/false, show/hide the value expressions; By default definitions
   -- values are shown and theorem values are hidden.
   value?: Option Bool := .some false
+  -- If true, show the type and value dependencies
+  dependency?: Option Bool := .some false
   deriving Lean.FromJson
 structure LibInspectResult where
   type: Expression
   value?: Option Expression := .none
   module?: Option String
+  typeDependency?: Option (Array String) := .none
+  valueDependency?: Option (Array String) := .none
   deriving Lean.ToJson
 
 /-- Set options; See `Options` struct above for meanings -/