10.2. External Grammar of Core

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

Modulemodule→ %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
∣vdefnon-recursive
vdef→qvar :: ty = exp 
Atomic expr.aexp→qvarvariable
∣qdcondata constructor
∣litliteral
∣( exp )nested expr.
Expressionexp→aexpatomic expresion
∣aexp { arg }+application
∣\ { binder }+ -> expabstraction
∣%let vdefg %in explocal definition
∣%case ( aty ) exp %of vbind { alt { ; alt } }case expression
∣%cast exp atytype coercion
∣%note " { char } " expexpression note
∣%external ccall " { char } " atyexternal reference
∣%dynexternal ccall atyexternal reference (dynamic)
∣%label " { char } "external label
Argumentarg→@ atytype argument
∣aexpvalue argument
Case alt.alt→qdcon { @ tbind }{ vbind } -> expconstructor alternative
∣lit -> expliteral alternative
∣%_ -> expdefault alternative
Binderbinder→@ tbindtype binder
∣vbindvalue binder
Type bindertbind→tyvarimplicitly of kind *
∣( tyvar :: kind )explicitly kinded
Value bindervbind→( var :: ty ) 
Literallit→( [-] { digit }+ :: ty )integer
∣( [-] { digit }+ % { digit }+ :: ty )rational
∣( ' char ' :: ty )character
∣( " { char } " :: ty )string
Characterchar→any ASCII character in range 0x20-0x7E except 0x22,0x27,0x5c
∣\x hex hexASCII code escape sequence
hex→0∣…∣9 ∣a ∣…∣f 
Atomic typeaty→tyvartype variable
∣qtycontype constructor
∣( ty )nested type
Basic typebty→atyatomic type
∣bty atytype application
∣%trans aty atytransitive coercion
∣%sym atysymmetric coercion
∣%unsafe aty atyunsafe coercion
∣%left atyleft coercion
∣%right atyright coercion
∣%inst aty atyinstantiation coercion
Typety→btybasic type
∣%forall { tbind }+ . tytype abstraction
∣bty -> tyarrow type construction
Atomic kindakind→*lifted kind
∣#unlifted kind
∣?open kind
∣bty :=: btyequality kind
∣( kind )nested kind
Kindkind→akindatomic kind
∣akind -> kindarrow kind
Identifiermident→pname : unamemodule
tycon→unametype constr.
qtycon→mident . tyconqualified type constr.
tyvar→lnametype variable
dcon→unamedata constr.
qdcon→mident . dconqualified data constr.
var→lnamevariable
qvar→[ mident . ] varoptionally qualified variable
Namelname→lower { namechar } 
uname→upper { namechar } 
pname→{ namechar }+ 
namechar→lower ∣ upper ∣ digit 
lower→a ∣ b ∣ … ∣ z ∣ _ 
upper→A ∣ B ∣ … ∣ Z 
digit→0 ∣ 1 ∣ … ∣ 9