source
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 ...`

Instances For

source
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.

Instances For

source
@[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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
partial def Lean.Compiler.LCNF.LambdaLifting.mkAuxDeclName :
LiftM Name
source
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.

Instances For

source
partial def Lean.Compiler.LCNF.LambdaLifting.visitFunDecl (funDecl : FunDecl) :
LiftM FunDecl
source
partial def Lean.Compiler.LCNF.LambdaLifting.visitCode (code : Code) :
LiftM Code
source
def Lean.Compiler.LCNF.LambdaLifting.main (decl : Decl) :
LiftM Decl
Equations

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

Instances For

source
def Lean.Compiler.LCNF.Decl.lambdaLifting (decl : Decl) (liftInstParamOnly : 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.

Instances For

source
def Lean.Compiler.LCNF.lambdaLifting :
Pass

Eliminate all local function declarations.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.eagerLambdaLifting :
Pass

During eager lambda lifting, we lift

- All local function declarations from instances (motivation: make sure it is cheap to inline them later)
- Local function declarations that take local instances as parameters (motivation: ensure they are specialized)

Equations

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

Instances For