(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 }}