structure Lean.Compiler.LCNF.LambdaLifting.Context : Type

Context for the LiftM monad.

• liftInstParamOnly : Bool

  If liftInstParamOnly is true, then only local functions that take local instances as parameters are lambda lifted.

• suffix : Name

  Suffix for the new auxiliary declarations being created.

• mainDecl : Decl

  Declaration where lambda lifting is being applied. We use it to provide the "base name" for auxiliary declarations and the flag safe.

• inheritInlineAttrs : Bool

  If true, the lambda-lifted functions inherit the inline attribute from mainDecl. We use this feature to implement @[inline] instance ... and @[always_inline] instance ...

• minSize : Nat

  Only local functions with size > minSize are lambda lifted. We use this feature to implement @[inline] instance ... and @[always_inline] instance ...

• allowEtaContraction : Bool

  Allow for eta contraction instead of lifting to a lambda if possible.

structure Lean.Compiler.LCNF.LambdaLifting.State : Type

State for the LiftM monad.

• decls : Array Decl

  New auxiliary declarations

• nextIdx : Nat

  Next index for generating auxiliary declaration name.

@[reducible, inline]

abbrev Lean.Compiler.LCNF.LambdaLifting.LiftM (α : Type) : Type

Monad for applying lambda lifting.

Equations

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

def Lean.Compiler.LCNF.LambdaLifting.hasInstParam (decl : FunDecl) : CompilerM Bool

Return true if the given declaration takes a local instance as a parameter. We lambda lift this kind of local function declaration before specialization.

Equations

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

def Lean.Compiler.LCNF.LambdaLifting.shouldLift (decl : FunDecl) : LiftM Bool

Return true if the given declaration should be lambda lifted.

Equations

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

partial def Lean.Compiler.LCNF.LambdaLifting.mkAuxDeclName : LiftM Name

def Lean.Compiler.LCNF.LambdaLifting.replaceFunDecl (decl : FunDecl) (value : LetValue) : LiftM LetDecl

Equations

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

def Lean.Compiler.LCNF.LambdaLifting.mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl

Create a new auxiliary declaration. The array closure contains all free variables occurring in decl.

Equations

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

def Lean.Compiler.LCNF.LambdaLifting.etaContractibleDecl? (decl : FunDecl) : LiftM (Option LetDecl)

Equations

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

partial def Lean.Compiler.LCNF.LambdaLifting.visitFunDecl (funDecl : FunDecl) : LiftM FunDecl

partial def Lean.Compiler.LCNF.LambdaLifting.visitCode (code : Code) : LiftM Code

def Lean.Compiler.LCNF.LambdaLifting.main (decl : Decl) : LiftM Decl

Equations

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

def Lean.Compiler.LCNF.Decl.lambdaLifting (decl : Decl) (liftInstParamOnly allowEtaContraction : Bool) (suffix : Name) (inheritInlineAttrs : Bool := false) (minSize : Nat := 0) : CompilerM (Array Decl)

Equations

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

def Lean.Compiler.LCNF.lambdaLifting : Pass

Eliminate all local function declarations.

Equations

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

def Lean.Compiler.LCNF.eagerLambdaLifting : Pass

During eager lambda lifting, we inspect declarations that are not inlineable or instances (doing it everywhere can accidentally introduce mutual recursion which the compiler cannot handle well at the moment). We then lift local function declarations that take local instances as parameters from their body to ensure they are specialized.

Equations

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