[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Comments on Abstract Syntax
New proposals are marked with a | in the left hand margin.
[Comments in square brackets below are by Bernd himself, NOT by the
moderator. --PDM]
General Improvements
--------------------
In general, I beleive that the AS should often be made more "flat" by
allowing cases to be alternatives rather than introducing an extra
constructor that introduces yet another level in any AS tree and makes the
usual case tree bigger.
A good example is
| APPLICATION ::= application FUN-SYMB TERM+
| | FUN-SYMB
[obviously, one could also introduce the special case directly in TERM, say
as CONST (next to VAR); this is a matter of emphasis]
similarly PREDICATION, FUN-TYPE (see below) or (more importantly)
| FUN-SYMB ::= FUN-NAME
| | fun-symb FUN-NAME FUN-TYPE
[I prefer this order with the simple case first, also in APPLICATION]
This way, a TERM can directly be a FUN-NAME; also, I believe that the
semantics will have to distinguish between the resp. 2 cases anyway. Note
that this all becomes easily possible in a CASL representation of trees, as
opposed to some other languages (?).
A consequence is that TERM is then a supertype of FUN-SYMB. Thus an
eventual extension of APPLICATION to HO will just have to move up to:
| application TERM TERM+
It is worth thinking about removing "?" [option] altogether this way.
Another case where a lot of (unnecessary?) constructors are introduced that
*every* tool will always have to make a case distinction about is that
where a static restriction is made of a more general case; however, once
the static restriction has been checked, it is a burden. Now this remark is
very general, but let me give you a typical example:
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
Why not
| SYMB-MAP ::= symb-map SYMB SYMB
and use a static restriction, i.e. a structural predicate (in the static
semantics) or the concrete syntax which is likely to check this anyway.
[I would even re-use this as SPEC_NAME_MAP]
Distinction between FUN and PRED
--------------------------------
Quite obviously, the context determines whether a NAME is a FUN-NAME or
PRED-NAME, as for SORT or VAR. However, here it is even more complicated
since the same NAME can be overloaded as a FUN-NAME or PRED-NAME. In the
semantics, these names are fully qualified anyway (after overload
resolution). So why keep the distinction in the AS? This means that the
first context-free parsing phase will build evrything as one (say FUN-...)
and then re-build after the static semantics phase.
Perhaps more inportantly, the concrete syntax has to be written in an
awkward way, since Predication will also go to Term (with als the business
about infix, prefix, postfix etc.) unless one duplicates it.
So I ask you to think about reconsidering the distinction [now I must have
shocked some of you, but please go on reading]
TYPE for HO extension
---------------------
In the spirit of the discussion above about flattening the AS, and the
preparation for extension to HO, I propose
| FUN-TYPE ::= SORT
| | partial-type SORT
| | total-fun-type SORT+ SORT
| | partial-fun-type SORT+ SORT
[or in some other order, or with extra non-terminals]
| PRED-TYPE ::= pred-type SORT*
Even better would be
| FUN-TYPE ::= TYPE
| | partial-type TYPE
| | total-fun-type TYPE+ TYPE
| | partial-fun-type TYPE+ TYPE
| PRED-TYPE ::= pred-type TYPE*
| TYPE ::= SORT
[better: SORT-NAME to emphasize]
then only the rhs of TYPE has to be changed for HO.
[I would even prefer to introduce an extra PROD-TYPE for products, and
TUPLE as a TERM; also application FUN-SMB TERM]
SORTED-TERM and FUN-SYMB
------------------------
There is a nasty ambiguity in the concrete syntax, if one wants to have the
same symbol to denote sorting in SORTED-TERM and for a qualified FUN-SYMB;
I guiess this is not so far fetched as ":" seems to be the preferred symbol
here which I went to some trouble to realizeas well.
The ambiguity is whether X:T is a FUN-SYMB [i.e. an APPLICATION] or a
SORTED-TERM? I vote for the latter; then we get:
| APPLICATION ::= application FUN-SYMB TERM+
| | FUN-NAME
SORTED-TERM ::= sorted-term TERM SORT
one more reason for the split advocated above.
Small proposals
---------------
| SORT-GEN ::= sort-gen FUN-SYMB+ SORT
[order; why more than one SORT?]
| SIG-MORPH ::= sig-morph SYMB-MAP+
[why allow empty one?]
| UNIT-REDUCT ::= unit-reduct UNIT-TERM SIG-MORPH
[more consistent with rest, where SIG-MORPH alway comes last]
| LIBRARY ::= library URL? LIBRARY-ITEM+
[why allow empty one?]
better:
| LIBRARY ::= library URL LIBRARY-ITEM+
| LIBRARY-ITEM+
[to flatten out]
Non-generic and Generic Specs
-----------------------------
I believe there was a tendency at the last meeting to separate between
non-generic and generic specs; I support this!! Anyway look at my previous
comments for analogy to constant and other functions.
| SPEC-DEFN ::= spec-defn SPEC-NAME SPEC
| | generic-spec-defn SPEC-NAME PARAM-SPEC+ SPEC
| PARAM-SPEC ::= OF-SPEC
[depending on what happens there]
In any case, I would prefer GEN-SPEC to go since it looks as if it is meant
to appear "on the right hand side" of the DEFN; i.e. expand GEN-SPEC
inline.
SORT DECLs and DEFNs
--------------------
With the "inline" interpretation of type definitions now, the association
of "loose" and "tight" ones (never mind the terminology, see my previous
comment), and moreover the interpretation "a sort-decl/defn *contributes*
to those already present", it is perhaps in order to re-group all this a
little bit in the Abstract Syntax, as follows: [some concrete syntax in
comments]
| SORT-DECL ::= sort-decl SORT+ -- S1, S2: sort
| | subsort-decl SORT+ SORT+ -- S1, S2: sort < T1, T2
[subsort-decl adds one SORT-LAYER and introduces S1, S2, if not already defined]
| SORT-DEFN ::= subsort-defn SORT COMPREHENSION
| | tight-sort-defn SORT ALTERNATIVE+ -- S: sort = A | B
| | loose-sort-defn SORT ALTERNATIVE+ -- S: sort > A | B
| | sort-generation SORT FUN-SYMB+
[in the first two rules, SORT must not be added to later, except by an
ISO-decl (see below)]
Note that an isomorphism sort declaration is now a special case of a
tight-sort-defn:
S: sort = T
This seems very natural to me; never mind that multiple iso-decls require
more writing now; this is the rare case. Similarly, I think it is quite
sufficient to introduce one SORT-LAYER at a time. Note that now embedding
and iso decls and sort-gens are subsumed above; everything that may
contribute to a (sub)sort is either a SORT-DECL or a SORT-DEFN.
AS a general rule, SORT-DECL or SORT-DEFN always *may* introduce a new
SORT-name [before the colon] and use others already defined (before or
after) in their rhs.
A consequence of the interpretation "a sort-decl/defn *contributes* to
those already present" is that there are two ways to introduce a
sub/supersort relationship:
(1) S: sort < T -- subsort-decl
(2) T: sort > S -- loose-sort-defn
If S *and* T are both defined, this introces a sub/supersort relationship;
if T is defined, (1) can be used to define a subsort S; if S is defined,
(2) can be used to define a supersort T. This seems all quite natural to
me.
___________________________________________________________________
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
NEW: http://www.informatik.uni-bremen.de/~bkb