C.5.2.3 Parsing Annotations

These annotations, applicable to an entire library, are to allow users to specify the precedence of operation symbols, and the significance of layout in the so-called "offside" rule. Their primary purpose is to allow the omission of grouping parentheses and/or list separators in the input; but formatters may also exploit them to avoid superfluous parentheses in the display.

A set of parsing annotations has been proposed in Note L-11 [RM99] (see also Note T-6 [Mos98a]). The following have been approved:

• Annotations on Operator Precedences: The proposal was accepted with the amendment that operator lists of more than one item are to be grouped by {...}..
• Annotations on Associativity: `%left assoc' and `%right assoc' were both accepted.

A prededence annotation is written:

%prec {id₁, ..., id_n} < {id_n+1, ..., id_n+k}

It is also possible to specify that two mixfix operation symbols id₁ and id₂ (which need not to be of form `__ ... __ ... __') are not allowed to be combined without explicit grouping parentheses This is done using an annotation:

%prec {id₁, ..., id_n} <> {id_n+1, ..., id_n+k}

The precedence annotations determine a pre-order, which is obtained in the following way:

1. Expand all precedence relations into binary relations, i.e.:
   • from annotations of the form {id₁, ..., id_n} < {id_n+1, ..., id_n+k} we get { (id_i, id_j) | 1 < i < n, n+1 < j < n+k }, and
   • from annotations of the form {id₁, ..., id_n} <> {id_n+1, ..., id_n+k} we get { (id_i, id_j), (id_j, id_i) | 1 < i < n, n+1 < j < n+k }.
2. Take the union of all declared expanded precedence relations with the predefined precedences listed in Section C.3.1.
3. Take the reflexive transitive closure of this union.

If two symbols occurring in a term of atomic formula are equivalent (i.e. related in both directions) or incomparable (i.e. related in no direction) in the precedence relation, their grouping has to be explicitly specified by using parentheses.

There are two associativity annotations, `%left assoc' and `%right assoc'. They may be used immediately after an operation or predicate declaration. For example, declaring __+__ to be left associative means that t₁ + t₂ + t₃ is parsed as (t₁ + t₂) + t₃, while declaring it to be right associative leads to t₁ + (t₂ + t₃). If there is no associativity annotation for a mixfix symbol, it is not allowed to repeat that symbol without explicit grouping using parentheses.

For precedence and associativity annotations, we adopt non-linear visibility, that is, they are visible in the whole enclosing basic specification (cf. Section C.3.1).

Precedence annotations interact with structured specifications in the same way as the subsorting relation. That is, for renamings and restrictions, the precedence relation is lifted along the renaming or restriction. For unions and extensions, the precedence relations are united. Note that in the case that there are conflicting precedence annotations this may lead to equivalent symbols in the union. In this case these symbols cannot be combined without explicit grouping. Associativity annotations are translated along renamings and restrictions and united along unions and extensions in the same way as the operations they refer to.