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

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

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

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

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

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.

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

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

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

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.

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

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

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

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

structure Lean.Compiler.LCNF.CtorLayout : Type

• ctorInfo : CtorInfo
• fieldInfo : Array CtorFieldInfo

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorLayout : Inhabited CtorLayout

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

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

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.

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.