(thanks to Bernie Pope for letting me take advantage of his efforts with notation and abstract syntax)

### An abstract syntax

For the purpose of exploring the rules we need an abstract syntax. Below is one for a simple core functional language:

```
Decls(D) --> x :: T | x = E | data f a1 .. an = K1 .. Km
Constructors(K) --> k T1 .. Tn
Types(T) --> f | a | T1 T2
Expressions(E) --> x | k | E1 E2 | let D1 .. Dn in E | case E of A1 .. An | \y1 .. yn -> E
Alts(A) --> p -> E
Pats(P) --> x | k P1 .. Pn
```

### Notation

Double square brackets denote the transformation function, which has two arguments: the expression itself and a list of bindings in scope. For instance:

` [[E ]]_b ==> [[E' ]]_b'`

means transform expression E with b as the list of bindings in scope into E' with the new list l'

Double brackets denote the auxiliary binding capture function, which takes an expression and returns a list of the variables bound in it:

` {{ E }} ==> x1 .. xn | []`

### breakpointJump desugaring

The main role of the desugaring, as shown by the rules, is injecting the explicit list of local bindings.

In the rules below <breakpoint> and <breakpointJump> are placeholders for the several breakpoint flavors. Each flavor of breakpoint has a corresponding jump function:

```
breakpoint - breakpointJump
breakpointCond - breakpointJumpCond
breakpointAuto - breakpointJumpAuto
```

The <ptr b> placeholder denotes a pointer to the compiler datastructures for b, which in GHC are values of type compiler/basictypes/Id.hs.

The <srcloc x> placeholder denotes the source code location information for the expression x.

```
Declarations:
[[x :: T ]]_b ==> x :: T
[[x = E ]]_b ==> x = [[E ]]_b
[[data f a1 .. an = K1 .. Km ]]_b
==> data f a1 .. an = K1 .. Km
{{ x = E }} ==> x
Expressions:
[[<breakpoint> x ]]_b ==> <breakpointJump> <ptr b> b <srcloc x> [[x]]_b
[[x ]]_b ==> x
[[k ]]_b ==> k
[[E1 E2 ]]_b ==> [[E1 ]]_b [[E2 ]]_b
[[let D1 .. Dn in E ]]_b ==> let [[D1 ]]_b .. [[Dn ]]_b in [[E ]]_b'
where b' = {{ D1 }} ++ .. ++ {{ Dn }}
[[case E of A1 .. An ]]_b ==> case [[E ]]_b of [[A1 ]]_b .. [[An ]]_b
[[\y1 .. yn -> E ]]_b ==> \y1 .. yn -> [[E ]]_(y1 .. yn ++ b)
{{ E }} ==> []
Alternatives:
[[p -> E ]]_b ==> p -> [[E ]]_({{p}} ++ b)
{{ A }} ==> []
Pats:
{{ x }} ==> x
{{ k P1 .. Pn }} ==> {{ P1 }} ++ ... ++ {{ Pn }}
```