L-11 -- 4.1 Precedence Annotations

Go up to 4 Parsing Annotations
Go forward to 4.2 Associativity Annotations

4.1 Precedence Annotations

The CASL summary defines some predefined precedences between mixfix operation symbols [CoF98], page C-8:

The declaration of infix, prefix, postfix, and general mixfix operation symbols may introduce further potential ambiguities, which are partially resolved as follows (remaining ambiguities have to be eliminated by explicit use of grouping parentheses in terms, or by use of parsing annotations):
Ordinary function application `OP-SYMB(TERMS)' has the highest precedence.
Applications of all postfix symbols have the next-highest precedence within terms after ordinary function application. This extends to all mixfix operation symbols of the form `__ ... __ TOKEN', and to sorted terms and casts.
Applications of all prefix symbols have the next-highest precedence within terms after postfixes. This extends to all mixfix operation symbols of the form `TOKEN __ ... __'.
Applications of infix symbols have the next-highest precedence within terms after prefixes. This extends to all mixfix symbols of the form `__ ... __ ... __'. Mixtures of different infix symbols and iterations of the same infix symbol have to be explicitly grouped--although the attribute of associativity implies a parsing annotation that allows iterated applications of that symbol to be written without grouping.
The conditional `TERM when FORMULA else TERM' has the weakest
precedence within terms, and iterations such as:
               T₁ when F₁ else T₂ when                F₂ else T₃
are implicitly grouped to the right:
               T₁ when F₁ else (T₂ when                F₂ else T₃)

Call a mixfix symbol of the form `__ ... __ ... __' a generalized infix symbol. Precedence annotations allow the user to extend the above priority scheme in order to disambiguate mixtures of different generalized infix symbols and iterations of the same generalized infix symbol -- without using parentheses. As a basic notion for precedence we use precedence relations of the form

id₁, ..., id_n < id_n+1, ..., id_n+k, n > 1, k > 1.

Here each id_i is an (unqualified) generalized infix operation symbol. The relation specifies that for 1 < i < n the symbol id_i has lower priority (i.e., binds weaker) than the symbol id_j, where n+1 < j < n+k. We combine such precedence relations to a precedence-list, which consists of at least one precedence relation. The different precedence relations of one precedence list are separated by a semicolon. The annotation has the form

%prec <precedence-list>

For example the specification of natural numbers in [RM99] includes the following annotation for operator precedence:

spec: Nat=
...
%%: precedences __ + __, __ - __ < __ * __, __ div __, __ mod __
...
end

A second form of annotations is motivated by the fact that the predefined precedences on page C-8 of the CASL summary do not allow us to use the standard mathematical notation: -x^ 2 In mathematical textbooks, this is being disambiguated as -(x^ 2) Due to the rules of page C-8, prefix operators bind stronger than infix operators, so we get (-x)^ 2 in CASL.

Therefore, we allow to add a precedence annotation

%prec -__ <> __^ __

with the effect that -__ and __^ __ have equivalent precedence, which means that -x^ 2 is ambiguous (see below) and must be explicitly disambiguated with parentheses ⁵. The general form of this annotation is

id₁, ..., id_n <> id_n+1, ..., id_n+k, n > 1, k > 1,

where id_i can be any mixfix symbol (not just an generalized infix operation symbol). The precedence annotations determine a pre-order, which is obtained in the following way:

Expand all precedence relations into binary relations, i.e. from annotations of form (4.1), we get { (id_i, id_j) | 1 < i < n, n+1 < j < n+k }, and from annotations of form (4.1), we get { (id_i, id_j), (id_j, id_i) | 1 < i < n, n+1 < j < n+k }.
Take the union of all declared expanded precedence relations with the predefined precedences. The predefined precedences are those listed on page C-8 of the CASL summary [CoF98]⁶.
Take the reflexive transitive closure of this union.

For example, the annotation

%prec __+__ < __*__

has the effect that the term 3 + 4 * 5 is parsed as 3 + (4 * 5). 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. Thus the annotation

%prec -__ <> __^ __

has the effect that the term -x^ 2 is ill-formed and must be explicitly disambiguated using parentheses.

CoFI Note: L-11 -- Version: 0.1 -- 11 March 1999.
Comments to roba@informatik.uni-bremen.de