- arity : Nat
The arity of the candidate
The set of candidates that rely on this candidate to be a join point. For a more detailed explanation see the documentation of
Info about a join point candidate (a
fun declaration) during the find phase.
All current join point candidates accessible by their
FVarIds of all
fundeclarations that were declared within the current
The state for the join point candidate finder.
fun declarations that qualify as a join point, that is:
- are always fully applied
- are always called in tail position
f is in tail position iff it is called as follows:
let res := f arg res
The majority (if not all) tail calls will be brought into this form by the simplifier pass.
fun disqualifies as a join point if turning it into a join
point would turn a call to it into an out of scope join point.
This can happen if we have something like:
def test (b : Bool) (x y : Nat) : Nat := fun myjp x => Nat.add x (Nat.add x x) fun f y => let x := Nat.add y y myjp x fun f y => let x := Nat.mul y y myjp x cases b (f x) (g y)
g can be detected as a join point right away, however
myjp can only ever be detected as a join point after we have established
this. This is because otherwise the calls to
produce out of scope join point jumps.
FVarIdof the current join point if we are currently inside one.
- candidates : Lean.FVarIdSet
The list of valid candidates for extending the context. This will be all
fundeclarations as well as all
jpparameters up until the last
fundeclaration in the tree.
The context managed by
A map from join point
FVarIds to a respective map from free variables to
Params. The free variables in this map are the once that the context of said join point will be extended by by passing in the respective parameter.
The state managed by
The monad for the
Replace a free variable if necessary, that is:
- It is in the list of candidates
- We are currently within a join point (if we are within a function there cannot be a need to replace them since we dont extend their context)
- Said join point actually has a replacement parameter registered.
otherwise just return
Add a new candidate to the current scope + to the list of candidates
if we are currently within a join point. Then execute
withNewCandidate but with multiple
Extend the context of the current join point (if we are within one)
fvar if necessary.
This is necessary if:
fvaris not in scope (that is, was declared outside of the current jp)
- we have not already extended the context by
- the list of candidates contains
fvar. This is because if we have something like:
There is no point in extending the context of
let x := .. fun f a => jp j b => let y := x y
xbecause we cannot lift a join point outside of a local function declaration.
Merge the extended context of two join points if necessary. That is if we have a structure such as:
jp j.1 ... => jp j.2 .. => ... ...
And we are just done visiting
j.2 we want to extend the context of
j.1 by all free variables that the context of
j.2 was extended by
as well because we need to drag these variables through at the call sites
We call this whenever we enter a new local function. It clears both the
current join point and the list of candidates since we cant lift join
points outside of functions as explained in
We call this whenever we enter a new join point. It will set the current join point and extend the list of candidates by all of the parameters of the join point. This is so in the case of nested join points that refer to parameters of the current one we extend the context of the nested join points by said parameters.
We call this whenever we visit a new arm of a cases statement. It will back up the current scope (since we are doing a case split and want to continue with other arms afterwards) and add all of the parameters of the match arm to the list of candidates.
Use all of the above functions to find free variables declared outside of join points that said join points can be reasonaly extended by. Reasonable meaning that in case the current join point is nested within a function declaration we will not extend it by free variables declared before the function declaration because we cannot lift join points outside of function declarations.
All of this is done to eliminate dependencies of join points onto their position within the code so we can pull them out as far as possible, hopefully enabling new inlining possibilities in the next simplifier run.
The variables that are in scope at the time of the definition of the join point.
A map, that for each join point id contains a map from all (so far) duplicated argument ids to the respective duplicate value
Take a look at each join point and each of their call sites. If all call sites of a join point have one or more arguments in common, for example:
jp _jp.1 a b c => ... ... cases foo | n1 => jmp _jp.1 d e f | n2 => jmp _jp.1 g e h
We can get rid of the common argument in favour of inlining it directly
into the join point (in this case the
e). This reduces the amount of
arguments we have to pass around drastically for example in
Note 1: This transformation can in certain niche cases obtain better results. For example:
jp foo a b => .. let x := ... cases discr | n1 => jmp foo x y | n2 => jmp foo x z
Here we will not collapse the
x since it is defined after the join point
and thus not accessible for substitution yet. We could however reorder the code in
such a way that this is possible, this is currently not done since we observe
than in praxis most of the applications of this transformation can occur naturally
Note 2: This transformation is kind of the opposite of
However we still benefit from the extender because in the
simp run after it
we might be able to pull join point declarations further up in the hierarchy
of nested functions/join points which in turn might enable additional optimizations.
After we have performed all of these optimizations we can take away the
(remaining) common arguments and end up with nicely floated and optimized
code that has as little arguments as possible in the join points.