feat: Remove most filters on catalog

This commit is contained in:
Leni Aniva 2024-10-04 12:58:16 -07:00 committed by Leni Aniva
parent 22ddfaaf21
commit 8d774d3281
2 changed files with 4 additions and 8 deletions

View File

@ -10,16 +10,12 @@ namespace Pantograph.Environment
@[export pantograph_is_name_internal] @[export pantograph_is_name_internal]
def isNameInternal (n: Name): Bool := def isNameInternal (n: Name): Bool :=
-- Returns true if the name is an implementation detail which should not be shown to the user. -- Returns true if the name is an implementation detail which should not be shown to the user.
isLeanSymbol n (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) n.isAuxLemma n.hasMacroScopes n.isAuxLemma n.hasMacroScopes
where
isLeanSymbol (name: Name): Bool := match name.getRoot with
| .str _ name => name == "Lean"
| _ => true
/-- Catalog all the non-internal and safe names -/ /-- Catalog all the non-internal and safe names -/
@[export pantograph_environment_catalog] @[export pantograph_environment_catalog]
def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name info => def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
match isNameInternal name || info.isUnsafe with match isNameInternal name with
| false => acc.push name | false => acc.push name
| true => acc) | true => acc)

View File

@ -33,7 +33,7 @@ def test_catalog: IO LSpec.TestSeq := do
def test_symbol_visibility: IO LSpec.TestSeq := do def test_symbol_visibility: IO LSpec.TestSeq := do
let entries: List (Name × Bool) := [ let entries: List (Name × Bool) := [
("Nat.add_comm".toName, false), ("Nat.add_comm".toName, false),
("Lean.Name".toName, true), ("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
("Init.Data.Nat.Basic._auxLemma.4".toName, true), ("Init.Data.Nat.Basic._auxLemma.4".toName, true),
] ]
let suite := entries.foldl (λ suites (symbol, target) => let suite := entries.foldl (λ suites (symbol, target) =>