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:are implicitly grouped to the right:T_{1}whenF_{1}elseT_{2}whenF_{2}elseT_{3}T_{1}whenF_{1}else (T_{2}whenF_{2}elseT_{3})

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

Here eachid_{1}, ..., id_{n}< id_{n+1}, ..., id_{n+k}, n>1, k>1.

For example the specification of natural numbers in [RM99] includes the following annotation for operator precedence:% prec<precedence-list>

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

Therefore, we allow to add a precedence annotation

with the effect that% prec-__ <> __^ __

whereid_{1}, ..., id_{n}<> id_{n+1}, ..., id_{n+k}, n>1, k>1,

- Expand all precedence relations into binary relations, i.e. from
annotations of form (4.1), we get
*{ (id*, and from annotations of form (4.1), we get_{i}, id_{j}) | 1__<__i__<__n, n+1__<__j__<__n+k }*{ (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]
^{6}. - Take the reflexive transitive closure of this union.

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% prec-__ <> __^ __

CoFI Note: L-11 -- Version: 0.1 -- 11 March 1999.

Comments to roba@informatik.uni-bremen.de