[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Comments on Abstract Syntax (addendum)
[Sorry, this further bit from BKB arrived just after I'd forwarded the
previous bits... --PDM]
these are the last comments on the AS in this iteration.
-------------- new --------------------------
DECLs and DEFNs in general
--------------------------
A re-arrangement proposal for the AS that is still going further than that
for SORTs in the comment before is one in which all DECLs and DEFNs are
grouped together such that an immediate environment map from Names/Ids to
the resp. Category and possibly a rhs emerges (in this latter case, it is a
definition). This has, I think, obvious advantages for tools and shoul also
be OK for the semantics (I think the question there should be rather: can
the Semantics group live with it since the semantics is essentially written
once and tools will have to be written by many people and efficiency is
also an issue). So let me make a proposal:
| DECL ::= decl NAME+ CATEGORY DEF
| CATEGORY ::= sort | FUN-TYPE | PRED-TYPE | var SORT
| | SPEC-TYPE | UNIT-SPEC-TYPE
| SPEC-TYPE ::= spec | gen-spec PARAM-SPEC+
[or spec PARAM-SPEC*]
|UNIT-SPEC-TYPE ::= UNIT-SPEC-NAME | UNIT-TYPE
| DEF ::= SORT-DEF
| | SPEC | ARCH-SPEC
| SORT-DEF ::= subsort-def COMPREHENSION
| | supersort-layer SORT+ -- < T1, T2
| | type-def ALTERNATIVE+ -- = A | B
| | loose-type-def ALTERNATIVE+ -- > A | B
| | sort-generation FUN-SYMB+ -- generated by F, G
CONST-DEFNs as substitute for LOCAL-VARs
----------------------------------------
The substitute for LOCAL-VARs we discussed in Paris could be easily added as
| DEF ::= ... | VAL
| VAL ::= val TERM -- = TERM
with the restriction that VAL can only appear for constants [in HO also for
general functions]
In the present AS or my proposed changes { see TYPE for HO extensions), it
would look something like
| CONST-DEFN ::= const-defn FUN-NAME CONST-TYPE TERM
where, in my proposal, we would have the obvious groupings
| FUN-TYPE ::= CONST-TYPE | FUNCTION-TYPE
| CONST-TYPE ::= SORT
| | partial-type SORT
| FUNCTION-TYPE ::= total-fun-type SORT+ SORT
| | partial-fun-type SORT+ SORT
___________________________________________________________________
Prof. Dr. Bernd Krieg-Brueckner courier mail only:
FB3 Mathematik und Informatik MZH 8071, FB3
Universitaet Bremen Universitaet Bremen
Postfach 330 440 Bibliothekstr. 1
D-28334 Bremen D-28359 Bremen
Telefon: (+49) 421-218-3660 telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE privat: (+49) 421-25-1024
http://www.informatik.uni-bremen.de/~bkb/