Mutually recursive PIR function inlining#7688
Conversation
| [ (constr 1 | ||
| [ cse | ||
| , cse ]) ])) | ||
| , (constr 1 |
There was a problem hiding this comment.
I think we have issue similar to #7681 here. CSE not doing it's job probably due to some rename happening
| match_Nat n {Bool} True (\(p : Nat) -> odd p)) | ||
| (\(n : Nat) -> | ||
| match_Nat n {Bool} False (\(p : Nat) -> even p))))) | ||
| (\(s : |
There was a problem hiding this comment.
this was the existing test cases that was originally inefficient due to mutual recursion but now more efficient.
zliu41
left a comment
zliu41
left a comment
There was a problem hiding this comment.
Can you check if this solves the problem described in Note [Making the cons case non-strict in caseList and caseList']?
| asRecBinding = \case | ||
| TermBind bindAnn strictness decl rhs | ||
| | let arity = rhsArity rhs | ||
| , not (null arity) -> |
There was a problem hiding this comment.
Why do you require this condition? Can you just use the purity analysis instead?
There was a problem hiding this comment.
I think if it's a non-lambda term, it should be handled by inliner instead.
| rhs' <- PLC.rename helperRhs | ||
| pure $ case saturates args (rhsArity rhs') of | ||
| Just Saturated -> fillAppContext rhs' args | ||
| _ -> term' |
There was a problem hiding this comment.
I don't think you need to give up if it is OverSaturated?
| This works across independent subgroups within the same @let rec@, e.g. | ||
| @{even, odd, f, g}@ where @{even, odd}@ and @{f, g}@ are separate cycles. | ||
|
|
||
| No beta reduction is performed here; the resulting unsaturated applications |
There was a problem hiding this comment.
| No beta reduction is performed here; the resulting unsaturated applications | |
| No beta reduction is performed here; the resulting applications |
The resulting application isn't necessarily unsaturated, is it?
| Nothing -> pure group | ||
|
|
||
| {-| Find a helper eligible for inlining: not a root, not self-recursive, | ||
| called from exactly one sibling, and used exactly once in that sibling. -} |
There was a problem hiding this comment.
These "exactly one" conditions seem quite restrictive. Can you use similar criteria as the main inliner - e.g., if it is used exactly once, then it's always OK. Otherwise, it is OK if costIsAcceptable and sizeIsAcceptable.
There was a problem hiding this comment.
nice. I'll do this
| pure (host, helper) | ||
|
|
||
| {-| Inline all saturated calls to the helper within the host's RHS. | ||
| If successful (all references eliminated), remove the helper from the group. -} |
There was a problem hiding this comment.
Inline all saturated calls to the helper
Doesn't findCandidate guarantee that there's exactly one callsite?
And why must the callsite be saturated?
| Just (hostKey, helperKey) -> | ||
| tryInline group hostKey helperKey >>= \case | ||
| Just group' -> collapseRecGroup group' | ||
| Nothing -> pure group |
There was a problem hiding this comment.
Is it possible that another candidate in the group can be inlined?
2 participants
New optimization pass that will inline mutually recursive PIR functions when they satisfy below criteria.
Given chain of mutually recursive functions f, g, and h, we inline when