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:T1 when F1 else T2 when F2 else T3T1 when F1 else (T2 when F2 else T3)
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
id1, ..., idn < idn+1, ..., idn+k, n > 1, k > 1.Here each idi is an (unqualified) generalized infix operation symbol. The relation specifies that for 1 < i < n the symbol idi has lower priority (i.e., binds weaker) than the symbol idj, 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
For example the specification of natural numbers in [RM99] includes the following annotation for operator precedence:
Therefore, we allow to add a precedence annotation
with the effect that -__ and __^ __ have equivalent precedence, which means that -x^ 2 is ambiguous (see below) and must be explicitly disambiguated with parentheses 5. The general form of this annotation is
%prec -__ <> __^ __
id1, ..., idn <> idn+1, ..., idn+k, n > 1, k > 1,where idi 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:
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.
%prec -__ <> __^ __