TOKEN-ID ::= ... | COMP-TOKEN-ID MIXFIX-ID ::= ... | COMP-MIXFIX-ID COMP-TOKEN-ID ::= comp-token-id TOKEN-ID ID+ COMP-MIXFIX-ID ::= comp-mixfix-id TOKEN-ID ID+
This extension of the syntax of identifiers for sorts, operations, and predicates is of relevance to generic specifications. A compound, token identifier COMP-TOKEN-ID or mixfix identifier COMP-MIXFIX-ID is written:
I[I1,...,In]The components Ii may (but need not) themselves identify sorts, operations, or predicates that are specified in the declared parameters of a generic specification.
When such a compound identifier is used to name, e.g., a sort in the body of a generic specification, the translation determined by fitting arguments to parameters applies to the components I1,...,In as well. Thus instantiations with different arguments generally give rise to different compound identifiers for what would otherwise be the same sort, which avoids unintended identifications when the instantiations are united.
E.g., a generic specification of sequences of arbitrary elements might use the simple identifier Elem for a sort in the parameter, and a compound identifier Seq[Elem] for the sort of sequences in the body. Fitting various argument sorts to Elem in different instantiations then results in distinct sorts of sequences.
[CHANGED:] Subsort embeddings between component sorts do not induce
subsort embeddings between the compound sorts: when desired, these have
to be declared explicitly. For example, when
Nat is declared as a subsort of Int, we do not
automatically get Seq[Nat] embedded as a subsort of
Seq[Int] in signatures containing all these sorts.
Instantiation, however, does preserve subsorts: if in a generic
specification we have Elem declared as a subsort of
Seq[Elem], where Elem is a parameter sort,
then in the result of instantiation of Elem by Nat, one
does get Nat automatically declared as a subsort of
Instantiation, however, does preserve subsorts: if in a generic specification we have Elem declared as a subsort of Seq[Elem], where Elem is a parameter sort, then in the result of instantiation of Elem by Nat, one does get Nat automatically declared as a subsort of Seq[Nat]. [CHANGED:] Compound identifiers must not be identified through the identification of components by the fitting morphism. E.g., if the body of a generic specification contains both List[Elem1] and List[Elem2], the fitting morphism must not map both Elem1 and Elem2 to Nat.  Higher-order extensions of CASL are expected to provide a more semantic treatment of parametrized sorts, etc.