Note that a DATATYPE-DECL 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
(summarized in Part II), or within basic
specifications by use of sort generation constraints and (rather
tedious) axioms.
When all the ALTERNATIVE constructs are CONSTANTs, the
defined type corresponds to an (unordered) enumeration type.
A COMPONENT with a FUN-NAME moreover declares the
function FUN-NAME as a selector, with the argument sort given
by the enclosing DATATYPE-DECL, and with the indicated result
sort. The function is declared as total if there is only one
ALTERNATIVE in the enclosing DATATYPE-DECL, otherwise as
partial.
A datatype declaration DATATYPE-DECL declares its component
SORT. For each alternative CONSTRUCT it declares the
required constructor and selector functions, and determines axioms
asserting the expected relationship between any selectors and the
constructors. All sorts used in each ALTERNATIVE must be
declared in the local environment provided to the enclosing
DATATYPE-DECL.
! DATATYPE-DECL ::= datatype-decl SORT ALTERNATIVE+
! ALTERNATIVE ::= CONSTANT | CONSTRUCT
A function FUN-NAME specified in a CONSTRUCT is declared as
a total constructor. Each COMPONENT specifies one
argument sort for the constructor; its result sort is the SORT
of the enclosing DATATYPE-DECL.
! CONSTRUCT ::= construct FUN-NAME COMPONENT+
A COMPONENT without a FUN-NAME merely provides its
SORT as an argument sort for the constructor for the enclosing
CONSTRUCT.
! COMPONENT ::= component FUN-NAME? SORT
CoFI Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk