Up Next
Go up to 2.1.4 Datatypes
Go forward to 2.1.4.2 Free Datatype Declarations

2.1.4.1 Datatype Declarations

      DATATYPE-DECL ::= datatype-decl SORT ALTERNATIVE+

A datatype declaration DATATYPE-DECL is written:

s ::= A1 | ... | An
It declares the sort s. For each alternative construct A1, ..., An, it declares the specified constructor and selector operations, and determines sentences asserting the expected relationship between selectors and constructors. All sorts used in an alternative construct must be declared in the local environment (which always includes the sort declared by the datatype declaration itself).

Note that a datatype declaration allows models where the ranges of the constructors are not disjoint, and where not all values are the results of constructors. This looseness can be eliminated in a general way by use of free extensions in structured specifications (as summarized in Part II), or by use of free datatypes within basic specifications (see below). Unreachable values can be eliminated also by the use of sort generation constraints.

Alternatives
      ALTERNATIVE       ::= TOTAL-CONSTRUCT | PARTIAL-CONSTRUCT
      TOTAL-CONSTRUCT   ::= total-construct   OP-NAME COMPONENTS*
      PARTIAL-CONSTRUCT ::= partial-construct OP-NAME COMPONENTS*

A total constructor TOTAL-CONSTRUCT with some components is written as:

f(C1; ...;Cn)
When the list of components is empty, the constructor is simply written `f'.

A partial constructor PARTIAL-CONSTRUCT with some components is written as:

f(C1; ...;Cn)?
(Partial constructors without components are not expressible in datatype declarations.)

The alternative declares f as an operation. Each component C1, ..., Cn specifies one or more argument sorts for the profile; the result sort is the sort s declared by the enclosing datatype declaration.

Components
      COMPONENTS     ::= TOTAL-SELECT | PARTIAL-SELECT | SORT
      TOTAL-SELECT   ::= total-select   OP-NAME+ SORT
      PARTIAL-SELECT ::= partial-select OP-NAME+ SORT

A declaration TOTAL-SELECT of total selectors is written:

f1, ..., fn:s
A declaration PARTIAL-SELECT of partial selectors is written:
f1, ..., fn:? s
The remaining case is a component sort without any selector, simply written `s'.

[CHANGED:] Note that when there is more than one alternative construct in a datatype declaration, selectors are usually partial, and must therefore be declared as such. Their values on constructs for which they are not declared as selectors are left unspecified. [] In the first two cases, it provides n components: the sort s is taken as an argument sort n times for the constructor operation declared by the enclosing alternative, and it declares f1, ..., fn as selector operations for the respective components. In the first case, each selector operation is declared as total, and in the second case, as partial. It also determines sentences that define the value of each selector on the values given by the constructor of the enclosing alternative.

In the last case, it provides the sort s only once as an argument sort for the constructor of the enclosing alternative, and it does not declare any selector operation for that component.

[CHANGED:] Some minor restrictions are imposed: In a datatype declaration with more than one alternative, any selector that is declared as total for some alternative must be declared as a total selector with the same result sort for every other alternative. Moreover, a list of datatype declarations must not declare a function symbol both as a constructor and selector with the same profiles. []

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk

Up Next