[CoFI] Language Design - Proposed Changes to CASL

[pdmosses@brics.dk]

At the meetings in Bremen (9-11 January 1998) participants of the
Tools, Methodology, and Language Design task groups discussed issues
affecting the abstract syntax and semantics of CASL, as well as
concrete syntax.

Moreover, the meetings were followed by some e-mail discussions -
mainly between the coordinators of the Language Design, Semantics, and
Methodology task groups - leading to further proposals.

This message includes a brief summary of the proposed changes to CASL.
It will be followed (later today) by supplementary messages that
address particular topics: concrete syntax, conservative extensions,
and named morphisms.

Please note especially that the CASL design (concrete and abstract
syntax, intended semantics) is to be FROZEN after the proposed
changes, listed below, have been properly discussed on this mailing
list!  Please send any 

  INITIAL COMMENTS AS SOON AS POSSIBLE

- preferably next week, i.e., by the end of January.

  FINAL DEADLINE FOR OBJECTIONS: MONDAY 9 FEBRUARY 1998

Provided we have reached a resonable consensus concerning the proposed
changes by then, the discussions will be concluded, and the long-
awaited version 0.99 of the CASL Summary should become available by
mid-February.  (Version 1.0 is to be the polished final version, with
only cosmetic differences from version 0.99.)

Peter

----   --------------------------------------------
\  /  | Peter D. Mosses - mailto:pdmosses@brics.dk |
CoFI  | Common Framework Initiative  - Coordinator |
/  \  | WWW URL: http://www.brics.dk/Projects/CoFI |
----   --------------------------------------------


Summary of Proposed Language Changes

  For further details see subsequent messages.
  The new version of the abstract syntax (only) is available at:
  http://www.brics.dk/Projects/CoFI/Documents/CASL/Summary-v0.99

BASIC-ITEMS, SORT-GEN-ITEMS:
     The abstract syntax now reflects the grouping of basic items of the
     same kind (sorts, operations, predicates, variables, axioms).
Visibility:
     The semantics now enforces linear visibility in lists of basic items,
     everywhere except within lists of datatype declarations.  Also,
     subsort (and isomorphic sort) declarations now declare all the 
     mentioned sorts.
FREE-DATATYPE:
     This construct has been added; there are to be some restrictions on the
     DATATYPE-DECLs used in it, such that its models are the same as with a
     corresponding FREE-SPEC (but these restrictions are not reflected by
     the context-free syntax).
LOCAL-VARS-AXIOMS:
     This construct for declaring variables local to a group of axioms has
     been added.
UNIT-OP-ATTR:
     The unit may now be any TERM, not just a (constant) OP-NAME.
ALTERNATIVE:
     There is now explicit indication of totality/partiality of constructors
     and selectors.
SUBSORTS:
     More than one subsort can now be given in a single ALTERNATIVE.
REDUCTION:
     The revealing case has been generalized to allow translation of the 
     revealed symbols.
CONS-EXTN:
     Conservativeness is now allowed only an annotation--so the semantics
     no longer takes account of whether an extension is conservative.
     (See the following message from Michel Bidoit for motivation.)
GEN-SPEC:
     IMPORTS have been added, and the body is now a single SPEC.
ARCH-SPEC:
     The new grammar here corresponds closely to that in Note M-4.
LIB-NAME:
     This replaces URL, and is to be interpreted relative to a map from
     LIB-NAMEs to physical URLs of (registered) libraries.
Named mophisms:
     These are more controversial than anticipated.  See the following
     messages for a proposal, and some immediate reactions to it.