refactor: compile @[extern] via standard pipeline (#13102)

src/Lean/Compiler/ExternAttr.lean

@@ -55,11 +55,6 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
       entries := entries.push <| ExternEntry.inline backend str
   return { entries := entries.toList }
 
--- Forward declaration
-set_option compiler.ignoreBorrowAnnotation true in
-@[extern "lean_add_extern"]
-opaque addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit
-
 builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
   registerParametricAttribute {
     name := `extern
@@ -71,7 +66,7 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
         if let some (.thmInfo ..) := env.find? declName then
           -- We should not mark theorems as extern
           return ()
-        addExtern declName externAttrData
+        compileDecls #[declName]
   }
 
 def getExternAttrData? (env : Environment) (n : Name) : Option ExternAttrData :=

src/Lean/Compiler/IR.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Compiler.IR.AddExtern
 public import Lean.Compiler.IR.Basic
 public import Lean.Compiler.IR.Format
 public import Lean.Compiler.IR.CompilerM

src/Lean/Compiler/IR/AddExtern.lean

@@ -1,86 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Cameron Zwarich
--/
-
-module
-
-prelude
-import Init.While
-import Lean.Compiler.IR.ToIR
-import Lean.Compiler.LCNF.ToImpureType
-import Lean.Compiler.LCNF.ToImpure
-import Lean.Compiler.LCNF.ExplicitBoxing
-import Lean.Compiler.LCNF.Internalize
-public import Lean.Compiler.ExternAttr
-import Lean.Compiler.LCNF.ExplicitRC
-import Lean.Compiler.Options
-
-public section
-
-namespace Lean.IR
-
-set_option compiler.ignoreBorrowAnnotation true in
-@[export lean_add_extern]
-def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit := do
-  if !isPrivateName declName then
-    modifyEnv (Compiler.LCNF.setDeclPublic · declName)
-  let monoDecl ← addMono declName
-  let impureDecls ← addImpure monoDecl
-  addIr impureDecls
-where
-  addMono (declName : Name) : CoreM (Compiler.LCNF.Decl .pure) := do
-    let type ← Compiler.LCNF.getOtherDeclMonoType declName
-    let mut typeIter := type
-    let mut params := #[]
-    let ignoreBorrow := Compiler.compiler.ignoreBorrowAnnotation.get (← getOptions)
-    repeat
-      let .forallE binderName ty b _ := typeIter | break
-      let borrow := !ignoreBorrow && isMarkedBorrowed ty
-      params := params.push {
-        fvarId := (← mkFreshFVarId)
-        type := ty,
-        binderName,
-        borrow
-      }
-      typeIter := b
-    let decl := {
-      name := declName,
-      levelParams := [],
-      value := .extern externAttrData,
-      inlineAttr? := some .noinline,
-      type,
-      params,
-    }
-    decl.saveMono
-    return decl
-
-  addImpure (decl : Compiler.LCNF.Decl .pure) : CoreM (Array (Compiler.LCNF.Decl .impure)) := do
-    let type ← Compiler.LCNF.lowerResultType decl.type decl.params.size
-    let params ← decl.params.mapM fun param =>
-      return { param with type := ← Compiler.LCNF.toImpureType param.type }
-    let decl : Compiler.LCNF.Decl .impure := {
-      name := decl.name,
-      levelParams := decl.levelParams,
-      value := .extern externAttrData
-      inlineAttr? := some .noinline,
-      type,
-      params
-    }
-    Compiler.LCNF.CompilerM.run (phase := .impure) do
-      let decl ← decl.internalize
-      decl.saveImpure
-      let decls ← Compiler.LCNF.addBoxedVersions #[decl]
-      let decls ← Compiler.LCNF.runExplicitRc decls
-      for decl in decls do
-        decl.saveImpure
-        modifyEnv fun env => Compiler.LCNF.recordFinalImpureDecl env decl.name
-      return decls
-
-  addIr (decls : Array (Compiler.LCNF.Decl .impure)) : CoreM Unit := do
-    let decls ← toIR decls
-    logDecls `result decls
-    addDecls decls
-
-end Lean.IR

tests/elab/ctor_layout.lean

@@ -1,4 +1,4 @@
-import Lean.Compiler.IR
+import Lean.Compiler.LCNF
 
 open Lean
 open Lean.IR