APPLICATION ::= application OP-SYMB TERMS
OP-SYMB ::= OP-NAME | QUAL-OP-NAME
QUAL-OP-NAME ::= qual-op-name OP-NAME OP-TYPE
TERMS ::= terms TERM*
An application of an operation symbol OS to some argument terms is written:
OS(T1, ..., Tn)When [CHANGED:] OS [] is a mixfix identifier, consisting of a sequence `t0__...__tn' of tokens or spaces ti separated by place-holders `__', the application may also be written:
t0T1t1...TntnWhen the operation symbol is a constant with no argument terms, its application is simply written `OS'.
Declaring different mixfix identifiers that involve some common tokens
may lead to ambiguity, with different candidate groupings of the same
sequence of tokens and terms. Such ambiguity prevents the enclosing
atomic formula from being well-formed, irrespective of the declared
profiles of the symbols involved, and generally has to be eliminated
by use of explicit grouping parentheses. However, to allow the
omission of some parentheses, infix identifiers are given weaker
precedence than prefix identifiers, which in turn are given weaker
precedence than postfix identifiers.
[CHANGED:] (The mixfix identifier `__ __' is allowed, and regarded as
an infix, although this is unlikely to be the case in
higher-order extensions of CASL, since there juxtaposition will be
reserved for function application.)
[] [CHANGED:] In an application, a
qualified operation name QUAL-OP-NAME with f qualified
by the operation type T is written:
(op f:T)
When the qualified operation name is a constant c, its application
(to no arguments) is also written (op c:T).
[] The application is well-sorted for some particular sort when there is
a declaration of the operation name (with the argument and result
sorts indicated by the type, if specified) such that all the argument
terms are well-sorted for the respective argument sorts, and the
result sort is the required sort. It then expands to an application
of the qualified operation name to the fully-qualified expansions of
the argument terms for those sorts.