[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Abstract syntax proposal for v0.97 [250 lines]

To: cofi-language@brics.dk
Subject: Abstract syntax proposal for v0.97 [250 lines]
From: pdmosses@brics.dk
Date: Tue, 13 May 1997 12:55:06 +0200 (MET DST)
Reply-To: cofi-language@daimi.aau.dk
Sender: owner-cofi-language@daimi.aau.dk
OK, here it is.  I (really) hope that you like it...

Please let me know TODAY if you notice anything wrong!

Thanks

Peter

PS  I have to attend some meetings this afternoon, and I have
commitments this evening too, so don't expect quick reactions... 
:-(

*********************************************************************

Summary of Changes to Abstract Syntax
_____________________________________

The following changes are all motivated (I hope) by recent comments on
cofi-language concerning v0.96 of the Language Summary:

* BASIC-SPEC has been reorganized to accommodate the revised SORT-GEN,
  which now applies to a list of SIG-DECLs

* FUN-DECL has been changed (back), and CONSTANT has been eliminated
  from TERM and ALTERNATIVE, to avoid treating constants specially

* SORTS and TERMS have been introduced, to facilitate extension to HO

* FUN-DECL now allows FUN-ATTR* (corr. to PROPERTY* in v0.96)

* LOCAL-BASIC-SPEC is analogous to LOCAL-BASIC-ITEMS (App C v0.95)

* FUN-DEFN allows definitions of functions (incl. constants)
  - not restricted to use in LOCAL-BASIC-SPEC!

* EXTENSION has been tidied-up, with CONS-EXTN separated;
  GEN-SPEC has been changed consistently with EXTENSION

* ARCH-SPEC is now allowed as a SPEC

The following simplifying changes are on my own initiative, as editor
of the CASL Summary and maintainer of the abstract syntax - they do
not seem to limit expressiveness significantly:

* ATTRIBUTION has been removed

  Motivation: A FUN-DECL can now be repeated in an extension, so one
  might as well attach the attributes to a FUN-DECL, rather than a
  FUN-SYMB.  The purported advantage of ATTRIBUTION in the Rationale was
  that it allowed the same properties to be attributed at one go to
  functions with different profiles.  But when these are related by
  subsorting, it is only necessary to specify the property for the
  highest profile(s), the others inherit it.  And one probably never
  needs to attribute properties to unrelated functions in the same basic
  specification.  If anyone misses it, it will be a trivial matter to
  reinstate ATTRIBUTION.

* SUBSORT-DECL (actually EMBEDDING-DECL) has been simplified

  Motivation: The new syntax is simpler, and more consistent with
  SORT-DECL.  The new semantics of (subsort-decl S1...Sn S') is to
  declare (maybe redeclare) S1...Sn, as well as the embedding of each Si
  in S'.  Users would probably forget to declare the Si separately, and
  anyway, we shouldn't require them to repeat symbols unnecessarily...
  If anyone misses the old SORT-LAYERs, please let them provide examples
  of their usefulness!

Here is the revised grammar, to be adopted in v0.97 unless someone
can convince me that there are reasons for rejecting the changes - or
refers me to comments on cofi-language that I appear to have overlooked.
____________________________

A `!' on the left indicates a change in the grammar for the abstract
syntax in relation to that provided for the Tentative Design.  A
double `!!' indicates a change in relation to version 0.96 of the
Language Summary.  Minor changes that do not affect the language
constructs are not marked.  (The marks and this comment will be
removed in the final CASL Design Proposal.)


\subsection*{Identifiers}

\begin{grammar}
  ID		   ::=	SIMPLE-ID
  SIMPLE-ID	    --	structure insignificant for abstract syntax
\end{grammar}


\subsection*{Basic Specifications}

\begin{grammar}
!!BASIC-SPEC	   ::=	basic-spec BASIC-PART*
!!BASIC-PART	   ::=  BASIC-ITEM | SORT-GEN | LOCAL-BASIC-SPEC
!!BASIC-ITEM	   ::=	SIG-DECL | VAR-DECL | AXIOM

!!SIG-DECL	   ::=	SORT-DECL | FUN-DECL | FUN-DEFN | PRED-DECL 
!!		     |  DATATYPE-DECL

  SORT-DECL	   ::=	sort-decl SORT+

!!FUN-DECL	   ::=	fun-decl FUN-NAME+ FUN-TYPE FUN-ATTR*
!!FUN-TYPE	   ::=	TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
!!TOTAL-FUN-TYPE   ::=	total-fun-type SORTS SORT
!!PARTIAL-FUN-TYPE ::=	partial-fun-type SORTS SORT
! FUN-ATTR	   ::=	BINARY-FUN-ATTR | UNIT-FUN-ATTR
! BINARY-FUN-ATTR  ::=	associative | commutative | idempotent
! UNIT-FUN-ATTR	   ::=	unit-fun-attr FUN-SYMB
!!FUN-DEFN	   ::=  fun-defn FUN-NAME VAR-DECL* SORT TERM

  PRED-DECL	   ::=	pred-decl PRED-NAME+ PRED-TYPE
!!PRED-TYPE	   ::=	pred-type SORTS

!!SORTS		   ::=  sorts SORT*

! DATATYPE-DECL	   ::=	datatype-decl SORT ALTERNATIVE+
!!ALTERNATIVE	   ::=	CONSTRUCT 
!!CONSTRUCT	   ::=	construct FUN-NAME COMPONENT*
! COMPONENT	   ::=	component FUN-NAME? SORT

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

  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 
!		     |	EXISTL-EQUATION | STRONG-EQUATION
  TRUTH		   ::=	true | false
!!PREDICATION	   ::=	predication PRED-SYMB TERMS
  DEFINEDNESS	   ::=	definedness TERM
! EXISTL-EQUATION  ::=	existl-equation TERM TERM
! STRONG-EQUATION  ::=	strong-equation TERM TERM

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

!!SORT-GEN	   ::=	sort-gen SIG-DECL+

!!LOCAL-BASIC-SPEC ::=  local-basic-spec BASIC-SPEC BASIC-SPEC

  SORT		   ::=	ID
  FUN-NAME	   ::=	ID
  PRED-NAME	   ::=	ID
  VAR		   ::=	SIMPLE-ID
\end{grammar}


\subsection*{Basic Specifications with Subsorts}

\begin{grammar}
!!SIG-DECL	   ::=	... | SUBSORT-DECL | ISO-DECL
!!SUBSORT-DECL	   ::=	subsort-decl SORT+ SORT
!!ISO-DECL	   ::=	iso-decl SORT+

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

! ALTERNATIVE	   ::=	... | SUBSORT
! SUBSORT	   ::=	subsort SORT

  BASIC-ITEM	   ::=	... | SUBSORT-DEFN
  SUBSORT-DEFN	   ::=	subsort-defn SORT VAR SORT FORMULA
\end{grammar}


\subsection*{Structured Specifications}

\begin{grammar}
  SPEC		   ::=	BASIC-SPEC | TRANSLATION | REDUCTION | UNION
!!		     |  EXTENSION | CONS-EXTN | FREE-SPEC | LOCAL-SPEC
  TRANSLATION	   ::=	translation SPEC SIG-MORPH
  REDUCTION	   ::=	reduction RESTRICTION SPEC 
  RESTRICTION	   ::=	restriction EXPOSURE SYMB+
  EXPOSURE	   ::=	hiding | revealing
  UNION		   ::=	union SPEC+
!!EXTENSION	   ::=	extension SPEC SPEC+
!!CONS-EXTN	   ::=	cons-extn SPEC SPEC+
  FREE-SPEC	   ::=	free-spec SPEC
! LOCAL-SPEC	   ::=	local-spec SPEC SPEC

  SIG-MORPH	   ::=	sig-morph SYMB-MAP*
! SYMB-MAP	   ::=	symb-map SYMB SYMB
  SYMB		   ::=	SORT | FUN-SYMB | PRED-SYMB
\end{grammar}

\subsection*{Named and Generic Specifications}

\begin{grammar}
! SPEC-DEFN	   ::=	spec-defn SPEC-NAME SPEC
! GEN-SPEC-DEFN	   ::=	gen-spec-defn GEN-SPEC-NAME GEN-SPEC
!!GEN-SPEC	   ::=	GEN-EXTENSION | GEN-CONS-EXTN
!!GEN-EXTENSION	   ::=	gen-extension UNION SPEC+
!!GEN-CONS-EXTN	   ::=	gen-cons-extn UNION SPEC+

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

  SPEC-NAME	   ::=	SIMPLE-ID
! GEN-SPEC-NAME	   ::=	SIMPLE-ID

  ID		   ::=	... | COMPOUND-ID
  COMPOUND-ID	   ::=	compound-id SIMPLE-ID ID+
\end{grammar}


\subsection*{Architectural and Unit Specifications}

\begin{grammar}
! ARCH-SPEC-DEFN   ::=	arch-spec-defn ARCH-SPEC-NAME ARCH-SPEC
! ARCH-SPEC	   ::=	BASIC-ARCH-SPEC | ARCH-SPEC-NAME
! BASIC-ARCH-SPEC  ::=	basic-arch-spec UNIT-DECL-DEFN+ RESULT-UNIT
!!SPEC		   ::=	... | ARCH-SPEC

! UNIT-DECL-DEFN   ::=	UNIT-DECL | UNIT-DEFN
  UNIT-DECL	   ::=	unit-decl UNIT-NAME UNIT-SPEC
! UNIT-DEFN	   ::=	unit-defn UNIT-NAME UNIT-TERM

! UNIT-SPEC-DEFN   ::=	unit-spec-defn UNIT-SPEC-NAME UNIT-SPEC
! UNIT-SPEC	   ::=	UNIT-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

! ARCH-SPEC-NAME   ::=	SIMPLE-ID
! UNIT-SPEC-NAME   ::=	SIMPLE-ID
  UNIT-NAME	   ::=	SIMPLE-ID
\end{grammar}

\subsection*{Specification Libraries}

\begin{grammar}
  LIBRARY	   ::=	library URL? LIBRARY-ITEM*
  LIBRARY-ITEM	   ::=	SPEC-DEFN | GEN-SPEC-DEFN 
		     |	ARCH-SPEC-DEFN | UNIT-SPEC-DEFN | DOWNLOAD
! DOWNLOAD	   ::=	download URL ITEM-NAME-MAP+
! ITEM-NAME-MAP	   ::=	item-name-map ITEM-NAME? ITEM-NAME
! ITEM-NAME	   ::=	SPEC-NAME | GEN-SPEC-NAME 
!		     |	ARCH-SPEC-NAME | UNIT-SPEC-NAME

  URL		   ::=	url SITE? DIRECTORY
  SITE		   --  structure insignificant for abstract syntax
\end{grammar}

*******************************************************************
Prev by Date: final comments on v0.96
Next by Date: moderation
Prev by thread: final comments on v0.96
Next by thread: moderation
Index(es):
- Date
- Thread