C.3 Disambiguation

The given grammar for input syntax is quite ambiguous. This section provides some precedence rules for disambiguation. Note that the syntax for atomic formulae and terms caters for use of mixfix notation when applying predicates and operations; however, the recognition of the exact applicative structure of these constructs is left unspecified here, since it is inherently context-dependent.

At the level of structured specifications, ambiguities of grouping are resolved as follows:

• `rename', `require', `reveal', and `hide' have the highest precedence;
• `within' has lower precedence;
• `and' has lower precedence than all the above; and
• `then' has the lowest precedence of all.

Within a FORMULA, the use of prefix and infix notation for the logical connectives gives rise to some potential ambiguities. These are resolved as follows:

• `not FORMULA' has the highest precedence;
• `FORMULA /\.../\ FORMULA' and `FORMULA \/...\/ FORMULA' both have lower precedence, but may not be combined without explicit grouping;
• The connectives `FORMULA => FORMULA', `FORMULA if FORMULA',
  `FORMULA <=> FORMULA' all have even lower precedence. When repeated, `=>' groups to the right, whereas `if' groups to the left; `<=>' may not be repeated without explicit grouping. These may not be combined without explicit grouping.
• `QUANTIFIER VAR-DECL;... . FORMULA' has the lowest precedence of the logical constructs, with the last FORMULA extending as far to the right as possible, e.g., `forall x:S . F => G' is disambiguated as
  `forall x:S . (F => G)', not as `(forall x:S . F) => G'.

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_1$ when $F_1$ else $T_2$ when $F_2$ else $T_3$ 
  

  are implicitly grouped to the right:

                 $T_1$ when $F_1$ else ($T_2$ when $F_2$ else $T_3$)
  

Various other techniques for allowing the omission of grouping parentheses and/or list-separators in input (and display) are familiar from previous specification and programming languages, e.g., user-specified precedence (relative or absolute), and the "offside" rule. Moreover, not all parsers are expected to implement full mixfix notation. CASL is therefore to allow parsing annotations on (libraries of) specifications, to indicate the possible omission of grouping parentheses, and the degree of use of mixfix notation. Such annotations are expected to apply uniformly to CASL sublanguages, and to most extensions.