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

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-21 16:40:54 -07:00
parent 9faca046d6
commit f9898a1d45
1 changed files with 10 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/Lean/Attributes.lean
View file

@ -37,7 +37,7 @@ Note that the attribute handler (`AttributeImpl.add`) is responsible for interpr
making sure that these kinds are respected.
-/
inductive AttributeKind
| global | «local» | «scoped»
| global | local | scoped
deriving BEq, Inhabited
instance : ToString AttributeKind where
@ -160,8 +160,7 @@ def registerTagAttribute (name : Name) (descr : String)
unless (env.getModuleIdxFor? decl).isNone do
throwError "invalid attribute '{name}', declaration is in an imported module"
validate decl
let env ← getEnv
setEnv <| ext.addEntry env decl
modifyEnv fun env => ext.addEntry env decl
}
registerBuiltinAttribute attrImpl
return { attr := attrImpl, ext := ext }
@ -192,7 +191,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()
def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
def registerParametricAttribute [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
name := impl.name
mkInitial := pure {}
@ -213,8 +212,7 @@ def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAtt
unless (env.getModuleIdxFor? decl).isNone do
throwError "invalid attribute '{impl.name}', declaration is in an imported module"
let val ← impl.getParam decl stx
let env' := ext.addEntry env (decl, val)
setEnv env'
modifyEnv fun env => ext.addEntry env (decl, val)
try impl.afterSet decl val catch _ => setEnv env
}
registerBuiltinAttribute attrImpl
@ -222,7 +220,7 @@ def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAtt
namespace ParametricAttribute
def getParam? {α : Type} [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α :=
def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α :=
match env.getModuleIdxFor? decl with
| some modIdx =>
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) with
@ -230,7 +228,7 @@ def getParam? {α : Type} [Inhabited α] (attr : ParametricAttribute α) (env :
| none => none
| none => (attr.ext.getState env).find? decl
def setParam {α : Type} (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment :=
def setParam (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment :=
if (env.getModuleIdxFor? decl).isSome then
Except.error ("invalid '" ++ toString attr.attr.name ++ "'.setParam, declaration is in an imported module")
else if ((attr.ext.getState env).find? decl).isSome then
@ -249,7 +247,7 @@ structure EnumAttributes (α : Type) where
ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
deriving Inhabited
def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α))
def registerEnumAttributes [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α))
(validate : Name → α → AttrM Unit := fun _ _ => pure ())
(applicationTime := AttributeApplicationTime.afterTypeChecking)
(ref : Name := by exact decl_name%) : IO (EnumAttributes α) := do
@ -274,7 +272,7 @@ def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDesc
unless (env.getModuleIdxFor? decl).isNone do
throwError "invalid attribute '{name}', declaration is in an imported module"
validate decl val
setEnv <| ext.addEntry env (decl, val)
modifyEnv fun env => ext.addEntry env (decl, val)
applicationTime := applicationTime
: AttributeImpl
}
@ -283,7 +281,7 @@ def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDesc
namespace EnumAttributes
def getValue {α : Type} [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option α :=
def getValue [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option α :=
match env.getModuleIdxFor? decl with
| some modIdx =>
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) with
@ -291,7 +289,7 @@ def getValue {α : Type} [Inhabited α] (attr : EnumAttributes α) (env : Enviro
| none => none
| none => (attr.ext.getState env).find? decl
def setValue {α : Type} (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String Environment :=
def setValue (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String Environment :=
if (env.getModuleIdxFor? decl).isSome then
Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, declaration is in an imported module")
else if ((attrs.ext.getState env).find? decl).isSome then