In designing the external grammar, we have tried to strike a balance among a number of competing goals, including easy parseability by machines, easy readability by humans, and adequate structural simplicity to allow straightforward presentations of the semantics. Thus, we had to make some compromises. Specifically:
We use the following notational conventions for syntax:
[ pat ] | optional |
{ pat } | zero or more repetitions |
{ pat }+ | one or more repetitions |
pat1 ∣ pat2 | choice |
fibonacci
| terminal syntax in typewriter font |
Module | module | → |
%module mident { tdef ; }{ vdefg ; }
| |
Type defn. | tdef | → |
%data qtycon { tbind } = { [ cdef {; cdef } ] }
| algebraic type |
∣ |
%newtype qtycon qtycon { tbind } = ty
| newtype | ||
Constr. defn. | cdef | → |
qdcon { @ tbind }{ aty }+
| |
Value defn. | vdefg | → | %rec { vdef { ; vdef } } | recursive |
∣ | vdef | non-recursive | ||
vdef | → | qvar :: ty = exp | ||
Atomic expr. | aexp | → | qvar | variable |
∣ | qdcon | data constructor | ||
∣ | lit | literal | ||
∣ | ( exp ) | nested expr. | ||
Expression | exp | → | aexp | atomic expresion |
∣ | aexp { arg }+ | application | ||
∣ | \ { binder }+ -> exp | abstraction | ||
∣ | %let vdefg %in exp | local definition | ||
∣ | %case ( aty ) exp %of vbind { alt { ; alt } } | case expression | ||
∣ | %cast exp aty | type coercion | ||
∣ | %note " { char } " exp | expression note | ||
∣ | %external ccall " { char } " aty | external reference | ||
∣ | %dynexternal ccall aty | external reference (dynamic) | ||
∣ | %label " { char } " | external label | ||
Argument | arg | → | @ aty | type argument |
∣ | aexp | value argument | ||
Case alt. | alt | → | qdcon { @ tbind }{ vbind } -> exp | constructor alternative |
∣ | lit -> exp | literal alternative | ||
∣ | %_ -> exp | default alternative | ||
Binder | binder | → | @ tbind | type binder |
∣ | vbind | value binder | ||
Type binder | tbind | → | tyvar | implicitly of kind * |
∣ | ( tyvar :: kind ) | explicitly kinded | ||
Value binder | vbind | → | ( var :: ty ) | |
Literal | lit | → | ( [- ] { digit }+ :: ty ) | integer |
∣ | ( [- ] { digit }+ % { digit }+ :: ty ) | rational | ||
∣ | ( ' char ' :: ty ) | character | ||
∣ | ( " { char } " :: ty ) | string | ||
Character | char | → | any ASCII character in range 0x20-0x7E except 0x22,0x27,0x5c | |
∣ | \x hex hex | ASCII code escape sequence | ||
hex | → | 0∣…∣9 ∣a ∣…∣f | ||
Atomic type | aty | → | tyvar | type variable |
∣ | qtycon | type constructor | ||
∣ | ( ty ) | nested type | ||
Basic type | bty | → | aty | atomic type |
∣ | bty aty | type application | ||
∣ | %trans aty aty | transitive coercion | ||
∣ | %sym aty | symmetric coercion | ||
∣ | %unsafe aty aty | unsafe coercion | ||
∣ | %left aty | left coercion | ||
∣ | %right aty | right coercion | ||
∣ | %inst aty aty | instantiation coercion | ||
Type | ty | → | bty | basic type |
∣ | %forall { tbind }+ . ty | type abstraction | ||
∣ | bty -> ty | arrow type construction | ||
Atomic kind | akind | → | * | lifted kind |
∣ | # | unlifted kind | ||
∣ | ? | open kind | ||
∣ | bty :=: bty | equality kind | ||
∣ | ( kind ) | nested kind | ||
Kind | kind | → | akind | atomic kind |
∣ | akind -> kind | arrow kind | ||
Identifier | mident | → | pname : uname | module |
tycon | → | uname | type constr. | |
qtycon | → | mident . tycon | qualified type constr. | |
tyvar | → | lname | type variable | |
dcon | → | uname | data constr. | |
qdcon | → | mident . dcon | qualified data constr. | |
var | → | lname | variable | |
qvar | → | [ mident . ] var | optionally qualified variable | |
Name | lname | → | lower { namechar } | |
uname | → | upper { namechar } | ||
pname | → | { namechar }+ | ||
namechar | → | lower ∣ upper ∣ digit | ||
lower | → | a ∣ b ∣ … ∣ z ∣ _ | ||
upper | → | A ∣ B ∣ … ∣ Z | ||
digit | → | 0 ∣ 1 ∣ … ∣ 9 |