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.

Equations

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

structure Lean.Compiler.LCNF.TrivialStructureInfo : Type

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.

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

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

Equations

• Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo = { default := { ctorName := default, numParams := default, fieldIdx := default } }

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

Equations

• Lean.Compiler.LCNF.instReprTrivialStructureInfo = { reprPrec := Lean.Compiler.LCNF.reprTrivialStructureInfo✝ }

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.

Equations

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

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

Equations

• Lean.Compiler.LCNF.getParamTypes type = Lean.Compiler.LCNF.getParamTypes.go type #[]

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

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.

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

  The LCNF type for the mono phase.

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

Equations

• Lean.Compiler.LCNF.instInhabitedMonoTypeExtState = { default := { mono := default } }

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

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

Equations

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