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

refactor: dead code AttributeExtensionOLeanEntry.decl (#5496)

Browse source 
The constructor `AttributeExtensionOLeanEntry.decl` and related code
seems to be unused, and has been unused since its introduction in
a77598f7cf three years ago. Probably worth
removing (and changing the now one-constructor inductive into a
structure).
This commit is contained in:
Joachim Breitner 2024-10-01 15:34:12 +02:00 • committed by GitHub
parent d0ee9d0127
commit 4932dbc65d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 13 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/Lean/Attributes.lean
View file

@ -305,15 +305,16 @@ def registerAttributeImplBuilder (builderId : Name) (builder : AttributeImplBuil
if table.contains builderId then throw (IO.userError ("attribute implementation builder '" ++ toString builderId ++ "' has already been declared"))
attributeImplBuilderTableRef.modify fun table => table.insert builderId builder
def mkAttributeImplOfBuilder (builderId ref : Name) (args : List DataValue) : IO AttributeImpl := do
let table ← attributeImplBuilderTableRef.get
match table[builderId]? with
| none => throw (IO.userError ("unknown attribute implementation builder '" ++ toString builderId ++ "'"))
| some builder => IO.ofExcept <| builder ref args
structure AttributeExtensionOLeanEntry where
builderId : Name
ref : Name
args : List DataValue
inductive AttributeExtensionOLeanEntry where
| decl (declName : Name) -- `declName` has type `AttributeImpl`
| builder (builderId ref : Name) (args : List DataValue)
def mkAttributeImplOfEntry (e : AttributeExtensionOLeanEntry) : IO AttributeImpl := do
let table ← attributeImplBuilderTableRef.get
match table[e.builderId]? with
| none => throw (IO.userError ("unknown attribute implementation builder '" ++ toString e.builderId ++ "'"))
| some builder => IO.ofExcept <| builder e.ref e.args
structure AttributeExtensionState where
newEntries : List AttributeExtensionOLeanEntry := []
@ -337,19 +338,13 @@ unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options)
@[implemented_by mkAttributeImplOfConstantUnsafe]
opaque mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl
def mkAttributeImplOfEntry (env : Environment) (opts : Options) (e : AttributeExtensionOLeanEntry) : IO AttributeImpl :=
match e with
| .decl declName => IO.ofExcept <| mkAttributeImplOfConstant env opts declName
| .builder builderId ref args => mkAttributeImplOfBuilder builderId ref args
private def AttributeExtension.addImported (es : Array (Array AttributeExtensionOLeanEntry)) : ImportM AttributeExtensionState := do
let ctx ← read
let map ← attributeMapRef.get
let map ← es.foldlM
(fun map entries =>
entries.foldlM
(fun (map : Std.HashMap Name AttributeImpl) entry => do
let attrImpl ← mkAttributeImplOfEntry ctx.env ctx.opts entry
let attrImpl ← mkAttributeImplOfEntry entry
return map.insert attrImpl.name attrImpl)
map)
map
@ -400,19 +395,13 @@ def getAttributeImpl (env : Environment) (attrName : Name) : Except String Attri
| some attr => pure attr
| none => throw ("unknown attribute '" ++ toString attrName ++ "'")
def registerAttributeOfDecl (env : Environment) (opts : Options) (attrDeclName : Name) : Except String Environment := do
let attrImpl ← mkAttributeImplOfConstant env opts attrDeclName
if isAttribute env attrImpl.name then
throw ("invalid builtin attribute declaration, '" ++ toString attrImpl.name ++ "' has already been used")
else
return attributeExtension.addEntry env (.decl attrDeclName, attrImpl)
def registerAttributeOfBuilder (env : Environment) (builderId ref : Name) (args : List DataValue) : IO Environment := do
let attrImpl ← mkAttributeImplOfBuilder builderId ref args
let entry := {builderId, ref, args}
let attrImpl ← mkAttributeImplOfEntry entry
if isAttribute env attrImpl.name then
throw (IO.userError ("invalid builtin attribute declaration, '" ++ toString attrImpl.name ++ "' has already been used"))
else
return attributeExtension.addEntry env (.builder builderId ref args, attrImpl)
return attributeExtension.addEntry env (entry, attrImpl)
def Attribute.add (declName : Name) (attrName : Name) (stx : Syntax) (kind := AttributeKind.global) : AttrM Unit := do
let attr ← ofExcept <| getAttributeImpl (← getEnv) attrName