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
vdefqvar :: ty = exp 
Atomic expr.aexpqvarvariable
qdcondata constructor
litliteral
( exp )nested expr.
Expressionexpaexpatomic 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.altqdcon { @ tbind }{ vbind } -> expconstructor alternative
lit -> expliteral alternative
%_ -> expdefault alternative
Binderbinder@ tbindtype binder
vbindvalue binder
Type bindertbindtyvarimplicitly of kind *
( tyvar :: kind )explicitly kinded
Value bindervbind( var :: ty ) 
Literallit( [-] { digit }+ :: ty )integer
( [-] { digit }+ % { digit }+ :: ty )rational
( ' char ' :: ty )character
( " { char } " :: ty )string
Charactercharany ASCII character in range 0x20-0x7E except 0x22,0x27,0x5c
\x hex hexASCII code escape sequence
hex0∣…∣9 ∣a ∣…∣f 
Atomic typeatytyvartype variable
qtycontype constructor
( ty )nested type
Basic typebtyatyatomic 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
Typetybtybasic type
%forall { tbind }+ . tytype abstraction
bty -> tyarrow type construction
Atomic kindakind*lifted kind
#unlifted kind
?open kind
bty :=: btyequality kind
( kind )nested kind
Kindkindakindatomic kind
akind -> kindarrow kind
Identifiermidentpname : unamemodule
tyconunametype constr.
qtyconmident . tyconqualified type constr.
tyvarlnametype variable
dconunamedata constr.
qdconmident . dconqualified data constr.
varlnamevariable
qvar[ mident . ] varoptionally qualified variable
Namelnamelower { namechar } 
unameupper { namechar } 
pname{ namechar }+ 
namecharlower ∣ upper ∣ digit 
lowerab ∣ … ∣ z_ 
upperAB ∣ … ∣ Z 
digit01 ∣ … ∣ 9