From 78a3b240ba6de1826d879801ceed5a4d61df4940 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 19:56:03 -0700 Subject: [PATCH] test: Catalog has no numeric symbols --- Pantograph/Environment.lean | 2 +- Test/Environment.lean | 29 ++++++++++++++++++++++------- 2 files changed, 23 insertions(+), 8 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index a85342a..19c3249 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -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" diff --git a/Test/Environment.lean b/Test/Environment.lean index 7014584..7a398da 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -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