Go backward to Structured Specifications
Go up to Structuring Constructs
Go forward to Generic Specifications

Type Definition Group

BASIC-ITEM     ::=   ... | TYPE-DEFN-GROUP
TYPE-DEFN-GROUP::=   type-defn-group TYPE-DEFN+ AXIOM*
A type definition group TYPE-DEFN-GROUP provides a concise way of specifying a collection of sorts equipped with function symbols called constructors and selectors. The intended interpretation is as a freely-generated extension: terms built with the constructors evaluate to distinct values, unless their equality is a consequence of the specified axioms.

The order of the type definitions TYPE-DEFN in a TYPE-DEFN-GROUP is insignificant. 

TYPE-DEFN       ::=   type-defn SORT ALTERNATIVE+
ALTERNATIVE     ::=   CONSTRUCT | SORT
A type-definition TYPE-DEFN 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. It declares each SORT that occurs as an ALTERNATIVE to be a subsort of the SORT of the enclosing TYPE-DEFN. All sorts used in each ALTERNATIVE must be declared in the enclosing TYPE-DEFN-GROUP or in the local environment provided to it.

When each ALTERNATIVE in a TYPE-DEFN is a SORT, the defined type corresponds to a sort union (which need not be a disjoint union). 

CONSTRUCT       ::=   construct FUN-NAME COMPONENTS*
A function FUN-NAME specified in a CONSTRUCT is declared as a total constructor. Each COMPONENTS specifies one or more argument sorts for the constructor; its result sort is the SORT of the enclosing TYPE-DEFN.

When all the ALTERNATIVE constructs are constants without components, the defined type corresponds to an (unordered) enumeration type. 

COMPONENTS      ::=   components FUN-NAME* SORT
A COMPONENTS with an empty list FUN-NAME* of selector functions merely provides its SORT as an argument sort for the constructor for the enclosing CONSTRUCT.

A COMPONENTS with a list FUN-NAME* of length n>0 provides n copies of its SORT as argument sorts for the constructor for the enclosing CONSTRUCT. Moreover, it declares each function FUN-NAME as a selector, with the argument sort given by the enclosing TYPE-DEFN, and with the indicated result sort. The function is declared as total if there is only one CONSTRUCT in the enclosing TYPE-DEFN, otherwise as partial.

A function symbol may be used more than once in a type definition group, giving rise to overloading. 

BASIC-ITEM      ::=   ... | TYPE-DEFN-GROUP
When a TYPE-DEFN-GROUP occurs as a BASIC-ITEM in a BASIC-SPEC, it corresponds to an EXTENSION of the TYPE-DEFN-GROUP by the rest of the BASIC-SPEC. Regarding visibility of symbols, however, basic items that occur before the TYPE-DEFN-GROUP are not allowed to refer to the symbols declared by it.
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk