A function binding, e.g. func(x,y)(z) = 0.

The binding of a pattern to an expression, e.g. (p,q) = e.

An assertion in a file, e.g. assert P [T= Q.

An import of an external function, e.g. external test,

An import of a transparent function, e.g. transparent normal.

A channel declaration, e.g. channel c, d : {0..1}.{0..1}.

A datatype declaration, e.g. datatype T = Clause1 | Clause2.

A subtype declaration, e.g. subtype T = Clause1 | Clause2.

A nametype declaration, e.g. nametype T2 = T.T.

A module declaration, e.g. module X(Y,Z) ... export ... endmodule.

A timed section, e.g. Timed(f) { P = a -> b -> P }.

A type annotation for the given names. This is only used inside the parser and never appears in outside ASTs.

A print statement, e.g. print x.

A refinement assertion, e.g. assert P [F= Q.

A check of property, like deadlock freedom, e.g. assert P :[deadlock free [F]].

The negation of an assertion, not currently supported.

Function application.

Application of a binary boolean operator.

Application of a unary boolean operator.

List concatenation, e.g. x^y.

Dot operator application, e.g. c.x.

If statements, e.g. if cond then e1 else e2.

Lambda functions, e.g. (x,y) @ e(x,y).

Let declarations, e.g. let func = e1 within e2.

Literals, e.g. true or 1.

List literals, e.g. 1,2,3.

List comprehensions, e.g. | (x,y) <- e.

Infinite list of integers from the given value, e.g. 1...

Bounded list of integers between the given values, e.g. 1..3.

List of integers from the given value, concatenating all adjacent lists, e.g. | x <- <0>.

List of integers between the given values, concatenating all items into one list, e.g. | (x,y) <- <(0,1)>.

The length of the list, e.g. #list.

A literal map, e.g. (| 1 => 2 |).

Application of binary maths operator, e.g. x+y.

Application of unary maths operator, e.g. -x.

A user provided bracket, e.g. (e).

Set literals, e.g. {1,2,3}.

Set comprehensions, e.g. {x,y | (x,y) <- e}.

Enumerated Sets, i.e. sets that complete the events, e.g. {| c.x |}.

Set comprehension version of SetEnum, e.g. {| c.x | x <- xs |}.

The infinite set of integers from the given value, e.g. {5..}.

The bounded set of integers between the two given values, e.g. {5..6}.

Set of integers from the given value, concatenating all adjacent sets, e.g. {x.. | x <- {0}}.

Set of integers between the given values, concatenating all items into one set, e.g. {x..y | (x,y) <- {(0,1)}}.

Tuples, e.g. (1,2).

Variables, e.g. x.

Alphabetised parallel, e.g. P [A || B] Q.

Exception operator, e.g. P [| A |> Q.

External choice, e.g. P [] Q.

Generalised parallel, e.g. P [| A |] Q.

Guarded expressions, e.g. b & P where b is a boolean expression. This is equivalent to if b then P else STOP.

Hiding of events, e.g. P A.

Internal choice, e.g. P |~| Q.

Interrupt (where the left process is turned off once the right process performs an event), e.g. P / Q.

Interleaving of processes, e.g. P ||| Q.

Event prefixing, e.g. c$x?y!z -> P.

Event renaming, e.g. P [[ a.x <- b.x | x <- X ]].

Sequential composition, e.g. P; Q.

Sliding choice, e.g. P |> Q.

Synchronising external choice, e.g. P [+A+] Q.

Synchronising interrupt, e.g. P /+A+ Q.

Replicated alphabetised parallel, e.g. || x : X @ [| A(x) |] P(x).

Replicated external choice, e.g. [] x : X @ P(x).

Replicated interleave, e.g. ||| x : X @ P(x).

Replicated internal choice, e.g. |~| x : X @ P(x).

Replicated link parallel, e.g. [a.x <- b.x | x <- X(y)] y : Y @ P(y).

Replicated parallel, e.g. [| A |] x : X @ P(x).

Replicated sequential choice, e.g. ; x : 0,1 @ P(x).

Replicated synchronising external choice, e.g. [+ A +] x : X @ P(x).

Used only for parsing - never appears in an AST.

Used only for parsing - never appears in an AST.

A timed prefix - only appears after desugaring.

!x

?x:A

$x:A (see P395 UCS)

The concatenation of two patterns, e.g. p1^p2.

The dot of two patterns, e.g. p1.p2.

A double pattern match, e.g. p1@@p2.

A literal pattern list, e.g. p1,p2,p3.

A literal pattern, e.g. true, or 0.

A user supplied parenthesis in a pattern.

A set pattern. Only singleton patterns, or zero patterns are supported. This is checked by the desugarer. For example, {p1,p2} is not allowed, but {p1} and {} are allowed.

A tuple pattern, e.g. (p1,p2,p3).

A variable pattern, e.g. x, or A where A is a datatype clause. If the variable is a datatype clause then it only matches that datatype tag, whereas for anything else it matches anything.

Matches anything but does not bind it.

Since you can write list patterns such as:

 f(<x,y>^xs^<z,p>^<9,0>)
 f(<x,y>)
 f(xs^<x,y>)

we need an easy may of matching them. Thus, we compile the patterns to a PCompList instead.

PCompList ps (Just (p, ps')) corresponds to a list where it starts with ps (where each p in ps matches exactly one list element, has a middle of p (which must be a variable pattern, or a wildcard) and and end matching exactly ps' (again, where each p in ps matches exactly one list component).

Like with a PCompList we flatten nested dot patterns to make it easier to evaluate.