6.5 Compound Identifiers

      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[I₁,...,I_n]

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 I₁,...,I_n 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 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.