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 : Lean.FVarId → Bool

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

• abstract : Lean.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.

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

State for the ClosureM monad.

• visited : Lean.FVarIdSet

  Set of already visited free variables.

• params : Array Lean.Compiler.LCNF.Param

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

• decls : Array Lean.Compiler.LCNF.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 : Lean.FVarId) : Lean.Compiler.LCNF.Closure.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 := s.visited.insert fvarId, params := s.params, decls := s.decls }

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

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

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

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

partial def Lean.Compiler.LCNF.Closure.collectCode (c : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Closure.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 : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.Closure.ClosureM Unit

Collect dependencies of a local function declaration.

partial def Lean.Compiler.LCNF.Closure.collectFVar (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Closure.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 : Lean.Expr) : Lean.Compiler.LCNF.Closure.ClosureM Unit

Collect dependencies of the given expression.

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