def Lean.Compiler.LCNF.getRelevantCtorFields (ctorName : Lake.Name) : Lean.CoreM (Array Bool)

Given a constructor, return a bitmask m s.t. m[i] is true if field i is computationally relevant.

structure Lean.Compiler.LCNF.TrivialStructureInfo : Type

• ctorName : Lake.Name
• numParams : Nat
• fieldIdx : Nat

We say a structure has a trivial structure if it has not builtin support in the runtime, it has only one constructor, and this constructor has only one relevant field.

instance Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo : Inhabited Lean.Compiler.LCNF.TrivialStructureInfo

instance Lean.Compiler.LCNF.instReprTrivialStructureInfo : Repr Lean.Compiler.LCNF.TrivialStructureInfo

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

Return some fieldIdx if declName is the name of an inductive datatype s.t.

• It does not have builtin support in the runtime.
• It has only one constructor.
• This constructor has only one computationally relevant field.

def Lean.Compiler.LCNF.getParamTypes (type : Lean.Expr) : Array Lean.Expr

def Lean.Compiler.LCNF.getParamTypes.go (type : Lean.Expr) (r : Array Lean.Expr) : Array Lean.Expr

Equations

• Lean.Compiler.LCNF.getParamTypes.go (Lean.Expr.forallE binderName d b binderInfo) r = Lean.Compiler.LCNF.getParamTypes.go b (Array.push r d)
• Lean.Compiler.LCNF.getParamTypes.go type r = r

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

Convert a LCNF type from the base phase to the mono phase.

LCNF types in the mono phase do not have dependencies, and universe levels have been erased.

The type contains only → and constants.

partial def Lean.Compiler.LCNF.toMonoType.visitApp (f : Lean.Expr) (args : Array Lean.Expr) : Lean.CoreM Lean.Expr

structure Lean.Compiler.LCNF.MonoTypeExtState : Type

• mono : Lean.PHashMap Lake.Name Lean.Expr

  The LCNF type for the mono phase.

State for the environment extension used to save the LCNF mono phase type for declarations that do not have code associated with them. Example: constructors, inductive types, foreign functions.

instance Lean.Compiler.LCNF.instInhabitedMonoTypeExtState : Inhabited Lean.Compiler.LCNF.MonoTypeExtState

opaque Lean.Compiler.LCNF.monoTypeExt : Lean.EnvExtension Lean.Compiler.LCNF.MonoTypeExtState

def Lean.Compiler.LCNF.getOtherDeclMonoType (declName : Lake.Name) : Lean.CoreM Lean.Expr