breakpoint jump

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