def Lean.Compiler.LCNF.setHasTrivialImpureStructure? (declName : Name) : CoreM Unit

Eagerly computes and persists the impure trivial-structure info of declName; see compileDecls.

Equations

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

def Lean.Compiler.LCNF.hasTrivialImpureStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)

Equations

• Lean.Compiler.LCNF.hasTrivialImpureStructure? declName = Lean.Compiler.LCNF.Irrelevant.hasTrivialStructure? Lean.Compiler.LCNF.impureTrivialStructureInfoExt✝ declName

def Lean.Compiler.LCNF.setImpureType (name : Name) : CoreM Unit

Eagerly computes and persists the IR type of inductive name; see compileDecls.

Equations

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

def Lean.Compiler.LCNF.nameToImpureType (name : Name) : CoreM Expr

Returns the IR (impure) type representation of name. Requires compileDecls to have been run for inductive type name.

Equations

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

partial def Lean.Compiler.LCNF.toImpureType (type : Expr) : CoreM Expr

inductive Lean.Compiler.LCNF.CtorFieldInfo : Type

• erased : CtorFieldInfo
• object (i : Nat) (type : Expr) : CtorFieldInfo
• usize (i : Nat) : CtorFieldInfo
• scalar (sz offset : Nat) (type : Expr) : CtorFieldInfo
• void : CtorFieldInfo
• spilled (depth i : Nat) (type : Expr) : CtorFieldInfo

  An object field that does not fit into the constructor object. It is stored at index i of the spill object reached by following the field at spillLinkIdx depth times.

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorFieldInfo : Inhabited CtorFieldInfo

Equations

• Lean.Compiler.LCNF.instInhabitedCtorFieldInfo = { default := Lean.Compiler.LCNF.instInhabitedCtorFieldInfo.default }

def Lean.Compiler.LCNF.CtorFieldInfo.spillDepth : CtorFieldInfo → Nat

The number of spill objects to follow to reach the field.

Equations

• (Lean.Compiler.LCNF.CtorFieldInfo.spilled depth i type).spillDepth = depth
• x✝.spillDepth = 0

def Lean.Compiler.LCNF.spillLinkIdx : Nat

The index of the object field holding the next spill object. A constructor with too many object fields for one constructor object keeps the first spillLinkIdx of them and stores the others in a chain of spill objects, each of which holds the next spillLinkIdx of them.

Equations

• Lean.Compiler.LCNF.spillLinkIdx = Lean.maxCtorNumObjs - 1

def Lean.Compiler.LCNF.numSpillObjs (numObjs : Nat) : Nat

The number of spill objects of a constructor with numObjs object fields.

Equations

• Lean.Compiler.LCNF.numSpillObjs numObjs = if numObjs ≤ Lean.maxCtorNumObjs then 0 else (numObjs - 1) / Lean.Compiler.LCNF.spillLinkIdx

def Lean.Compiler.LCNF.spillCtorInfo (ctorName : Name) (size : Nat) : CtorInfo

The constructor information of a spill object of constructor ctorName with size fields.

Equations

• Lean.Compiler.LCNF.spillCtorInfo ctorName size = { name := ctorName ++ `spill, cidx := 0, size := size, usize := 0, ssize := 0 }

structure Lean.Compiler.LCNF.CtorLayout : Type

• ctorInfo : CtorInfo
• fieldInfo : Array CtorFieldInfo

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorLayout : Inhabited CtorLayout

Equations

• Lean.Compiler.LCNF.instInhabitedCtorLayout = { default := Lean.Compiler.LCNF.instInhabitedCtorLayout.default }

def Lean.Compiler.LCNF.setCtorLayout (ctorName : Name) : CoreM Unit

Eagerly computes and persists the layout of constructor ctorName; see compileDecls.

Equations

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

def Lean.Compiler.LCNF.getCtorLayout (ctorName : Name) : CoreM CtorLayout

Returns the runtime layout of constructor ctorName. Requires compileDecls to have been run for its inductive type.

Equations

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

def Lean.Compiler.LCNF.compileInductives (typeNames : Array Name) : CoreM Unit

Eagerly computes and persists all cross-module compiler caches for the inductive types typeNames (and their constructors) in their defining module; run from compileDecls.

Equations

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