diff --git a/Pantograph.lean b/Pantograph.lean index 30ac0c0..9d9399d 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,7 +1,6 @@ import Pantograph.Goal import Pantograph.Protocol import Pantograph.Serial -import Pantograph.Symbol import Pantograph.Environment import Lean.Data.HashMap diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index e9a884e..ab4513f 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -1,5 +1,4 @@ import Pantograph.Protocol -import Pantograph.Symbol import Pantograph.Serial import Lean @@ -10,6 +9,29 @@ namespace Pantograph.Environment abbrev CR α := Except Protocol.InteractionError α +def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool := + isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe + where + isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with + | .str _ name => name == "Lean" + | _ => true + +def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String := + let pref := match info with + | .axiomInfo _ => "a" + | .defnInfo _ => "d" + | .thmInfo _ => "t" + | .opaqueInfo _ => "o" + | .quotInfo _ => "q" + | .inductInfo _ => "i" + | .ctorInfo _ => "c" + | .recInfo _ => "r" + s!"{pref}{toString n}" + +def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String := + if is_symbol_unsafe_or_internal n info + then Option.none + else Option.some <| to_compact_symbol_name n info def catalog (_: Protocol.EnvCatalog): CoreM (CR Protocol.EnvCatalogResult) := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 1589408..9b68319 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -1,7 +1,5 @@ import Lean -import Pantograph.Symbol - def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := { msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false diff --git a/Pantograph/Symbol.lean b/Pantograph/Symbol.lean deleted file mode 100644 index ba80877..0000000 --- a/Pantograph/Symbol.lean +++ /dev/null @@ -1,29 +0,0 @@ -import Lean - -namespace Pantograph - -def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool := - isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe - where - isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with - | .str _ name => name == "Lean" - | _ => true - -def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String := - let pref := match info with - | .axiomInfo _ => "a" - | .defnInfo _ => "d" - | .thmInfo _ => "t" - | .opaqueInfo _ => "o" - | .quotInfo _ => "q" - | .inductInfo _ => "i" - | .ctorInfo _ => "c" - | .recInfo _ => "r" - s!"{pref}{toString n}" - -def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String := - if is_symbol_unsafe_or_internal n info - then Option.none - else Option.some <| to_compact_symbol_name n info - -end Pantograph diff --git a/Test/Catalog.lean b/Test/Catalog.lean index 44c2bf7..43becdc 100644 --- a/Test/Catalog.lean +++ b/Test/Catalog.lean @@ -1,6 +1,6 @@ import LSpec import Pantograph.Serial -import Pantograph.Symbol +import Pantograph.Environment namespace Pantograph.Test.Catalog @@ -14,7 +14,7 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do ] let suite := entries.foldl (λ suites (symbol, target) => let constant := env.constants.find! symbol - let test := LSpec.check symbol.toString ((is_symbol_unsafe_or_internal symbol constant) == target) + let test := LSpec.check symbol.toString ((Environment.is_symbol_unsafe_or_internal symbol constant) == target) LSpec.TestSeq.append suites test) LSpec.TestSeq.done return suite diff --git a/Test/Serial.lean b/Test/Serial.lean index 0730bad..e502fa8 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -1,6 +1,5 @@ import LSpec import Pantograph.Serial -import Pantograph.Symbol namespace Pantograph.Test.Serial