Documentation

Lean.Compiler.Specialize

inductive Lean.Compiler.SpecializeAttributeKind:

Type

specialize: Lean.Compiler.SpecializeAttributeKind
nospecialize: Lean.Compiler.SpecializeAttributeKind

instance Lean.Compiler.instInhabitedSpecializeAttributeKind:

Inhabited Lean.Compiler.SpecializeAttributeKind

Equations

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

instance Lean.Compiler.instBEqSpecializeAttributeKind:

BEq Lean.Compiler.SpecializeAttributeKind

Equations

Lean.Compiler.instBEqSpecializeAttributeKind = { beq := [anonymous] }

opaque Lean.Compiler.specializeAttrs:

Lean.EnumAttributes Lean.Compiler.SpecializeAttributeKind

@[export lean_has_specialize_attribute]

def Lean.Compiler.hasSpecializeAttribute (env : Lean.Environment) (n : Lean.Name) :

Equations

Lean.Compiler.hasSpecializeAttribute env n = Lean.Compiler.hasSpecializeAttrAux env Lean.Compiler.SpecializeAttributeKind.specialize n

@[export lean_has_nospecialize_attribute]

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

Equations

Lean.Compiler.hasNospecializeAttribute env n = Lean.Compiler.hasSpecializeAttrAux env Lean.Compiler.SpecializeAttributeKind.nospecialize n

inductive Lean.Compiler.SpecArgKind:

Type

instance Lean.Compiler.instInhabitedSpecArgKind:

Inhabited Lean.Compiler.SpecArgKind

Equations

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

structure Lean.Compiler.SpecInfo:

Type

mutualDecls : List Lean.Name
argKinds : Lean.Compiler.SpecArgKind

instance Lean.Compiler.instInhabitedSpecInfo:

Inhabited Lean.Compiler.SpecInfo

Equations

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

structure Lean.Compiler.SpecState:

Type

specInfo : Lean.SMap Lean.Name Lean.Compiler.SpecInfo
cache : Lean.SMap Lean.Expr Lean.Name

instance Lean.Compiler.instInhabitedSpecState:

Inhabited Lean.Compiler.SpecState

Equations

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

inductive Lean.Compiler.SpecEntry:

Type

info: Lean.Name → Lean.Compiler.SpecInfo → Lean.Compiler.SpecEntry
cache: Lean.Expr → Lean.Name → Lean.Compiler.SpecEntry

instance Lean.Compiler.instInhabitedSpecEntry:

Inhabited Lean.Compiler.SpecEntry

Equations

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

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

Lean.Compiler.SpecState

Equations

One or more equations did not get rendered due to their size.

def Lean.Compiler.SpecState.switch:

Lean.Compiler.SpecState → Lean.Compiler.SpecState

Equations

Lean.Compiler.SpecState.switch _fun_discr = match _fun_discr with | { specInfo := m₁, cache := m₂ } => { specInfo := Lean.SMap.switch m₁, cache := Lean.SMap.switch m₂ }

opaque Lean.Compiler.specExtension:

Lean.SimplePersistentEnvExtension Lean.Compiler.SpecEntry Lean.Compiler.SpecState

@[export lean_add_specialization_info]

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

Lean.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 : Lean.Environment) (fn : Lean.Name) :

Option Lean.Compiler.SpecInfo

Equations

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

@[export lean_cache_specialization]

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

Lean.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 : Lean.Environment) (e : Lean.Expr) :

Option Lean.Name

Equations

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