Re: Literal Syntax

[Peter Mosses <mosses@csl.sri.com>]

Dear Markus and Till,

Thanks for your prompt reconsideration of the proposal.

> > In summary: I'm sympathetic towards most of the proposed syntax for
> > literals themselves, but I'd much prefer to use annotations (rather
> > than attributes and new forms of datatype declarations) for linking
> > the literal syntax to declarations of operations.
> 
> OK, this would be more uniform with the other syntax annotations
> (precedences and associativities). However, note that the syntax
> annotations have an impact on the way how concrete syntax is
> translated to abstract syntax, and thus also indirectly
> influence the semantics of a given piece of concrete syntax.

Of course - but once they have had their influence on the creation of
the abstract syntax, their only remaining relevance is to formatting
tools, I think.

> A similar argument holds for the semantic annotations,
> which can generate proof obligations, like e.g. instantiations
> of generic specifications also do. Dieter Hutter told me that he
> found this confusing and would prefer more uniformity.
> This would mean to turn the semantic and parsing annotations into
> constructs of the language, while annotations are used
> for more special things like simplicifation orderings.
> Anyway, I agree that the literal syntax declarations
> should have the same status as the parsing annotations
> (regardless whether they are language constructs or annotations).

My impression is that there is general agreement in the Language
Design, Tools, and Semantics task groups on the usefulness of
separating both parsing and semantic annotations from language
constructs.  Any change in policy here would need a thorough
discussion.  Perhaps our explanation of the general role of
annotations needs improving, to avoid anyone finding them confusing;
suggestions for how to do that are welcome!

> > It might be good to cater also for binary, octal, and hexadecimal
> > notation for numbers.  Isn't there a rather standard notation for
> > indicating the base, by prefixing a sequence of digits by `2#', `8#',
> > or `16#'?  It should be easy to add this (now or in some later
> > extension), provided that words are not allowed to start with a digit;
> > otherwise, one might need to remove further patterns of letters and
> > digits from WORD...
>
> OK. In C, hexadecimal numbers are prefixed with 0x.

Fine (so long as x followed by a digit can still be a WORD :-)

> > Each single digit could be reserved too - or is it important to allow
> > the use of the constants `0' and `1' in non-numerical specifications?
> 
> Exactly, 0 and 1 could, for example, be used in
> 
> free type  bit ::= 0 | 1

OK - and bit should definitely not be a subsort of nat!

(BTW, sorry that the lines in my message were so long: the wrapping of
them when you cited them in your reply has made it difficult to read.)

> >   Literal syntax for lists
> >
> >        DATATYPE-DECL   ::= SORT "::=" ALTERNATIVE "|"..."|"
> >                                       ALTERNATIVE , LIST-BRACKETS
> >        LIST-BRACKETS ::= brackets SIGNS-BACKETS PLACE SIGNS-BRACKETS
> >
> >   The attribute for declaring a list-like syntax for a datatype is
> >   written `brackets b1 __ b2'. Thus enclosing datatype declaration
> >   declaring the sort s must consists of excatly two ALTERNATIVEs:
> >   the first has to be a constant c of arbitrary argument type,
> >   while the second is a constructor f with exactly two argument
> >   sorts, the second of which has to be s. 
> > ________________________________________________________________________
> >
> > Although the above proposal allows the introduction of neat notation
> > for literals of various sorts of collections (e.g. {e1,...,en} for
> > sets, as well as [e1,...,en] for lists), I find the means used to
> > determine the translation quite ugly.  In particular, it seems strange
> > to REQUIRE the use of a DATATYPE-DECL; what about sub-languages that
> > don't support this construct?
> >
> > Couldn't one instead use annotations for indicating that any outfix
> > operation `b1 __ b2' is a unary bracketing constructor, determining at
> > the same time the intended `nil' and `cons' (or `conc') operations
> > used in translating non-unary applications?  How the latter
> > constructors have been declared is then irrelevant.
> 
> OK, Bernd proposed a similar thing.
> This would mean something like
> 
> free type List[Elem] ::= nil | cons (Elem; List[Elem])
> op [__] : Elem -> List[Elem] %bracket-ops nil, cons

Right, much better.

> I will try to revise the proposal on Friday.

Thank you, I'll look forward to that - and to Bernd's decision about
whether it is ready to be incorporated in the Summary.

Cheers,

-- Peter
_________________________________________________________
Dr. Peter D. Mosses             International Fellow  (*)

Computer Science Laboratory     mailto:mosses@csl.sri.com
SRI International               phone: +1 (650)  859-2200
333 Ravenswood Avenue           fax:   +1 (650)  859-2844
Menlo Park, CA 94025, USA       http://www.brics.dk/~pdm/

(*) on leave from DAIMI & BRICS, University of Aarhus, DK
    also affiliated to CS Department, Stanford University
_________________________________________________________