Prev Up
Go backward to 6.4 Symbol Lists and Mappings
Go up to 6 Structuring Constructs

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[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.

Subsort embeddings between component sorts induce subsort embeddings between the compound sorts (but not vice versa). For example, when Nat is declared as a subsort of Int, we get automatically Seq[Nat] embedded as a subsort of Seq[Int] in signatures containing all these sorts.

If there are two compound sorts with multiple components, and the number of components are the same, and each pair of corresponding components either consist of two identical IDs or of two sorts in the subsort relationship, then there also is a subsort embedding between the compound sorts.

Instantiation also behaves as expected here: 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].

Higher-order extensions of CASL are expected to provide a more semantic treatment of parametrized sorts, etc.


CoFI Document: CASL/Summary --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk

Prev Up