Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Compiler.LCNF.Specialize.findSpecCache? key = do let a ← Lean.getEnv pure (Lean.PersistentHashMap.find? (Lean.EnvExtension.getState Lean.Compiler.LCNF.Specialize.specCacheExt a) key)
Set of free variables in scope. The "collector" uses this information when collecting dependencies for code specialization.
scope : Lean.FVarIdSetSet of let-declarations in scope that do not depend on parameters.
ground : Lean.FVarIdSetName of the declaration being processed
declName : Lean.Name
Instances For
- decls : Array Lean.Compiler.LCNF.Decl
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Compiler.LCNF.Specialize.withFVar fvarId x = withReader (fun ctx => { scope := Lean.RBTree.insert ctx.scope fvarId, ground := ctx.ground, declName := ctx.declName }) x
Return true if e is a ground term. That is,
it contains only free variables t
Equations
- Lean.Compiler.LCNF.Specialize.isGround e = do let a ← read let s : Lean.FVarIdSet := a.ground pure !Lean.Expr.hasAnyFVar e fun a => !Lean.RBTree.contains s a
Equations
- One or more equations did not get rendered due to their size.
Dependency collector for the code specialization function. #
During code specialization, we select which arguments are going to be used during the specialization.
Then, we have to collect their dependencies. For example, suppose are trying to specialize the following IO.println
and List.forM applications in the following example:
def f xs a.1 :=
let _x.2 := @instMonadEIO IO.Error
let _x.5 := instToStringString
let _x.9 := instToStringNat
let _x.6 := "hello"
let _x.61 := @IO.println String _x.5 _x.6 a.1 -- (*)
cases _x.61
| EStateM.Result.ok a.6 a.7 =>
fun _f.72 _y.69 _y.70 :=
let _x.71 := @IO.println Nat _x.9 _y.69 _y.70 -- (*)
_x.71
let _x.65 := @List.forM (fun α => PUnit → EStateM.Result IO.Error PUnit α) _x.2 Nat xs _f.72 a.7 -- (*)
...
...
For IO.println the SpecArgInfo is [N, I, O, O], i.e., only the first two arguments are considered
for code specialization. The first one is computationally neutral, and the second one is an instance.
For List.forM, we have [N, I, N, O, H]. In this case, the fifth argument (tagged as H) is a function.
Note that the actual List.forM application has 6 arguments, the extra argument comes from the IO monad.
For the first IO.println application, the collector collects _x.5.
For the List.forM, it collects _x.2, _x.9, and _f.72.
The collected values are used to construct a key to identify the specialization. Arguments that were not considered are
replaced with lcErased. The key is used to make sure we don't keep generating the same specialization over and over again.
This is not an optimization, it is essential to prevent the code specializer from looping while specializing recursive functions.
The keys for these two applications are the terms.
@IO.println Nat instToStringNat lcErased lcErased
and
@List.forM
(fun α => PUnit → EStateM.Result IO.Error PUnit α)
(@instMonadEIO IO.Error) Nat lcErased
(fun _y.69 _y.70 =>
let _x.71 := @IO.println Nat instToStringNat _y.69 _y.70;
_x.71)
The keys never contain free variables or loose bound variables.
Set of already visited free variables.
visited : Lean.FVarIdSetFree variables that must become new parameters of the code being specialized.
params : Array Lean.Compiler.LCNF.ParamLet-declarations and local function declarations that are going to be "copied" to the code being specialized. For example, 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.
The current heuristic tries 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.
decls : Array Lean.Compiler.LCNF.CodeDecl
State for the CollectorM monad.
Instances For
Monad for implementing the code specializer dependency collector.
See collect
Mark a free variable as already visited. We perform a topological sort over the dependencies.
Equations
- Lean.Compiler.LCNF.Specialize.Collector.markVisited fvarId = modify fun s => { visited := Lean.RBTree.insert s.visited fvarId, params := s.params, decls := s.decls }
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.
Given the specialization mask paramsInfo and the arguments args,
collect their dependencies, and return an array mask of size paramsInfo.size s.t.
mask[i] = some args[i]ifparamsInfo[i] != .othermask[i] = none, otherwise. That is,maskcontains only the arguments that are contributing to the code specialization. We use this information to compute a "key" to uniquely identify the code specialization, and creating the specialized code.
Equations
- One or more equations did not get rendered due to their size.
Return true if it is worth using arguments args for specialization given the parameter specialization information.
Equations
- One or more equations did not get rendered due to their size.
Convert the given declarations into Expr, and "zeta-reduce" them into body.
This function is used to compute the key that uniquely identifies an code specialization.
Equations
- One or more equations did not get rendered due to their size.
Create the "key" that uniquely identifies a code specialization.
params and decls are the declarations collected by the collect function above.
The result contains the list of universe level parameter names the key that params, decls, and body depends on.
We use this information to create the new auxiliary declaration and resulting application.
Equations
- One or more equations did not get rendered due to their size.
Specialize decl using
us: the universe level used to instantiatedecl.nameargMask: arguments that are being used to specialize the declaration.params: new parameters that arguments inargMaskdepend on.decls: local declarations that arguments inargMaskdepend on.levelParamsNew: the universe level parameters for the new declaration.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Given the specialization mask paramsInfo and the arguments args,
return the arguments that have not been considered for specialization.
Equations
- One or more equations did not get rendered due to their size.
Try to specialize the function application in the given let-declaration.
k is the continuation for the let-declaration.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.