Go backward to C.2 Context-Free Syntax
Go up to C Concrete Syntax
Go forward to C.4 Lexical Syntax
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:
- [CHANGED:] `with',
[] `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.
[CHANGED:] At the level of architectural specifications, ambiguities of grouping
in unit terms are resolved in the same way as for structured
specifications. Moreover, a SPEC-NAME occurring as a
UNIT-SPEC gives rise to just the SPEC-NAME itself in the
abstract syntax tree, rather than a UNIT-TYPE with an empty
list SPEC* of argument specifications.
[] 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.
CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk