max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add assertions to make sure TagDeclarationExtension and MapDeclarationExtension are not being misused

Browse source 
see #1111
This commit is contained in:
Leonardo de Moura 2022-04-15 13:47:49 -07:00
parent 7797fa3e2d
commit 7995cb071f
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Lean/Environment.lean
View file

@ -463,17 +463,19 @@ namespace TagDeclarationExtension
instance : Inhabited TagDeclarationExtension :=
inferInstanceAs (Inhabited (SimplePersistentEnvExtension Name NameSet))
def tag (ext : TagDeclarationExtension) (env : Environment) (n : Name) : Environment :=
ext.addEntry env n
def tag (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : Environment :=
assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `TagDeclarationExtension`
ext.addEntry env declName
def isTagged (ext : TagDeclarationExtension) (env : Environment) (n : Name) : Bool :=
match env.getModuleIdxFor? n with
| some modIdx => (ext.getModuleEntries env modIdx).binSearchContains n Name.quickLt
| none => (ext.getState env).contains n
def isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : Bool :=
match env.getModuleIdxFor? declName with
| some modIdx => (ext.getModuleEntries env modIdx).binSearchContains declName Name.quickLt
| none => (ext.getState env).contains declName
end TagDeclarationExtension
/-- Environment extension for mapping declarations to values. -/
/-- Environment extension for mapping declarations to values.
Declarations must only be inserted into the mapping in the module where they were declared. -/
def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α)
@ -491,6 +493,7 @@ instance : Inhabited (MapDeclarationExtension α) :=
inferInstanceAs (Inhabited (SimplePersistentEnvExtension ..))
def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment :=
assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`
ext.addEntry env (declName, val)
def find? [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) : Option α :=