test: Catalog has no numeric symbols

This commit is contained in:
Leni Aniva 2024-03-28 19:56:03 -07:00
parent 8fa1a7d383
commit e79e386b39
2 changed files with 23 additions and 8 deletions

View File

@ -9,7 +9,7 @@ namespace Pantograph.Environment
def isNameInternal (n: Lean.Name): Bool := def isNameInternal (n: Lean.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 isLeanSymbol n (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) n.isAuxLemma n.hasMacroScopes
where where
isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
| .str _ name => name == "Lean" | .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.RecursorInfo
deriving instance DecidableEq, Repr for Protocol.EnvInspectResult 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 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),
@ -30,7 +45,11 @@ inductive ConstantCat where
| ctor (info: Protocol.ConstructorInfo) | ctor (info: Protocol.ConstructorInfo)
| recursor (info: Protocol.RecursorInfo) | 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) := [ let testCases: List (String × ConstantCat) := [
("Or", ConstantCat.induct { ("Or", ConstantCat.induct {
numParams := 2, numParams := 2,
@ -76,13 +95,9 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
runCoreMSeq env inner runCoreMSeq env inner
def suite: IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
return LSpec.group "Environment" $ return LSpec.group "Environment" $
(LSpec.group "Catalog" (← test_catalog)) ++
(LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++ (LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
(LSpec.group "Inspect" (← test_inspect env)) (LSpec.group "Inspect" (← test_inspect))
end Pantograph.Test.Environment end Pantograph.Test.Environment