Documentation

Lean.Compiler.Specialize

inductive Lean.Compiler.SpecializeAttributeKind :

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

Instances For

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 := Lean.Compiler.beqSpecializeAttributeKind✝ }

opaque Lean.Compiler.nospecializeAttr :

Lean.TagAttribute

opaque Lean.Compiler.specializeAttr :

Lean.ParametricAttribute (Array Nat)

def Lean.Compiler.getSpecializationArgs? (env : Lean.Environment) (declName : Lake.Name) :

Option (Array Nat)

Equations

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

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

Equations

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

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

Equations

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

@[export lean_has_specialize_attribute]

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

@[export lean_has_nospecialize_attribute]

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

inductive Lean.Compiler.SpecArgKind :

Instances For

Lean.Compiler.instInhabitedSpecArgKind

instance Lean.Compiler.instInhabitedSpecArgKind :

Inhabited Lean.Compiler.SpecArgKind

Equations

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

structure Lean.Compiler.SpecInfo :

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

Instances For

Lean.Compiler.instInhabitedSpecInfo

instance Lean.Compiler.instInhabitedSpecInfo :

Inhabited Lean.Compiler.SpecInfo

Equations

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

structure Lean.Compiler.SpecState :

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

Instances For

Lean.Compiler.instInhabitedSpecState

instance Lean.Compiler.instInhabitedSpecState :

Inhabited Lean.Compiler.SpecState

Equations

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

inductive Lean.Compiler.SpecEntry :

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

Instances For

Lean.Compiler.instInhabitedSpecEntry

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

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 :

Lean.Compiler.SpecState → Lean.Compiler.SpecState

Equations

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

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 : Lake.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 : Lake.Name) :

Option Lean.Compiler.SpecInfo

Equations

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

@[export lean_cache_specialization]

def Lean.Compiler.cacheSpecialization (env : Lean.Environment) (e : Lean.Expr) (fn : Lake.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 Lake.Name

Equations

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