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

• 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

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

• 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

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.