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.

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.

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.

@[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)

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 }

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.

partial def Lean.Compiler.LCNF.Closure.collectArg (arg : Arg) : ClosureM Unit

partial def Lean.Compiler.LCNF.Closure.collectLetValue (e : LetValue) : ClosureM Unit

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.

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

Collect dependencies of a local function declaration.

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.

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

Collect dependencies of the given expression.

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.