Case desugaring

[klntsky]

Here I'm trying to establish our approach to case desugaring. PIR only supports pattern matching on ADTs, without | guards, let or <- binders in patterns, so we need to remove these. I'll start with an example to illustrate the problem, and then present a more formal algorithm for desugaring.

Consider this expression (let's completely forget about non-exhaustiveness now):

case expr of
  Just x | x == False -> expr0
  Just x | x == True -> expr1
  Nothing -> expr2

Let's peel off the first guard by transforming it into an if-then-else:

case expr of
  Just x ->
    if x == False
    then expr0
    else -- we take the remaining guards and blindly move them down
      case expr of
        Just x | x == True -> expr1
        Nothing -> expr2
  Just x | x == True -> expr1
  Nothing -> expr2

Let's expand the inner pattern guard:

case expr of
  Just x ->
    if x == False
    then expr0
    else
      case expr of
        Just x ->
          if x == True
          then expr1
          else
            case expr of
              Nothing -> expr2
        Nothing -> expr2
  Just x | x == True -> expr1
  Nothing -> expr2

And the last remaining one:

case expr of
  Just x ->
    if x == False
    then expr0
    else
      case expr of
        Just x ->
          if x == True
          then expr1
          else
            case expr of
              Nothing -> expr2
        Nothing -> expr2
  Just x ->
    if x == True then expr1
    else
      case expr of
        Nothing -> expr2
  Nothing -> expr2

Now we have a problem: we've blown up the size of the whole expression by a lot, because we duplicated the alternatives branches (expr0, expr1 and expr2).

How can we fix this?

Every case branch can be seen as a function that accepts variables bound in patterns. Let's introduce a "temporary" datatype for every case expression. The datatype would represent the control flow: it will have as many alternatives as there are execution branches, and every alternative of the ADT will have as many parameters as there are binders in case alternatives.

Consider this generalized form of a case expression:

case scr of
  p_1 (* binds m variables *) -> expr_1
  ..
  p_N (* binds k variables *) -> expr_N

We could construct a type like this:

data PatternsTmp
  = Alternative1 bndrType_1_1 .. bndrType_1_m
  | ..
  | AlternativeN bndrType_N_1 .. bndrType_N_k

Then we will translate the expression, schematically, into something like this:

let
  path = case scr of
    p_1 ->
      (* some code for binding the variables is omitted, see the note below *)
      Alternative1 bndr_1_1 .. bndr_1_m
    .. -> ..
    p_N ->
      AlternativeN bndr_N_1 .. bndr_N_m
in
  case path of
    Alternative1 bndr_1_1 .. bndr_1_m -> expr1
    ..
    AlternativeN bndr_N_1 .. bndr_N_m -> expr_N

Then we will desugard the first case-expression, allowing it to explode in size. But its branches will only contain trivial expressions consisting of just Alternative* constructor calls.

The case expression in the let body will already be desugared by construction.