[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Proposal for Generic Extensions with Import Clauses
Hi all,
the following is the proposal for generic extensions with import
clauses.
Greetings,
Hubert
[This change is required to ensure that the semantics of instantiation
always corresponds to a pushout. Follow-ups on technical details of
the formal semantics below should be sent to cofi-semantics@brics.dk,
and all other follow-ups to cofi-language@brics.dk. --PDM]
New abstract syntax:
--------------------
GEN-EXTENSION ::= gen-extension IMPORT? PARAMS SPEC+
GEN-CONS-EXT ::= gen-cons-ext IMPORT? PARAMS SPEC+
IMPORT ::= import SPEC
New text in the summary:
------------------------
The abstract syntax of a generic specification GEN-SPEC is comparable to
that of an EXTENSION: the parameters PARAMS of the generic specification
extend the SPEC of the IMPORT (or the empty specification, if no IMPORT
is given), and are themselves extended by the list of specifications
SPEC+ that form the body. If the IMPORT is present, its local
environment is empty.
The well-formedness and semantics of GEN-SPEC are essentially as for the
corresponding extension of the SPEC of the IMPORT by the union of the
PARAMS specifications and then by the body SPEC+, the only difference
being that a fitting argument has to be supplied for each declared
parameter when referencing a GEN-SPEC through its name, as explained
below.
Semantics:
----------
The (combined static and model) semantics of a generic specification is
NAME |-> (I(),(P_1(I()),..,P_n(I())),B(P_1(I()) + .. + P_n(I())),
where I() denotes the semantics of I wrt. the empty local environment,
which is the pair (Sigma_I,Mset_I), and P_i(I()) denotes the semantics
of P_i wrt. the local environment given by I(). I is the import, P_i
the parameters and B the body of the generic specification.
New text for instantiation:
---------------------------
A generic specification instantiation GEN-SPEC-INST refers to the
generic specification named GEN-SPEC-NAME in the global environment,
providing a fitting argument FITTING-ARG for each declared parameter (in
the same order).
A fitting argument FITTING-ARG fits the argument specification SPEC to
the corresponding parameter specification via a signature morphism
determined by the symbol map lists SYMB-MAP* specified in the
FITTING-ARG and in the enclosing GEN-SPEC-INST. Unmapped symbols are
included unchanged.
The local environment given to the argument specifications is the union
of the current local environment and the import part of the generic
specification.
When there is more than one parameter, the symbol maps of the fitting
arguments have to be \textit{compatible} and their union has to yield a
single morphism from the union of the parameters to the union of the
arguments. Thus any common parts of declared parameters have to be
instantiated in the same way (cf. UNION). It is pointless to declare the
same parameter twice in a generic specification. (Generic specifications
that require two similar but independent parameters can be expressed by
using a translation to distinguish between the symbols in the signatures
of the two parameters.)
If the import part exists, the fitting morphism has to be the identity
on the import part.
All the symbols that the body and the argument have in common are either
introduced by the import part or by the parameter. If this is not the
case, instantiation is not well-formed.
The semantics of a well-formed instantiation GEN-SPEC-INST is the same
as that of the specification determined as follows: the fitting
morphisms are extended to a single morphism applicable to the signature
of the entire generic specification GEN-SPEC named by the GEN-SPEC-NAME,
then the translation of it by this morphism is united with all the
argument specifications. Each model of an argument is required to be a
model of the corresponding parameter, otherwise the instantiation is
undefined.
The semantics:
--------------
A sketch of the semantics of instantiation of a generic specification
with import is given by the following diagram:
----> A(I()+Env) ------------> Res
| ^ ^
I() --| fm po |
| | |
----> P(I()) ----------------> B(P(I()))
Env is the local environment given to the instantiation and Res the
result of the instantiation.
P(I()) = P_1(I()) + .. + P_n(I()) and A(I()+Env) = A_1(I()+Env) + .. +
A_n(I()}Env) are the union of the parameter and argument specifications.
Strictly speaking, the semantics is not defined to be a pushout.
Instead, the semantics describes a way of constructing the result from
the arguments and the body. Then we get the theorem that the
instantiation diagram always is a pushout.
--
Hubert Baumeister
MPI Informatik, Im Stadtwald, D-66123 Saarbr"ucken, Germany
Phone: (x49-681)9325-220 Fax: -299
e-mail: hubert@mpi-sb.mpg.de
WWW: http://www.mpi-sb.mpg.de/~hubert/