DATATYPE-DECL ::= datatype-decl SORT ALTERNATIVE+
A datatype declaration DATATYPE-DECL is written:
S ::= A1 | ... | AnIt 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. Unreachable values can be eliminated also by the use of sort generation constraints.
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:
ON(C1; ...;Cn)When the list of components is empty, the constructor is simply written `ON'.
A partial constructor PARTIAL-CONSTRUCT with some components is written as:
ON(C1; ...;Cn)?(Partial constructors without components are not expressible in datatype declarations.)
The alternative declares ON 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 ::= 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:
ON1, ..., ONn:SA declaration PARTIAL-SELECT of partial selectors is written:
ON1, ..., ONn:?SThe remaining case is a component sort without any selector, simply written `S'.
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 ON1, ..., ONn 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.