feat: Read dependencies of library symbols #32

Merged
aniva merged 1 commits from library/dependency into dev 2023-11-25 23:06:48 -08:00
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 { return .ok {
type := ← serialize_expression state.options info.type, type := ← serialize_expression state.options info.type,
value? := ← value?.mapM (λ v => serialize_expression state.options v), 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? module? := module?
} }
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do 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 -- If true/false, show/hide the value expressions; By default definitions
-- values are shown and theorem values are hidden. -- values are shown and theorem values are hidden.
value?: Option Bool := .some false value?: Option Bool := .some false
-- If true, show the type and value dependencies
dependency?: Option Bool := .some false
deriving Lean.FromJson deriving Lean.FromJson
structure LibInspectResult where structure LibInspectResult where
type: Expression type: Expression
value?: Option Expression := .none value?: Option Expression := .none
module?: Option String module?: Option String
typeDependency?: Option (Array String) := .none
valueDependency?: Option (Array String) := .none
deriving Lean.ToJson deriving Lean.ToJson
/-- Set options; See `Options` struct above for meanings -/ /-- Set options; See `Options` struct above for meanings -/