def Lean.Compiler.LCNF.getRelevantCtorFields (ctorName : Name) : 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 : Name
• numParams : Nat
• fieldIdx : Nat

Instances For

• Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo
• Lean.Compiler.LCNF.instReprTrivialStructureInfo

instance Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo : Inhabited TrivialStructureInfo

Equations

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

instance Lean.Compiler.LCNF.instReprTrivialStructureInfo : Repr TrivialStructureInfo

Equations

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

def Lean.Compiler.LCNF.hasTrivialStructure? (declName : Name) : CoreM (Option 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 : Expr) : Array Expr

Equations

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

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

Equations

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

partial def Lean.Compiler.LCNF.toMonoType (type : Expr) : CoreM 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 : Expr) (args : Array Expr) : CoreM Expr

opaque Lean.Compiler.LCNF.monoTypeExt : CacheExtension Name Expr

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.

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

Equations

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