Re: [CoFI] Proposal for named morphisms in CASL - CORRECTION

[Didier Bert <Didier.Bert@imag.fr>]

[Sorry, this arrived about 10 secs after I'd forwarded Didier's other
message!  And yes, I should have caught the mistake myself...  --PDM]

   Dear Peter,

I have not a copy of my e-mail, but I wonder if I did not do a mistake on
the abstract syntax. The definition of views must be as Hubert shown,
from SPEC-NAME to SPEC-NAME. For generic views, we must have only SPEC-NAME
followed optionally by a "formal" instance, if this notion is available
in the language (i.e. an instance of parameters by formal entities).

   VIEW-DEFN ::= view-defn VIEW-NAME VIEW
   VIEW ::= view SPEC-NAME SPEC-NAME SYMB-MAP*

Example of generic view (I don't check the syntax [I've corrected it -
except that for the views: I suggest we defer all discussion of the
concrete syntax of views until their abstract syntax and semantics
have been settled. --PDM]):

    spec EQ =
    BOOL then
	sort t
	ops  eq : t*t -> bool
	...
    end

    spec LIST [EQ] =
    	sort list[t]
	ops  nil : list[t];
	     ...
	     __==__ : list[t]*list[t] -> bool;
	...
    end

    view Eq-List [EQ] =
	EQ --{ t |-> list[t], eq |-> __==__ }--> LIST [EQ]

    view Eq-Nat =
	EQ --{ t |-> nat, eq |-> __==__ }--> NAT

    spec MY_LISTS =
    LIST[LIST[NAT]]	%% or LIST[Eq-List[Eq-Nat]]
    then
	ops ...
    end

Thanks for correcting my syntax.
Didier

----------------------------------------------------------------------------
Dr. Didier Bert			   http://www-lsr.imag.fr/users/Didier.Bert/
CNRS, Laboratoire LSR-IMAG	   Tel: 04 76 82 72 16	    +33 476 82 72 16
681, rue de la Passerelle 	   Fax: 04 76 82 72 87	    +33 476 82 72 87
BP 72 
38402 Saint-Martin-d'Heres CEDEX, France
----------------------------------------------------------------------------