Up Next
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):

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
%prec <precedence-list>
For example the specification of natural numbers in [RM99] includes the following annotation for operator precedence:
precedences __ + __, __ - __ < __ * __, __ div __, __ mod __
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 5. The general form of this annotation is
  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:
  1. Expand all precedence relations into binary relations, i.e. from annotations of form (4.1), we get { (idi, idj) | 1 < i < n, n+1 < j < n+k }, and from annotations of form (4.1), we get { (idi, idj), (idj, idi) | 1 < i < n, n+1 < j < n+k }.
  2. 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.
  3. 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

Up Next