The arity of the candidate
arity : NatThe set of candidates that rely on this candidate to be a join point. For a more detailed explanation see the documentation of
findassociated : Lean.HashSet Lean.FVarId
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.The
FVarIds of allfundeclarations that were declared within the currentfun.scope : Lean.HashSet Lean.FVarId
The state for the join point candidate finder.
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.
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.
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.