[DTS] The first clause below is redundant.
Discharged: All this goes to BASIC-ITEMs anyway. Type definition groups are not needed with non-linear visibility. Type definitions simply expand to a list of basic items.
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.BASIC-ITEM ::= ... | TYPE-DEFN-GROUP TYPE-DEFN-GROUP::= type-defn-group TYPE-DEFN+ AXIOM*
[TM] Are non-persistent interpretations of TYPE-DEFN-GROUPs allowed? (No)
Discharged: Irrelevant.
The order of the type definitions TYPE-DEFN in a TYPE-DEFN-GROUP is insignificant.
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).
When all the ALTERNATIVE constructs are constants without
components, the defined type corresponds to an (unordered) enumeration
type.
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.
A function symbol may be used more than once in a type definition
group, giving rise to overloading.
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 ::= type-defn SORT ALTERNATIVE+
ALTERNATIVE ::= CONSTRUCT | SORT
TYPE-DEFN-GROUP or in the local environment provided to it.
[AT]
I have no good intuition how the use of SORTs as
ALTERNATIVEs mixes with the freeness requirement.
Discharged:
TM supplies some intuition in
ftp://ftp.brics.dk/Projects/CoFI/Notes/S-3/
but the issue is now irrelevant since these no longer mix.
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.
CONSTRUCT ::= construct FUN-NAME COMPONENTS*
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.
COMPONENTS ::= components FUN-NAME* SORT
[AT]
I rather dislike recently introduced CONSTRUCTs with
multiple selectors to denote multiple arguments; I personally find
this confusing and misleading in a type definition, and would rather
insist here that the argument sort must be repeated as many times as
it appears as an argument for the constructor.
Discharged:
Restrict to single selectors.
The
function is declared as total if there is only one CONSTRUCT
in the enclosing TYPE-DEFN, otherwise as partial.
[AT]
If it really has to be declared as total in some cases then
the requirement should be that there is only one ALTERNATIVE
(not one CONSTRUCT) in the enclosing TYPE-DEFN.
Discharged:
Adjust wording.
BASIC-ITEM ::= ... | TYPE-DEFN-GROUP
[AT]
TYPE-DEFN-GROUP is both a BASIC-ITEM and a
SPEC. Is this intended? At the SPEC level, it is the
only construct (except for SIG-MORPH and reduction lists) that
is institution-specific. But it does not quite fit at the
BASIC-ITEM level either. If TYPE-DEFN-GROUPs are to
stay as BASIC-ITEMs: are axioms allowed to use variables
declared earlier in the list of basic items, or do they have to be
closed? And I would stick to linear visibility also in their
interpretation:
is to be treated as
basic-items-without-type-defn-groups; type-defn-group; basic-item
(modulo visibility of variables and perhaps re-declaration restrictions).
enrich basic-items-without-type-defn-groups
by (enrich type-defn-group
by basic-item)
Discharged:
TYPE-DEFN-GROUP no longer exists, and TYPE-DEFN is now
just a BASIC-ITEM.
When a TYPE-DEFN-GROUP occurs as a BASIC-ITEM in a
BASIC-SPEC, it corresponds to an EXTENSION of the
TYPE-DEFN-GROUP
[TM]
plus the BASIC-ITEMs occurring before the
TYPE-DEFN-GROUP? (This is an unfortunate mixture of
in-the-small and in-the-large, but with the above correction, I
believe that there is a semantics)
Discharged:
This is irrelevant now.
by the rest of the BASIC-SPEC.
[HB]
But what about the symbols declared by basic items used in
TYPE-DEFN-GROUP, e.g., argument sorts of a constructor?
Discharged:
This is irrelevant now.
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
Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk