- arity : Nat
The arity of the candidate
- associated : Lean.HashSet Lean.FVarId
The set of candidates that rely on this candidate to be a join point. For a more detailed explanation see the documentation of
find
Info about a join point candidate (a fun declaration) during the find phase.
Instances For
Equations
- Lean.Compiler.LCNF.JoinPointFinder.instInhabitedCandidateInfo = { default := { arity := default, associated := default } }
All current join point candidates accessible by their
FVarId.- scope : Lean.HashSet Lean.FVarId
The
FVarIds of allfundeclarations that were declared within the currentfun.
The state for the join point candidate finder.
Instances For
Instances For
Equations
Instances For
Equations
Instances For
Find all fun declarations that qualify as a join point, that is:
- are always fully applied
- are always called in tail position
Where a fun 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.
Furthermore a 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)
f and 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 myjp in f and g would
produce out of scope join point jumps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Replace all join point candidate fun declarations with jp ones
and all calls to them with jmps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
- currentJp? : Option Lean.FVarId
The
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
letandfundeclarations as well as alljpparameters up until the lastfundeclaration in the tree.
The context managed by ExtendM.
Instances For
A map from join point
FVarIds to a respective map from free variables toParams. 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 ExtendM.
Instances For
The monad for the extendJoinPointContext pass.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
fvar.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add a new candidate to the current scope + to the list of candidates
if we are currently within a join point. Then execute x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Same as withNewCandidate but with multiple FVarIds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extend the context of the current join point (if we are within one)
by 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
fvar - the list of candidates contains
fvar. This is because if we have something like:
There is no point in extending the context oflet x := .. fun f a => jp j b => let y := x yjbyxbecause we cannot lift a join point outside of a local function declaration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
of j.2 in j.1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 mergeJpContextIfNecessary.
Equations
- Lean.Compiler.LCNF.JoinPointContextExtender.withNewFunScope decl x = withReader (fun ctx => { currentJp? := none, candidates := ∅ }) (Lean.Compiler.LCNF.ScopeM.withNewScope x)
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- jpScopes : Lean.FVarIdMap Lean.FVarIdSet
The variables that are in scope at the time of the definition of the join point.
Context for ReduceAnalysisM.
Instances For
- jpJmpArgs : Lean.FVarIdMap Lean.Compiler.LCNF.FVarSubst
A map, that for each join point id contains a map from all (so far) duplicated argument ids to the respective duplicate value
State for ReduceAnalysisM.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- Lean.Compiler.LCNF.JoinPointCommonArgs.isInJpScope jp var = do let __do_lift ← read pure (Lean.RBTree.contains (Lean.RBMap.find! __do_lift.jpScopes jp) var)
Instances For
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 ReaderT based
monad stacks.
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 foo
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
without reordering.
Note 2: This transformation is kind of the opposite of JoinPointContextExtender.
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Find all fun declarations in decl that qualify as join points then replace
their definitions and call sites with jp/jmp.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Compiler.LCNF.extendJoinPointContext occurrence phase = Lean.Compiler.LCNF.Pass.mkPerDeclaration `extendJoinPointContext Lean.Compiler.LCNF.Decl.extendJoinPointContext phase occurrence