From 4932dbc65dc8a459ab8cec1c13c6bcae06d951ac Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 1 Oct 2024 15:34:12 +0200
Subject: [PATCH] refactor: dead code AttributeExtensionOLeanEntry.decl (#5496)

The constructor `AttributeExtensionOLeanEntry.decl` and related code
seems to be unused, and has been unused since its introduction in
a77598f7cfcb058da41cf3af8a7120aeca68fe8c three years ago. Probably worth
removing (and changing the now one-constructor inductive into a
structure).
---
 src/Lean/Attributes.lean | 37 +++++++++++++------------------------
 1 file changed, 13 insertions(+), 24 deletions(-)

diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 32b7e8e18a..4a06fbc2c7 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -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