refactor: extract AttributeImplCore, introduce ParametricAttributeImpl

src/Lean/Attributes.lean

@@ -36,11 +36,15 @@ instance : MonadResolveName AttrM := {
 -- TODO: after we delete the old frontend, we should use `EIO` with a richer exception kind at AttributeImpl.
 -- We must perform a similar modification at `PersistentEnvExtension`
 
-structure AttributeImpl :=
+structure AttributeImplCore :=
   (name : Name)
   (descr : String)
+  (applicationTime := AttributeApplicationTime.afterTypeChecking)
+
+structure AttributeImpl extends AttributeImplCore :=
   (add (decl : Name) (args : Syntax) (persistent : Bool) : AttrM Unit)
-  (applicationTime : AttributeApplicationTime := AttributeApplicationTime.afterTypeChecking)
+  -- TODO: shouldn't be necessary
+  (applicationTime := AttributeApplicationTime.afterTypeChecking)
 
 instance : Inhabited AttributeImpl :=
   ⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure () }⟩
@@ -315,13 +319,15 @@ structure ParametricAttribute (α : Type) :=
   (attr : AttributeImpl)
   (ext  : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
 
-def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr : String)
-    (getParam : Name → Syntax → AttrM α)
-    (afterSet : Name → α → AttrM Unit := fun env _ _ => pure ())
-    (appTime := AttributeApplicationTime.afterTypeChecking)
-    : IO (ParametricAttribute α) := do
+structure ParametricAttributeImpl (α : Type) extends AttributeImplCore :=
+  (getParam : Name → Syntax → AttrM α)
+  (afterSet : Name → α → AttrM Unit := fun env _ _ => pure ())
+  -- TODO: shouldn't be necessary
+  (applicationTime := AttributeApplicationTime.afterTypeChecking)
+
+def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
   let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
-    name            := name,
+    name            := impl.name,
     mkInitial       := pure {},
     addImportedFn   := fun _ _ => pure {},
     addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
@@ -330,19 +336,16 @@ def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr
       r.qsort (fun a b => Name.quickLt a.1 b.1),
     statsFn         := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
   }
-  let attrImpl : AttributeImpl := {
-    name  := name,
-    descr := descr,
-    applicationTime := appTime,
+  let attrImpl : AttributeImpl := { impl with
     add   := fun decl args persistent => do
-      unless persistent do throwError! "invalid attribute '{name}', must be persistent"
+      unless persistent do throwError! "invalid attribute '{impl.name}', must be persistent"
       let env ← getEnv
       unless (env.getModuleIdxFor? decl).isNone do
-        throwError! "invalid attribute '{name}', declaration is in an imported module"
-      let val ← getParam decl args
+        throwError! "invalid attribute '{impl.name}', declaration is in an imported module"
+      let val ← impl.getParam decl args
       let env' := ext.addEntry env (decl, val)
       setEnv env'
-      try afterSet decl val catch _ => setEnv env
+      try impl.afterSet decl val catch _ => setEnv env
   }
   registerBuiltinAttribute attrImpl
   pure { attr := attrImpl, ext := ext }

src/Lean/Compiler/ExportAttr.lean

@@ -18,12 +18,16 @@ private def isValidCppName : Name → Bool
 | _                           => false
 
 builtin_initialize exportAttr : ParametricAttribute Name ←
-registerParametricAttribute `export "name to be used by code generators" $ fun _ stx =>
-  match attrParamSyntaxToIdentifier stx with
-  | some exportName =>
-    if isValidCppName exportName then pure exportName
-    else throwError "invalid 'export' function name, is not a valid C++ identifier"
-  | _ => throwError "unexpected kind of argument"
+registerParametricAttribute {
+  name := `export,
+  descr := "name to be used by code generators",
+  getParam := fun _ stx =>
+    match attrParamSyntaxToIdentifier stx with
+    | some exportName =>
+      if isValidCppName exportName then pure exportName
+      else throwError "invalid 'export' function name, is not a valid C++ identifier"
+    | _ => throwError "unexpected kind of argument",
+}
 
 @[export lean_get_export_name_for]
 def getExportNameFor (env : Environment) (n : Name) : Option Name :=

src/Lean/Compiler/ExternAttr.lean

@@ -80,15 +80,18 @@ private def syntaxToExternAttrData (s : Syntax) : ExceptT String Id ExternAttrDa
 constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment
 
 builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
-  registerParametricAttribute `extern "builtin and foreign functions"
-    (fun _ stx => ofExcept $ syntaxToExternAttrData stx)
-    (fun declName _ => do
+  registerParametricAttribute {
+    name := `extern,
+    descr := "builtin and foreign functions",
+    getParam := fun _ stx => ofExcept $ syntaxToExternAttrData stx,
+    afterSet := fun declName _ => do
       let env ← getEnv
       if env.isProjectionFn declName || env.isConstructor declName then do
         env ← ofExcept $ addExtern env declName
         setEnv env
       else
