inductive Lean.Compiler.SpecializeAttributeKind : Type

• specialize : SpecializeAttributeKind
• nospecialize : SpecializeAttributeKind

instance Lean.Compiler.instInhabitedSpecializeAttributeKind : Inhabited SpecializeAttributeKind

Equations

• Lean.Compiler.instInhabitedSpecializeAttributeKind = { default := Lean.Compiler.SpecializeAttributeKind.specialize }

instance Lean.Compiler.instBEqSpecializeAttributeKind : BEq SpecializeAttributeKind

Equations

• Lean.Compiler.instBEqSpecializeAttributeKind = { beq := Lean.Compiler.beqSpecializeAttributeKind✝ }

opaque Lean.Compiler.nospecializeAttr : TagAttribute

Marks a definition to never be specialized during code generation.

opaque Lean.Compiler.specializeAttr : ParametricAttribute (Array Nat)

Marks a definition to always be specialized during code generation.

Specialization is an optimization in the code generator for generating variants of a function that are specialized to specific parameter values. This is in particular useful for functions that take other functions as parameters: Usually when passing functions as parameters, a closure needs to be allocated that will then be called. Using @[specialize] prevents both of these operations by using the provided function directly in the specialization of the inner function.

@[specialize] can take additional arguments for the parameter names or indices (starting at 1) of the parameters that should be specialized. By default, instance and function parameters are specialized.

def Lean.Compiler.getSpecializationArgs? (env : Environment) (declName : Name) : Option (Array Nat)

Equations

• Lean.Compiler.getSpecializationArgs? env declName = Lean.Compiler.specializeAttr.getParam? env declName

def Lean.Compiler.hasSpecializeAttribute (env : Environment) (declName : Name) : Bool

Equations

• Lean.Compiler.hasSpecializeAttribute env declName = (Lean.Compiler.getSpecializationArgs? env declName).isSome

def Lean.Compiler.hasNospecializeAttribute (env : Environment) (declName : Name) : Bool

Equations

• Lean.Compiler.hasNospecializeAttribute env declName = Lean.Compiler.nospecializeAttr.hasTag env declName

@[export lean_has_specialize_attribute]

partial def Lean.Compiler.hasSpecializeAttributeOld (env : Environment) (n : Name) : Bool

@[export lean_has_nospecialize_attribute]

partial def Lean.Compiler.hasNospecializeAttributeOld (env : Environment) (n : Name) : Bool

inductive Lean.Compiler.SpecArgKind : Type

• fixed : SpecArgKind
• fixedNeutral : SpecArgKind
• fixedHO : SpecArgKind
• fixedInst : SpecArgKind
• other : SpecArgKind

instance Lean.Compiler.instInhabitedSpecArgKind : Inhabited SpecArgKind

Equations

• Lean.Compiler.instInhabitedSpecArgKind = { default := Lean.Compiler.SpecArgKind.fixed }

structure Lean.Compiler.SpecInfo : Type

• mutualDecls : List Name
• argKinds : List SpecArgKind

instance Lean.Compiler.instInhabitedSpecInfo : Inhabited SpecInfo

Equations

• Lean.Compiler.instInhabitedSpecInfo = { default := { mutualDecls := default, argKinds := default } }

structure Lean.Compiler.SpecState : Type

• specInfo : SMap Name SpecInfo
• cache : SMap Expr Name

instance Lean.Compiler.instInhabitedSpecState : Inhabited SpecState

Equations

• Lean.Compiler.instInhabitedSpecState = { default := { specInfo := default, cache := default } }

inductive Lean.Compiler.SpecEntry : Type

• info (name : Name) (info : SpecInfo) : SpecEntry
• cache (key : Expr) (fn : Name) : SpecEntry

instance Lean.Compiler.instInhabitedSpecEntry : Inhabited SpecEntry

Equations

• Lean.Compiler.instInhabitedSpecEntry = { default := Lean.Compiler.SpecEntry.info default default }

def Lean.Compiler.SpecState.addEntry (s : SpecState) (e : SpecEntry) : SpecState

Equations

• s.addEntry (Lean.Compiler.SpecEntry.info name info) = { specInfo := s.specInfo.insert name info, cache := s.cache }
• s.addEntry (Lean.Compiler.SpecEntry.cache key fn) = { specInfo := s.specInfo, cache := s.cache.insert key fn }

def Lean.Compiler.SpecState.switch : SpecState → SpecState

Equations

• { specInfo := m₁, cache := m₂ }.switch = { specInfo := m₁.switch, cache := m₂.switch }

opaque Lean.Compiler.specExtension : SimplePersistentEnvExtension SpecEntry SpecState

@[export lean_add_specialization_info]

def Lean.Compiler.addSpecializationInfo (env : Environment) (fn : Name) (info : SpecInfo) : Environment

Equations

• Lean.Compiler.addSpecializationInfo env fn info = Lean.PersistentEnvExtension.addEntry Lean.Compiler.specExtension env (Lean.Compiler.SpecEntry.info fn info)

@[export lean_get_specialization_info]

def Lean.Compiler.getSpecializationInfo (env : Environment) (fn : Name) : Option SpecInfo

Equations

• Lean.Compiler.getSpecializationInfo env fn = (Lean.Compiler.specExtension.getState env).specInfo.find? fn

@[export lean_cache_specialization]

def Lean.Compiler.cacheSpecialization (env : Environment) (e : Expr) (fn : Name) : Environment

Equations

• Lean.Compiler.cacheSpecialization env e fn = Lean.PersistentEnvExtension.addEntry Lean.Compiler.specExtension env (Lean.Compiler.SpecEntry.cache e fn)

@[export lean_get_cached_specialization]

def Lean.Compiler.getCachedSpecialization (env : Environment) (e : Expr) : Option Name

Equations

• Lean.Compiler.getCachedSpecialization env e = (Lean.Compiler.specExtension.getState env).cache.find? e