feat: Read dependencies of library symbols

This commit is contained in:
Leni Aniva 2023-11-25 15:07:56 -08:00
parent a1d991f5db
commit aaebb6b121
2 changed files with 6 additions and 0 deletions

View File

@ -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

View File

@ -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 -/