Changes to CASL abstract syntax from v0.94

[pdmosses@brics.dk]

Version 0.95 FINAL DRAFT was announced on cofi-list yesterday;
if you didn't receive it, please refer to the archives of cofi-list.
(All CoFI participants are expected to subscribe to cofi-list.
BTW, I've at last updated the majordomo info files, so they no longer
refer to the non-existent cofi-task - sorry for any confusion caused!)

All significant changes to the CASL abstract syntax between v0.94 and
v0.95 should be indicated below by exclamation marks in the left margin.
Please let me know if I've inadvertently missed some.  (I don't count
uniform changes of nonterminal as significant.)

Note that several of the changes are marking replacement of ... X X+
by ... X+ - the restriction to lists with at least two items is now
merely a well-formedness condition.  Some of the other marked changes
are just internal reorganization of the tree structure of the abstract
syntax.

Peter

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

Appendix A: Abstract Syntax

Basic Specifications

  BASIC-SPEC      ::=   basic-spec BASIC-ITEM*
! BASIC-ITEM      ::=   SIG-DECL | VAR-DECL | AXIOM
                  |     SORT-GEN | TYPE-DEFN-GROUP

  SIG-DECL        ::=   SORT-DECL | FUN-DECL | PRED-DECL
  SORT-DECL       ::=   sort-decl SORT+
  FUN-DECL        ::=   fun-decl  FUN-NAME+ FUN-TYPE
  PRED-DECL       ::=   pred-decl PRED-NAME+ PRED-TYPE
  FUN-TYPE        ::=   fun-type  TOTALITY SORT* SORT
  TOTALITY        ::=   total | partial
  PRED-TYPE       ::=   pred-type SORT*

! VAR-DECL        ::=   var-decl VAR+ SORT

  AXIOM           ::=   FORMULA
  FORMULA         ::=   QUANTIFICATION | CONJUNCTION | DISJUNCTION 
                  |     IMPLICATION | EQUIVALENCE | NEGATION | ATOM
  QUANTIFICATION  ::=   quantification QUANTIFIER VAR-DECL+ FORMULA
  QUANTIFIER      ::=   forall | exists | exists-uniquely
! CONJUNCTION     ::=   conjunction FORMULA+
! DISJUNCTION     ::=   disjunction FORMULA+
  IMPLICATION     ::=   implication FORMULA FORMULA
  EQUIVALENCE     ::=   equivalence FORMULA FORMULA
  NEGATION        ::=   negation FORMULA

  ATOM            ::=   TRUTH | PREDICATION | DEFINEDNESS | EQUATION
  TRUTH           ::=   true | false
  PREDICATION     ::=   predication PRED-SYMB TERM*
  DEFINEDNESS     ::=   definedness TERM
  EQUATION        ::=   equation QUALITY TERM TERM
  QUALITY         ::=   existential | strong

  TERM            ::=   VAR | APPLICATION | SORTED-TERM
  APPLICATION     ::=   application FUN-SYMB TERM*
  SORTED-TERM     ::=   sorted-term TERM SORT

  SORT-GEN        ::=   sort-gen SORT+ FUN-SYMB+

  TYPE-DEFN-GROUP ::=   type-defn-group TYPE-DEFN+ AXIOM*
! TYPE-DEFN       ::=   type-defn SORT ALTERNATIVE+
  ALTERNATIVE     ::=   CONSTRUCT
  CONSTRUCT       ::=   construct FUN-NAME COMPONENT*
  COMPONENT       ::=   SORT | SELECTION
  SELECTION       ::=   selection FUN-NAME SORT

  FUN-SYMB        ::=   fun-symb FUN-NAME FUN-TYPE?
  PRED-SYMB       ::=   pred-symb PRED-NAME PRED-TYPE?

! SORT            ::=   SIMPLE-ID
  FUN-NAME        ::=   SIMPLE-ID
  PRED-NAME       ::=   SIMPLE-ID
! VAR             ::=   SIMPLE-ID


Basic Specifications with Subsorts

  BASIC-ITEM      ::=   ... | EMBEDDING-DECL | PRED-SORT-DEFN

! EMBEDDING-DECL  ::= embedding-decl SORT-LAYER+
  SORT-LAYER      ::= sort-layer SORT+

  PRED-SORT-DEFN  ::= pred-sort-defn SORT VAR-DECL FORMULA

  ATOM            ::=   ... | MEMBERSHIP
  MEMBERSHIP      ::=   membership TERM SORT
  TERM            ::=   ... | CAST
  CAST            ::=   cast TERM SORT

  ALTERNATIVE     ::=   ... | SORT


Modular Specifications

  SPEC            ::=   BASIC-SPEC | TRANSLATION | REDUCTION
                  |     UNION | EXTENSION | FREE-SPEC
  TRANSLATION     ::=   translation SPEC SIG-MORPH
  REDUCTION       ::=   reduction RESTRICTION SPEC 
! RESTRICTION     ::=   restriction EXPOSURE SYMB+
! EXPOSURE        ::=   hiding | revealing
  SYMB            ::=   SORT | FUN-SYMB | PRED-SYMB
! UNION           ::=   union SPEC+
  EXTENSION       ::=   extension OF-SPEC* SPEC
  OF-SPEC         ::=   PERSISTENT-SPEC | SPEC
  PERSISTENT-SPEC ::=   persistent-spec SPEC
  FREE-SPEC       ::=   free-spec SPEC

  SIG-MORPH       ::=   sig-morph SYMB-MAP*
  SYMB-MAP        ::=   SORT-MAP | FUN-SYMB-MAP | PRED-SYMB-MAP
  SORT-MAP        ::=   sort-map SORT SORT
  FUN-SYMB-MAP    ::=   fun-symb-map FUN-SYMB FUN-SYMB
  PRED-SYMB-MAP   ::=   pred-symb-map PRED-SYMB PRED-SYMB


Generic Specifications

! SPEC-DEFN       ::=   spec-defn SPEC-NAME GEN-SPEC
  SPEC-NAME       ::=   SIMPLE-ID
! GEN-SPEC        ::=   gen-spec OF-SPEC* SPEC

  SPEC            ::=   ... | SPEC-INST
  SPEC-INST       ::=   spec-inst SPEC-NAME FITTING-ARG*
  FITTING-ARG     ::=   fitting-arg SPEC SIG-MORPH?

  SORT            ::=   ...| COMPOUND-ID
  FUN-NAME        ::=   ...| COMPOUND-ID
  PRED-NAME       ::=   ...| COMPOUND-ID
  COMPOUND-ID     ::=   compound-id SIMPLE-ID ID+
  ID              ::=   SIMPLE-ID | COMPOUND-ID


Architectural Specifications

! ARCH-SPEC-DEFN  ::=   arch-spec-defn SPEC-NAME ARCH-SPEC
! ARCH-SPEC       ::=   arch-spec UNIT-DECL+ RESULT-UNIT

  UNIT-DECL       ::=   unit-decl UNIT-NAME UNIT-SPEC
  UNIT-NAME       ::=   SIMPLE-ID

! UNIT-SPEC-DEFN  ::=   unit-spec-defn SPEC-NAME UNIT-SPEC
! UNIT-SPEC       ::=   SPEC-NAME | UNIT-TYPE
  UNIT-TYPE       ::=   unit-type SPEC* SPEC

! 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


Specification Libraries

  LIBRARY         ::=   library LIBRARY-ITEM*
! LIBRARY-ITEM    ::=   SPEC-DEFN | ARCH-SPEC-DEFN | UNIT-SPEC-DEFN


Simple Identifiers

  SIMPLE-ID       -- structure insignificant for abstract syntax