Prev Up Next
Go backward to 2.3.4.2 Qualified Variables
Go up to 2.3.4 Terms
Go forward to 2.3.4.4 Sorted Terms

2.3.4.3 Operation Application

      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...Tntn
When 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.
CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk

Prev Up Next