wiki:GhciDebugger/BreakpointJump

Version 1 (modified by mnislaih, 7 years ago) (diff)

--

(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

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 b [[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 }}