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 Purity.pure

  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 Purity.pure)

  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.

def Lean.Compiler.LCNF.LambdaLifting.hasInstParam (decl : FunDecl Purity.pure) : 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.

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

Return true if the given declaration should be lambda lifted.

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

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

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

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

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

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

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

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

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

def Lean.Compiler.LCNF.lambdaLifting : Pass

Eliminate all local function declarations.

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.