Documentation

Lean.Compiler.LCNF.LambdaLifting

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

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

    liftInstParamOnly : Bool

  • Suffix for the new auxiliary declarations being created.

    suffix : Lean.Name

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

    mainDecl : Lean.Compiler.LCNF.Decl

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

    inheritInlineAttrs : Bool

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

    minSize : Nat

Context for the LiftM monad.

Instances For
    source
    structure Lean.Compiler.LCNF.LambdaLifting.State :
    Type

    State for the LiftM monad.

    Instances For
      source
      @[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.
      source
      def Lean.Compiler.LCNF.LambdaLifting.hasInstParam (decl : Lean.Compiler.LCNF.FunDecl) :
      Lean.Compiler.LCNF.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.
      source
      def Lean.Compiler.LCNF.LambdaLifting.shouldLift (decl : Lean.Compiler.LCNF.FunDecl) :
      Lean.Compiler.LCNF.LambdaLifting.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.
      source
      partial def Lean.Compiler.LCNF.LambdaLifting.mkAuxDeclName :
      Lean.Compiler.LCNF.LambdaLifting.LiftM Lean.Name
      source
      def Lean.Compiler.LCNF.LambdaLifting.mkAuxDecl (closure : Array Lean.Compiler.LCNF.Param) (decl : Lean.Compiler.LCNF.FunDecl) :
      Lean.Compiler.LCNF.LambdaLifting.LiftM Lean.Compiler.LCNF.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.
      source
      def Lean.Compiler.LCNF.LambdaLifting.mkAuxDecl.go (closure : Array Lean.Compiler.LCNF.Param) (decl : Lean.Compiler.LCNF.FunDecl) (nameNew : Lean.Name) (safe : Bool) (inlineAttr? : Option Lean.Compiler.InlineAttributeKind) :
      Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.Decl
      Equations
      • One or more equations did not get rendered due to their size.
      source
      partial def Lean.Compiler.LCNF.LambdaLifting.visitFunDecl (funDecl : Lean.Compiler.LCNF.FunDecl) :
      Lean.Compiler.LCNF.LambdaLifting.LiftM Lean.Compiler.LCNF.FunDecl
      source
      partial def Lean.Compiler.LCNF.LambdaLifting.visitCode (code : Lean.Compiler.LCNF.Code) :
      Lean.Compiler.LCNF.LambdaLifting.LiftM Lean.Compiler.LCNF.Code
      source
      def Lean.Compiler.LCNF.LambdaLifting.main (decl : Lean.Compiler.LCNF.Decl) :
      Lean.Compiler.LCNF.LambdaLifting.LiftM Lean.Compiler.LCNF.Decl
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Decl.lambdaLifting (decl : Lean.Compiler.LCNF.Decl) (liftInstParamOnly : Bool) (suffix : Lean.Name) (inheritInlineAttrs : optParam Bool false) (minSize : optParam Nat 0) :
      Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Decl)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.lambdaLifting :
      Lean.Compiler.LCNF.Pass

      Eliminate all local function declarations.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.eagerLambdaLifting :
      Lean.Compiler.LCNF.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.