9 EventML’s syntax

n	∈	Nat		(natural numbers)
ptc	∈	PostTyC	::=	Int∣List∣Bool∣Unit∣Bag∣Class∣Msg∣Loc∣Token
itc	∈	InfTyC	::=	*∣→∣+
b	∈	Bool	=	true∣false
op	∈	Op	::=	+∣-∣*∣/∣=∣.∣++∣<∣>∣or∣&∣>>=∣||∣@
atexp	∈	AtExp	::=	vid∣n∣b∣~atexp∣inl(exp)∣inr(exp)
			∣	(exp1,…,expn)
			∣	{exp1; …; expn}
			∣	Prior(exp)
			∣	Once(exp)
			∣	Output(exp)
			∣	OnLoc(exp)
			∣	(exp)
exp	∈	Exp	::=	atexp
			∣	atexp/ ~
			∣	exp o (exp1,,expn⌜,Prior(self)?exp′⌝)
			∣	exp1 op exp2
			∣	exp:ty
			∣	exp atexp
			∣	\pat.exp
			∣	if exp1 then exp2 else exp3
			∣	let bind in exp
			∣	letrec bind in exp
			∣	class bind in exp
			∣	atexp where bind
pat	∈	Pat	::=	vid
			∣	_
			∣	(pat1,…,patn)
			∣	pat:ty
tyseq	∈	TySeq	::=	ϵ
			∣	ty
			∣	(ty0,…,tyn)
ty	∈	Ty	::=	a
			∣	tyseq ptc
			∣	ty1 itc ty2
			∣	(ty)

Figure 25: EventML syntax – expression

tok	∈	Token	::=	`cseq`
toks	∈	Tokens	::=	[tok0; …; tokn]
status	∈	Status	::=	internal
			∣	input
			∣	output
hdropt	∈	HdrOpt	::=	base vid
			∣	send vid
			∣	broadcast vid
hdropts	∈	HdrOpts	::=	hdropt⌜,hdropts⌝
header	∈	Header	::=	status (toks : ty⌜, hdropts⌝)
bind	∈	Bind	::=	vid atpat1  atpatn = exp
dec	∈	Dec	::=	let bind;;
			∣	letrec bind;;
			∣	class bind;;
			∣	parameter vid : ty
			∣	import vid0  vidn
			∣	MSGS header0  headern
			∣	main exp
			∣	specification vid
prog	∈	Prog	::=	dec ⌜prog⌝

Figure 26: EventML syntax – declarations

Identifiers

An identifier can either be alphanumeric or symbolic. An alphanumeric identifier is a sequence of letters, digits, primes (quotes), dashes and underscores starting with a letter. For example, bag_map, bag-map, bag-map’, and bag-map1 are identifiers, but 1bag-map is not. A symbolic identifier is a sequence of the following symbols: !, %, &, #, /, <, =, ?, \, ˜, ˆ, |, >, -, :, +, @, *. Some alphanumerics as well as some symbolic identifiers are disallowed because they are reserved keywords. They are described in Figures 25 and 26 bellow.

Let Vid be the set of identifiers and let vid range over identifiers.

Type variables

A type variable is an alphanumeric identifier preceded by primes (quotes). For example, ’a and ’’a are type variables

Let TyVar be the set of type variable and let a range over type variables.

Character sequences

Let CharSeq be the set of sequences of characters other than backquotes (`) and let cseq range over CharSeq.

Other syntactic forms

Figures 25 and 26 defines EventML’s syntax. In this figure we write ⌜x⌝ to indicate that x is optional. These brackets are not part of EventML’s syntax. For example, a program prog can either be a declaration followed by two semicolons, or a declaration followed by two semicolons followed by another program (it allows us to define recursive production rules).

We also impose the following syntactic restrictions:

• In a program, a declaration of the form specification vid has to be the first declaration and there can only be one.
• In a program, a declaration of the form main exp has to be the last declaration and there can only be one.
• In an expression of the form letrec bind in exp′, where bind is of the form vid atpat₁  atpat_n = exp, either n >= 1 or exp is a lambda expression the form \pat.exp′′ (i.e., a recursive declaration can only bind a function).
• In a declaration of the form letrec bind;;, where bind is of the form vid atpat₁  atpat_n = exp, either n >= 1 or exp is a lambda expression (i.e., of the form \pat.exp′).