Documentation

Lean.Compiler.Specialize

inductive Lean.Compiler.SpecializeAttributeKind :

Type

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

instance Lean.Compiler.instBEqSpecializeAttributeKind :

BEq Lean.Compiler.SpecializeAttributeKind

Equations

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

instance Lean.Compiler.instInhabitedSpecializeAttributeKind :

Inhabited Lean.Compiler.SpecializeAttributeKind

Equations

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

constant Lean.Compiler.specializeAttrs :

Lean.EnumAttributes Lean.Compiler.SpecializeAttributeKind

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

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

Lean.Compiler.SpecState.addEntry s e = match e with | Lean.Compiler.SpecEntry.info name info => { specInfo := Lean.SMap.insert s.specInfo name info, cache := s.cache } | Lean.Compiler.SpecEntry.cache key fn => { specInfo := s.specInfo, cache := Lean.SMap.insert s.cache key fn }

def Lean.Compiler.SpecState.switch :

Lean.Compiler.SpecState → Lean.Compiler.SpecState

Equations

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

constant Lean.Compiler.specExtension :

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

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)

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

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)

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