feat: Remove display of implementation details #50

Merged
aniva merged 5 commits from io/serial into dev 2024-03-28 22:35:38 -07:00
2 changed files with 23 additions and 8 deletions
Showing only changes of commit 78a3b240ba - Show all commits

View File

@ -9,7 +9,7 @@ namespace Pantograph.Environment
def isNameInternal (n: Lean.Name): Bool :=
-- 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
isLeanSymbol n (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) n.isAuxLemma n.hasMacroScopes
where
isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
| .str _ name => name == "Lean"

View File

@ -14,6 +14,21 @@ deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
deriving instance DecidableEq, Repr for Protocol.RecursorInfo
deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
def test_catalog: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let inner: CoreM LSpec.TestSeq := do
let catalogResult ← Environment.catalog {}
let symbolsWithNum := env.constants.fold (init := #[]) (λ acc name info =>
match (Environment.toFilteredSymbol name info).isSome && (name matches .num _ _) with
| false => acc
| true => acc.push name
)
return LSpec.check "No num symbols" (symbolsWithNum.size == 0)
runCoreMSeq env inner
def test_symbol_visibility: IO LSpec.TestSeq := do
let entries: List (Name × Bool) := [
("Nat.add_comm".toName, false),
@ -30,7 +45,11 @@ inductive ConstantCat where
| ctor (info: Protocol.ConstructorInfo)
| recursor (info: Protocol.RecursorInfo)
def test_inspect (env: Environment): IO LSpec.TestSeq := do
def test_inspect: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let testCases: List (String × ConstantCat) := [
("Or", ConstantCat.induct {
numParams := 2,
@ -76,13 +95,9 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
runCoreMSeq env inner
def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
return LSpec.group "Environment" $
(LSpec.group "Catalog" (← test_catalog)) ++
(LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
(LSpec.group "Inspect" (← test_inspect env))
(LSpec.group "Inspect" (← test_inspect))
end Pantograph.Test.Environment