inductive Lean.Compiler.SpecializeAttributeKind : Type

• specialize : SpecializeAttributeKind
• nospecialize : SpecializeAttributeKind

Instances For

• Lean.Compiler.instBEqSpecializeAttributeKind
• Lean.Compiler.instInhabitedSpecializeAttributeKind

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

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

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

Instances For

• Lean.Compiler.instInhabitedSpecArgKind

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

Instances For

• Lean.Compiler.instInhabitedSpecInfo

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

Instances For

• Lean.Compiler.instInhabitedSpecState

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

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