# Documentation

Lean.Compiler.LCNF.JoinPoints

• The arity of the candidate

arity : Nat
• The set of candidates that rely on this candidate to be a join point. For a more detailed explanation see the documentation of find

associated :

Info about a join point candidate (a fun declaration) during the find phase.

Instances For
Equations
• All current join point candidates accessible by their FVarId.

• The FVarIds of all fun declarations that were declared within the current fun.

scope :

The state for the join point candidate finder.

Instances For
@[inline]
Equations

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 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.

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.
• The FVarId of the current join point if we are currently inside one.

currentJp? :
• The list of valid candidates for extending the context. This will be all let and fun declarations as well as all jp parameters up until the last fun declaration in the tree.

candidates : Lean.FVarIdSet

The context managed by ExtendM.

Instances For
• 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 ExtendM.

Instances For
@[inline]

The monad for the extendJoinPointContext pass.

Equations
• One or more equations did not get rendered due to their size.

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.

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.

Same as withNewCandidate but with multiple FVarIds.

Equations
• One or more equations did not get rendered due to their size.

Extend the context of the current join point (if we are within one) by fvar if necessary. This is necessary if:

• fvar is 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:
let x := ..
fun f a =>
jp j b =>
let y := x
y

There is no point in extending the context of j by x because 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.

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.

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
• = withReader (fun ctx => { currentJp? := none, candidates := }) ()

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.

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.

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.
Equations
• One or more equations did not get rendered due to their size.
• The variables that are in scope at the time of the definition of the join point.

jpScopes :

Context for ReduceAnalysisM.

Instances For
• A map, that for each join point id contains a map from all (so far) duplicated argument ids to the respective duplicate value

jpJmpArgs :

State for ReduceAnalysisM.

Instances For
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Equations

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.

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.