-        pure ())
+        pure (),
+  }
 
 @[export lean_get_extern_attr_data]
 def getExternAttrData (env : Environment) (n : Name) : Option ExternAttrData :=

src/Lean/Compiler/ImplementedByAttr.lean

@@ -9,16 +9,19 @@ import Lean.MonadEnv
 
 namespace Lean.Compiler
 
-builtin_initialize implementedByAttr : ParametricAttribute Name ←
-registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) function that implements opaque constant" fun declName stx => do
-  let decl ← getConstInfo declName
-  match attrParamSyntaxToIdentifier stx with
-  | some fnName =>
-    let fnName ← resolveGlobalConstNoOverload fnName;
-    let fnDecl ← getConstInfo fnName;
-    if decl.type == fnDecl.type then pure fnName
-    else throwError! "invalid function '{fnName}' type mismatch"
-  | _ => throwError "expected identifier"
+builtin_initialize implementedByAttr : ParametricAttribute Name ← registerParametricAttribute {
+  name := `implementedBy,
+  descr := "name of the Lean (probably unsafe) function that implements opaque constant",
+  getParam := fun declName stx => do
+    let decl ← getConstInfo declName
+    match attrParamSyntaxToIdentifier stx with
+    | some fnName =>
+      let fnName ← resolveGlobalConstNoOverload fnName
+      let fnDecl ← getConstInfo fnName
+      if decl.type == fnDecl.type then pure fnName
+      else throwError! "invalid function '{fnName}' type mismatch"
+    | _ => throwError "expected identifier",
+}
 
 @[export lean_get_implemented_by]
 def getImplementedBy (env : Environment) (declName : Name) : Option Name :=

src/Lean/Compiler/InitAttr.lean

@@ -23,22 +23,26 @@ match getIOTypeArg type with
 | _ => false
 
 def registerInitAttr (attrName : Name) : IO (ParametricAttribute Name) :=
-registerParametricAttribute attrName "initialization procedure for global references" fun declName stx => do
-  let decl ← getConstInfo declName
-  match attrParamSyntaxToIdentifier stx with
-  | some initFnName =>
-    let initFnName ← resolveGlobalConstNoOverload initFnName
-    let initDecl ← getConstInfo initFnName
-    match getIOTypeArg initDecl.type with
-    | none => throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO <type>`")
-    | some initTypeArg =>
-      if decl.type == initTypeArg then pure initFnName
-      else throwError ("initialization function '" ++ initFnName ++ "' type mismatch")
-  | _ => match stx with
-    | Syntax.missing =>
-      if isIOUnit decl.type then pure Name.anonymous
-      else throwError "initialization function must have type `IO Unit`"
-    | _ => throwError "unexpected kind of argument"
+registerParametricAttribute {
+  name := `init,
+  descr := "initialization procedure for global references",
+  getParam := fun declName stx => do
+    let decl ← getConstInfo declName
+    match attrParamSyntaxToIdentifier stx with
+    | some initFnName =>
+      let initFnName ← resolveGlobalConstNoOverload initFnName
+      let initDecl ← getConstInfo initFnName
+      match getIOTypeArg initDecl.type with
+      | none => throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO <type>`")
+      | some initTypeArg =>
+        if decl.type == initTypeArg then pure initFnName
+        else throwError ("initialization function '" ++ initFnName ++ "' type mismatch")
+    | _ => match stx with
+      | Syntax.missing =>
+        if isIOUnit decl.type then pure Name.anonymous
+        else throwError "initialization function must have type `IO Unit`"
+      | _ => throwError "unexpected kind of argument",
+}
 
 builtin_initialize regularInitAttr : ParametricAttribute Name ← registerInitAttr `init
 builtin_initialize builtinInitAttr : ParametricAttribute Name ← registerInitAttr `builtinInit

src/Lean/Meta/RecursorInfo.lean

@@ -269,11 +269,14 @@ match cinfo with
 | _                        => mkRecursorInfoAux cinfo majorPos?
 
 builtin_initialize recursorAttribute : ParametricAttribute Nat ←
-  registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise"
-    (fun _ stx => ofExcept $ syntaxToMajorPos stx)
-    (fun declName majorPos => do
-      (mkRecursorInfoCore declName (some majorPos)).run'
-      pure ())
+registerParametricAttribute {
+  name := `recursor,
+  descr := "user defined recursor, numerical parameter specifies position of the major premise",
+  getParam := fun _ stx => ofExcept $ syntaxToMajorPos stx,
+  afterSet := fun declName majorPos => do
+    (mkRecursorInfoCore declName (some majorPos)).run'
+    pure ()
+}
 
 def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=
 recursorAttribute.getParam env declName