GaloisInc / daedalus

The Daedalus data description language
BSD 3-Clause "New" or "Revised" License
63 stars 11 forks source link

Implement `case` inlining #332

Closed yav closed 1 year ago

yav commented 1 year ago

This, together with #329, should help mitigate some references that live too long, which in turn disables some update in place.

More concretely, we'd like to spot patterns where all alternatives return a constructor, and we follow this by doing a case on the result. In that case, we can "inline" the case, for example like this:

block
  let x = { let a = P; ^ (just e) } <| { Q; ^ nothing }
  case x of
     just b -> R
    nothing -> S

becomes:

{ let a = P;  let b = e; R } <| { Q; S }

We have to be a bit careful to not go back and forth with #329 though.

yav commented 1 year ago

The important case inlining to implement is "case of case" (i.e., inline in the branches of a case). While inlining in an alterantive is valid, we don't really want to do that because, in general, we'd like to minimize the backtracking regions, not increase them (that's what #329) is about.