feat: Add definitions and theorems to the environment #41

Merged
aniva merged 9 commits from env/add-decl into dev 2023-12-26 12:41:02 -08:00
6 changed files with 25 additions and 36 deletions
Showing only changes of commit 22789436bd - Show all commits

View File

@ -1,7 +1,6 @@
import Pantograph.Goal import Pantograph.Goal
import Pantograph.Protocol import Pantograph.Protocol
import Pantograph.Serial import Pantograph.Serial
import Pantograph.Symbol
import Pantograph.Environment import Pantograph.Environment
import Lean.Data.HashMap import Lean.Data.HashMap

View File

@ -1,5 +1,4 @@
import Pantograph.Protocol import Pantograph.Protocol
import Pantograph.Symbol
import Pantograph.Serial import Pantograph.Serial
import Lean import Lean
@ -10,6 +9,29 @@ namespace Pantograph.Environment
abbrev CR α := Except Protocol.InteractionError α 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 def catalog (_: Protocol.EnvCatalog): CoreM (CR Protocol.EnvCatalogResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info => let names := env.constants.fold (init := #[]) (λ acc name info =>

View File

@ -1,7 +1,5 @@
import Lean import Lean
import Pantograph.Symbol
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
{ {
msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false

View File

@ -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

View File

@ -1,6 +1,6 @@
import LSpec import LSpec
import Pantograph.Serial import Pantograph.Serial
import Pantograph.Symbol import Pantograph.Environment
namespace Pantograph.Test.Catalog 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 suite := entries.foldl (λ suites (symbol, target) =>
let constant := env.constants.find! symbol 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 LSpec.TestSeq.append suites test) LSpec.TestSeq.done
return suite return suite

View File

@ -1,6 +1,5 @@
import LSpec import LSpec
import Pantograph.Serial import Pantograph.Serial
import Pantograph.Symbol
namespace Pantograph.Test.Serial namespace Pantograph.Test.Serial