Documentation

Lean.Compiler.LCNF.Closure

Dependency collector for code specialization and lambda lifting. #

During code specialization and lambda lifting, we have code C containing free variables. These free variables are in a scope, and we say we are computing C's closure. This module is used to compute the closure.

  • inScope : Lean.FVarIdBool

    inScope x returns true if x is a variable that is not in C.

  • abstract : Lean.FVarIdBool

    If abstract x returns true, we convert x into a closure parameter. Otherwise, we collect the dependencies in the let/fun-declaration too, and include the declaration in the closure. Remark: the lambda lifting pass abstracts all let/fun-declarations.

Instances For

    State for the ClosureM monad.

    • visited : Lean.FVarIdSet

      Set of already visited free variables.

    • Free variables that must become new parameters of the code being specialized.

    • Let-declarations and local function declarations that are going to be "copied" to the code being processed. For example, when this module is used in the code specializer, the let-declarations often contain the instance values. In the current specialization heuristic all let-declarations are ground values (i.e., they do not contain free-variables). However, local function declarations may contain free variables.

      All customers of this module try to avoid work duplication. If a let-declaration is a ground value, it most likely will be computed during compilation time, and work duplication is not an issue.

    Instances For

      Mark a free variable as already visited. We perform a topological sort over the dependencies.

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

        Collect dependencies in parameters. We need this because parameters may contain other type parameters.

        Collect dependencies in the given code. We need this function to be able to collect dependencies in a local function declaration.

        Collect dependencies of a local function declaration.

        Process the given free variable. If it has not already been visited and is in scope, we collect its dependencies.

        Collect dependencies of the given expression.

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