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
This module is used to compute the closure.
xis a variable that is not in
true, we convert
xinto a closure parameter. Otherwise, we collect the dependecies in the
fun-declaration too, and include the declaration in the closure. Remark: the lambda lifting pass abstracts all
- 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.
State for the