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

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

- inScope : FVarId → Bool

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

- abstract : FVarId → Bool

  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.

- isUnderBinder : Bool

  Indicates whether we are processing terms beneath a binder.

Instances For

source
structure Lean.Compiler.LCNF.Closure.State :
Type

State for the `ClosureM` monad.

- visited : FVarIdHashSet

  Set of already visited free variables.

- params : Array Param

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

- decls : Array CodeDecl

  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

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.Closure.ClosureM (α : Type) :
Type

Monad for implementing the dependency collector.

Equations

- Lean.Compiler.LCNF.Closure.ClosureM = ReaderT Lean.Compiler.LCNF.Closure.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.Closure.State Lean.Compiler.LCNF.CompilerM)

Instances For

source
def Lean.Compiler.LCNF.Closure.markVisited (fvarId : FVarId) :
ClosureM Unit

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

Equations

- Lean.Compiler.LCNF.Closure.markVisited fvarId = modify fun (s : Lean.Compiler.LCNF.Closure.State) => { visited := Std.HashSet.insert s.visited fvarId, params := s.params, decls := s.decls }

Instances For

source
partial def Lean.Compiler.LCNF.Closure.collectParams (params : Array Param) :
ClosureM Unit

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

source
partial def Lean.Compiler.LCNF.Closure.collectArg (arg : Arg) :
ClosureM Unit
source
partial def Lean.Compiler.LCNF.Closure.collectLetValue (e : LetValue) :
ClosureM Unit
source
partial def Lean.Compiler.LCNF.Closure.collectCode (c : Code) :
ClosureM Unit

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

source
partial def Lean.Compiler.LCNF.Closure.collectFunDecl (decl : FunDecl) :
ClosureM Unit

Collect dependencies of a local function declaration.

source
partial def Lean.Compiler.LCNF.Closure.collectFVar (fvarId : FVarId) :
ClosureM Unit

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

source
partial def Lean.Compiler.LCNF.Closure.collectType (type : Expr) :
ClosureM Unit

Collect dependencies of the given expression.

source
def Lean.Compiler.LCNF.Closure.run {α : Type} (x : ClosureM α) (inScope : FVarId → Bool) (abstract : FVarId → Bool := fun (x : FVarId) => true) :
CompilerM (α × Array Param × Array CodeDecl)
Equations

- One or more equations did not get rendered due to their size.

Instances For