[CoFI] Proposed change to CASL: remove overall fitting

[Michel.Bidoit@lsv.ens-cachan.fr (Michel Bidoit)]

While discussing an ambiguity concerning the syntax of GEN-SPEC-INST 
("SPEC-NAME[SPEC-NAME[...] fitting SYMB-MAP]" has two parses) Peter
made the following suggestion:
 
> Personally, I'd be happy to remove the possibility for the overall
> fitting (which applies to symbols shared by all the parameters)
> since I don't think it is going to be used - especially now that we
> also have IMPORTS.

I remember we had a discussion about what would be the best from a
methodological point of view, without getting to a clear conclusion.
So I am happy to follow this suggestion and remove the possibility of
the overall "external" fitting. Please note however that Paris
examples will then have to be slightly adjusted.

Here is a rationale:

a) Most generic specs will have just one parameter; for these specs,
there is no true difference and both forms are extremely similar. It
seems better to keep just one form (whatever it is), in order to made
things easier to remember.

b) For generic specs with more than one parameter, say F [X] [Y], we
have two views:

* Using the "internal" style for fitting put more emphasis on how each
individual parameter is instantiated; this is even more true in case just
some of the parameters are instantiated, as e.g. in F [A fitting ...] [Y].

* Using the "external" style for fitting put more emphasis on the fact that
semantically speaking, the parameter is indeed the union of the individual
parameters (i.e. F [X] [Y] is equivalent to F [X + Y]), and also on the
fact that for being correct, all fitting morphisms should agree on shared
symbols. E.g. in F [A fitting ...f1...] [B fitting ...f2...], f1 and f2
should coincide on symbols shared by X and Y, if any. This seems to be more
easily ensured by the external style with F [A] [B] fitting ...f3...

Since, for methodological reasons, it has been chosen to allow for generic
specifications with more than one parameter, it seems more consistent to
keep the "internal" style for fitting morphisms. It is expected that tools
will warn the user in the case of incompatible fitting morphisms.

[If this change is implemented, the abstract syntax would become:
  GEN-SPEC-INST    ::=  gen-spec-inst GEN-SPEC-NAME FITTING-ARG+
and the concrete syntax would be simplified accordingly.  --PDM]

Cheers,
Michel
-- 
Michel Bidoit
Laboratoire Specification et Verification       Tel:  +33 (0)1 47 40 28 68
CNRS URA 2236                                   Secr: +33 (0)1 47 40 24 04
Ecole Normale Superieure de Cachan              Fax:  +33 (0)1 47 40 24 64
61, Avenue du President Wilson		
94235 CACHAN Cedex France                Email: Michel.Bidoit@lsv.ens-cachan.fr