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