[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [CoFI] Concrete + Abstract Syntax: minor comments




Dear Peter,
some final comments.

> Abstract Syntax
> ---------------
> 
> I think an extra constructor for
>         gen-datatype DATATYPE-ITEMS
> is needed
> 
> [Isn't is merely a special case of sort-gen SIG-ITEMS+, both regarding
> syntax and semantics?  --PDM]

No, the special case comes with {} , i.e. "generated {type ...}"
whereas "generated type ..." is at the same level as "free type ...". 
Thus one should distinguish as, presumably, tools (transformation,
unparsing etc.) will want to take advantage of the special case; or do
we rely on them to always take the context (see examples above) into
account in a case analysis? Unfortunately, the context to determine that
there is just one type def inside the brackets is until the end of the
bracket; on the other hand, this means that the list of SIG-ITEMS is
singular.

[I believe that the situation is analogous to explicit grouping
 parentheses in TERMs: there is no abstract syntax for grouping, so its
 use has to be kept as auxiliary information (attributes) in the
 abstract syntax tree.  Here, the information is that *no* braces
 "{...}" are needed/wanted around the singleton list of SIG-ITEMS, but
 the same principle applies: semantically irrelevant information that
 is needed by tools gives rise to attributes, but not to new kinds of
 abstract syntax nodes. 
--PDM]

Keywords
--------
I know this is extremely late, but is it really necessary to have the
"ing" in some of the keywords? [add an "ing" to your pet keyword!]
Why not use a more "imperative" style:
	hide, reveal, rename, fit
as in
	use [is no longer used --PDM], import, ...
this is not only much shorter but also means that non-native speakers do
not need to remember to put two Ts in fitting :-)

[I have nothing much against this proposal EXCEPT for its lateness!!! 
 Due to winter holidays in various countries, we cannot assume that
 everyone is reading e-mail this week.  Would those who support it, or
 oppose it, please let me know IMMEDIATELY!  If most of you are in
 favour, we may adopt it tentatively, with the possibility of reverting
 at the last moment if the others protest on their return to the net... 
--PDM]

Arrows in morphisms
-------------------
I find it very confusing for the beginner that the arrows |-> go one way
in renamings and the other in fitting morphisms. I know abstractly from
the theoretical background that the fitting morphisms go "the other way
round", but regard this rather as a technical detail. I am afraid that
this only occurred to me late last week when discussing with Till;
indeed there are some special cases when fitting can be replaced by
renaming. [I thought that this was actually the general case?  --PDM]
When both are next to each other it is particularly confusing;
see e.g. the example in SyntaxExamples:
spec PATH
	NON_EMPTY_LIST_OF[NAME fitting Item |-> Name]
		renaming List[Name] |-> Path, ...
My suggestion: regard "|->" as a symbol for substitution, and change the
direction in fittings.

[The fitting applies to the implicit parameter spec, e.g., spec ITEM =
 sort Item.  The induced renaming is applied to NON_EMPTY_LIST_OF[ITEM],
 and the fitting seems to me to go in the right direction for
 consistency with renaming.  Please would those who have opinions on
 this issue send them to cofi-language@brics.dk as soon as possible.
--PDM] 

best regards
Bernd 
________________________________________________________________
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
http://www.uni-bremen.de/~sppraum