Up Next
Go up to Top
Go forward to 2 SORT-ITEM : Some Examples for DATATYPE-DECL

1 CASL concrete syntax related to data type declaration

A first problem is to delineate which parts of CASL are considered here as relevant for "data type declaration". The reader will find below an extract of the basic specifications concrete syntax [BCKB+97] that will be considered here (for sake of completeness, the full basic specifications concrete syntax may be found in the appendix). Among the BASIC-ITEMS, we'll focus on SORT-ITEMS and on SORT-GEN-ITEMS. 
 ...
  BASIC-ITEMS      ::=  SORT-ITEMS  |  OP-ITEMS  |  SORT-GEN-ITEMS
                     |  VAR-ITEMS  |  AXIOM-ITEMS 

! SORT-ITEMS       ::=  SORT-S SORT-ITEM;...
  SORT-S           ::=  sort  | sorts
  SORT-ITEM        ::=  SORT-DECL  |  SUBSORT-DECL  |  SUBSORT-DEFN 
                     |  ISO-DECL  |  DATATYPE-DECL
  SORT-DECL        ::=  SORT,...,SORT

  SUBSORT-DECL     ::=  SORT,...,SORT < SORT

  SUBSORT-DEFN     ::=  SORT = { VAR : SORT . FORMULA }

  ISO-DECL         ::=  SORT,...,SORT = SORT

! DATATYPE-DECL    ::=  SORT "::=" ALTERNATIVE "|"..."|" ALTERNATIVE
  ALTERNATIVE      ::=  CONSTRUCT  |  SUBSORTS
  CONSTRUCT        ::=  FUN-NAME : COMPONENT *...* COMPONENT  |  FUN-NAME
!                    |  FUN-NAME :? COMPONENT *...* COMPONENT 
! COMPONENT        ::=  ( FUN-NAME,...,FUN-NAME : SORT )  |  SORT
!                    |  ( FUN-NAME,...,FUN-NAME :? SORT )
  SUBSORTS         ::=  SORT-S SORT,...,SORT
 ...
! SORT-GEN-ITEMS   ::=  OPT-FREELY generated SIG-DECL-GROUP
! OPT-FREELY       ::=  freely  |  EMPTY
! SIG-DECL-GROUP   ::=  { SIG-DECL-ITEMS;... }
                     |  SORT-S SORT-ITEM  |  OP-S OP-ITEM
  SIG-DECL-ITEMS   ::=  SORT-ITEMS  |  OP-ITEMS
 ...
! SORT             ::=  WORDS-ID
  FUN-NAME         ::=  ID
  PRED-NAME        ::=  ID
! VAR              ::=  WORDS
In this note, we shall concentrate on DATATYPE-DECL (which is a SORT-ITEM) and on SORT-GEN-ITEMS (which are BASIC-ITEMS). The DATATYPE-DECL construct provides a concise way to describe various alternatives for a given sort, these alternatives being either subsorts or functions the codomain of which is this sort. The syntax provides the possibility to declare at the same time a function and the corresponding selectors. The SORT-GEN-ITEMS construct provides the possibility to express generating constraints.

We'll also consider the FREE-SPEC construct in the structured specifications. 

  SPEC             ::=  BASIC-SPEC  |  TRANSLATION  |  REDUCTION
                     |  UNION  |  EXTENSION  |  CONS-EXTN
                     |  FREE-SPEC  |  LOCAL-SPEC  |  { SPEC }
 ...
  FREE-SPEC        ::=  freely SPEC
Acknowledgements
This note benefited from (i) trying to explain CASL to colleagues and students, (ii) discussions with Michel Bidoit and Peter Mosses.
CoFI Note: M-2 ---- 5 January 1998.
Comments to Christine.Choppy@irin.univ-nantes.fr

Up Next