Desugaring of Case

[hrutvik]

Currently Case desugars to a series of nested let expressions, e.g.:

exp_of (case x = e of C a b c -> k)
  =>  let x = exp_of e in
        if ... then
          let a = proj 0 x; b = proj 1 x; c = proj 2 x in exp_of c
        else fail

This causes issues when the pattern variables (a,b,c) shadow the Case variable (x), decoupling the binding structure of compiler expressions from semantic expressions. This requires keeping around invariants on a lack of shadowing in various places where we might otherwise hope to avoid them.

@myreen suggests an alternative desugaring which could help:

exp_of (case x = e of C [a,b,c] -> k)
  =>  let x = exp_of e in if ... then (\ a b c. exp_of c) (proj 0 x) (proj 1 x) (proj 2 x) else fail

In this desugaring, x can never be shadowed by any of the pattern variables - we would no longer need to carry around the invariants.

An initial approach could be to define an alternative exp_of and prove equivalence to the old one. Proofs can then choose which one to use. Better yet is to replace the existing exp_of and update all proofs.

[myreen]

An initial approach could be to define an alternative exp_of and prove equivalence to the old one. Proofs can then choose which one to use. Better yet is to replace the existing exp_of and update all proofs.

I suggest going straight for the "replace the existing exp_of and update all proofs", i.e. actually modifying the Case expansion in exp_of, rather than defining an alternative version.

The relevant definition is here. The definition lets_for_def should be deleted, and the use of lets_for in rows_of should be replaced a nesting of lambdas (Lam).

.