Documentation

Lean.Compiler.Specialize

inductive Lean.Compiler.SpecializeAttributeKind :

specialize : SpecializeAttributeKind
nospecialize : SpecializeAttributeKind

Instances For

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 :

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) :

Equations

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

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

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) :

@[export lean_has_nospecialize_attribute]

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

inductive Lean.Compiler.SpecArgKind :

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

Instances For

Lean.Compiler.instInhabitedSpecArgKind

instance Lean.Compiler.instInhabitedSpecArgKind :

Inhabited SpecArgKind

Equations

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

structure Lean.Compiler.SpecInfo :

mutualDecls : List Name
argKinds : List SpecArgKind

Instances For

Lean.Compiler.instInhabitedSpecInfo

instance Lean.Compiler.instInhabitedSpecInfo :

Inhabited SpecInfo

Equations

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

structure Lean.Compiler.SpecState :

specInfo : SMap Name SpecInfo
cache : SMap Expr Name

Instances For

Lean.Compiler.instInhabitedSpecState

instance Lean.Compiler.instInhabitedSpecState :

Inhabited SpecState

Equations

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

inductive Lean.Compiler.SpecEntry :

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

Instances For

Lean.Compiler.instInhabitedSpecEntry

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) :

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) :

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) :

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) :

Equations

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