Documentation

Lean.Compiler.LCNF.LambdaLifting

  • liftInstParamOnly : Bool

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

  • suffix : Lake.Name

    Suffix for the new auxiliary declarations being created.

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

Context for the LiftM monad.

Instances For

    State for the LiftM monad.

    Instances For
      @[inline, reducible]

      Monad for applying lambda lifting.

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

        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

          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

            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
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Eliminate all local function declarations.

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

                      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