A RESULT-UNIT determines how the units declared in the enclosing
architectural specification are to be composed, using a UNIT-TERM
built from applications UNIT-APPL. A unit reduct
UNIT-REDUCT allows parts of the resulting unit to be hidden or
renamed. Taking the UNIT-TYPE of each UNIT-NAME from its
declaration, and taking any reducts into account, the UNIT-TERM
must be well-typed: the signature of each argument UNIT-TERM must
match that of the corresponding argument specification, and the
compatibility of the arguments must be ensured.
RESULT-UNIT ::= result-unit UNIT-DECL* UNIT-TERM
UNIT-TERM ::= UNIT-APPL | UNIT-REDUCT
UNIT-APPL ::= unit-appl UNIT-NAME UNIT-TERM*
UNIT-REDUCT ::= unit-reduct SIG-MORPH UNIT-TERM
[PDM]
What are the conditions that ensure this?
Discharged:
Same origin (unit declaration), same thing. That is, sorts s, s'
are the same if they can be traced to the same sort in the same unit
declaration.
In determining this, UNIT-APPLs should be regarded as
"generative", i.e. two identical but separate applications F(A)
produce results with different sorts.
Then in order to avoid unintentional differentiation we need either
unit definitions in architectural specs or local unit declarations as
described in Appendix C.
The auxiliary unit
declarations UNIT-DECL* in a RESULT-UNIT are for
(non-parametrized) units that are required, but not specified, by the
enclosing architectural specification; this allows compositions which
express partial architectural specifications that depend on external
units as specified in the declarations.
CoFI
Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk