IntersectMBO / plutus

The Plutus language implementation and tools
Apache License 2.0
1.57k stars 480 forks source link

UPLC case-of-case improvements #5966

Open effectfully opened 6 months ago

effectfully commented 6 months ago

After #5960 we have some left-overs:

  1. this example is incorrect and needs to be updated:
{- | A special case of case-of-case optimisation: transforms

@
    case ((force ifThenElse) b (constr t) (constr f)) alts
@

into

@
    force ifThenElse b (case (constr t) alts) (case (constr f) alts)
@

This is always an improvement.
-}

Plus, there's no explanation of what we do and why we do it.

  1. the PR added generation of extra force-delay pairs, why don't we see them in the existing golden tests? Those that were affected by the original PR introducing case-of-case? UPD: @ana-pantilie figured it out: it's because we know how case-of-case in PIR and so no suitable expression survives compilation of PIR to be transformed at the UPLC level. Thanks Ana!

  2. should we avoid generating force-delay pairs when branches are pure?

  3. what about PIR, do we have the same issue there that was fixed for UPLC?

  4. UPLC case-of-case is exponential in the same way as PIR case-of-case (see this and below).

zliu41 commented 6 months ago

Plus, there's no explanation of what we do and why we do it.

The name of the transformation is self-explanatory: this is basically case-of-case transformation. The reason it is useful is because it can trigger case-of-known-constructor transformation on case (constr t) and case (constr f).

zliu41 commented 6 months ago

should we avoid generating force-delay pairs when branches are pure?

Yes, I think we already do that when compiling cases. Forces and delays are only added if at least one of the branches isn't pure.

effectfully commented 6 months ago

The name of the transformation is self-explanatory: this is basically case-of-case transformation. The reason it is useful is because it can trigger case-of-known-constructor transformation on case (constr t) and case (constr f).

The name is self-explanatory, but the force-delay caveat was so obscure that if went through the review process without anybody noticing. This must be documented.

Yes, I think we already do that when compiling cases.

In the UPLC case-of-case transformation? Where?

zliu41 commented 6 months ago

In the UPLC case-of-case transformation? Where?

I think it's in the compilation of Case in GHC Core into PIR, but it's the same idea.

effectfully commented 6 months ago

Ah, I misunderstood, I thought you were saying it was already implemented for UPLC case-of-case.