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

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.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.mkAuxDecl.go (closure : Array Param) (decl : FunDecl) (nameNew : Name) (safe : Bool) (inlineAttr? : Option InlineAttributeKind) : Internalize.InternalizeM Decl

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