[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [CASL] concrete syntax - mixfix, imports
Dear Peter,
Peter Mosses wrote:
>
> Dear Bernd,
>
> > Sorry I didn't have the time to comment on syntax so far.
> > Everything seems to be basically OK, as I learn from scanning the mail
> > and discussion with Till.
> >
> > Just a few small comments:
> >
> > Peter Mosses wrote:
> > >
> > >
> > > One further point concerning mixfix parsing:
>
> (which doesn't concern context-free parsing at all, of course)
>
> > > Thanks to linear visibility, one has the anomaly that a mixfix
> > > application that parsed OK may become ambiguous due to later
> > > declarations - even in the same basic spec! It might be better to be
> > > more strict, taking account of all the mixfix patterns declared in a
> > > basic spec (as well as the local environment), regardless of their
> > > order. This slightly increases the chance of rejection due to
> > > ambiguity of grouping, but ensures that rejection is independent of
> > > the order of basic items. Linear visibility can still be enforced by
> > > subsequently rejecting use before declaration (except in datatype
> > > declarations, of course...). This should perhaps have been made
> > > explicit somewhere in App C?
> > >
> > I agree and it merits an explanation. The non-linearness only affects
> > mixfix parsing patterns, I hope.
>
> OK. I'd previously proposed adding:
>
> C.3 Disambiguation
>
> The given grammar for input syntax is quite ambiguous. This section
> provides some precedence rules for disambiguation.
> !
> At the level of structured specifications, ambiguities of grouping
> are resolved as follows:
> ...
> The declaration of infix, prefix, postfix, and general mixfix
> operation symbols may introduce further potential ambiguities, which
> are partially resolved as follows (remaining ambiguities have to be
> eliminated by explicit use of grouping parentheses in terms, or by use
> ! of parsing annotations). Note, however, that the recognition of the
> ! exact applicative structure of mixfix atomic formulae and terms is
> ! inherently context-dependent. Consequently, the precedence rules
> ! for atomic formulae and terms given below cannot be incorporated in
> ! context-free parsing, but must be left to a subsequent phase of the
> ! analysis. For specifications that use only the standard prefix
> ! notation for application of predicates and operations, the
> ! precedence rules below are irrelevant, and the applicative structure
> ! of atomic formulae and terms is unambiguous. A parsing annotation
> ! may be introduced to indicate whether a particular specification or
> ! library uses mixfix notation or not.
>
> so I suggest to append to that:
>
> ! To avoid the mixfix analysis of an atomic formula or term being
> ! dependent on its position in a list of basic items, all the
> ! declarations of symbols in the enclosing basic specification are
> ! taken into account (but of course the subsequent static
> ! analysis should still reject the use of a symbol before its
> ! declaration, in general).
>
> Suggestions for improved wording are, as always, very welcome!
OK, except that, pragmatically, instead of "enclosing basic
specification" it is probably the whole text in the file that is being
parsed for which the mixfix patterns are computed in the first parse,
and then used subsequently; or is it perhaps the resp. libray item that
is treated one by one individually?
>
> > In general, I prefer {} to () in the "in-the-large" part.
> >
> > I was a little surprised about the () for SOME-IMPORTS:
> > are they really necessary? the section is always lead by "given"
> > and terminated by "[". If not, delete.
>
> I believe that they are necessary (which was why they were introduced
> at all!): without arbitrary lookahead, one cannot tell whether "[" is
> part of an instantiation in an import or part of the first parameter.
>
> I know that others have reservations about putting the (boring)
> imports before the (more significant) generic parameters, and for
> methodological reasons would prefer to keep to the order of v0.99,
> then also omitting the parentheses. There's a tension here with the
> visibility rules: the parameters actually extend the imports, so users
> might be surprised if the parameters come first. (They may be even
> more surprised that the arguments of instantiations also extend the
> imports, but at least that issue doesn't affect the syntax...)
> I guess there should be consistency with the syntax for imports in
> arch specs too.
>
> *** Please would those who have strong feelings about the concrete
> syntax for imports state their preferences NOW.
I definitely prefer parameters first, as before. I see now problem with
the semantics, if the order is explained. We do not have to follow the
semantics slavishly in the concrete syntax.
>
> Perhaps we can wait with settling this issue until Monday (EU time),
> without jeopardizing the schedule for releasing the final v1.0 on 22
> Oct. Maybe you'd like to air it on cofi-language too.
>
> > Definitely, f(x) should have preference as parsing as such, or
> > ambiguity, if anonymous operators are there (nobody will use them
> > anyway).
>
> The point of the discussion with Frederic was whether this preference
> should occur during context-free parsing or (context-dependent) mixfix
> analysis. Our conclusion was the latter. Thus "map f (x)" will be
> legal and grouped as "map__ __(f,x)" after declaring map__ __:s*s->s,
> f:s, and x:s. If the "f(x)" were to be irrevocably context-freely
> parsed as an application, "map f (x)" would not be legal (although one
> could still write it as "map(f)(x)"). Please react straight away if
> you see reasons to object to this.
No, no, this is fine!
>
> > The clarification on p 25: does this really mean that an
> > "overloading" of f and f __ is possible with the same profile,
> > since they are distinct symbols? If not (I hope), then the
> > wording has to be slightly more careful.
>
> In principle, such overloading is indeed allowed. However, as soon as
> one has declared both f and f__, "f(x)" would be deemed ambiguous
> regarding the mixfix analysis, regardless of the sorts in the
> profiles, so it'd be difficult to make use of it in practice. It
> seems simpler to live with this than to take the trouble to ban such
> overloading explicitly.
Exactly, people will then avoid it.
>
> There is a related issue that I'd like to check here: should the
> mixfix analysis take account of the particular number of argument
> sorts in non-mixfix declarations or not? E.g., consider
> ops f:s*s->s; f__:s->s; c:s
> the question is whether f(c) has a unique mixfix analyis or not. My
> personal opinion is that the non-mixfix declaration f:s*s->s should
> have the same effect as if one had declared f(__,__):s*s->s (note that
> parentheses and commas are not allowed in IDs, so one can't actually
> write such a mixfix declaration). Thus f(c) is unambiguously analysed
> as an application of f__. (I believe that Bjarke's prototype mixfix
> analyser implements my preference, but I haven't checked that yet.)
>
> In summary, I'd like to say that mixfix analysis should take full
> account of the number and placing of arguments of declared symbols
> (but not of the argument/result sorts). OK?
OK
>
> > page C-9: I wish we had the European currency symbol in addition
> > to Dollar and Pound;
>
> What does it look like? Is it available in some ISO character set?
> or in Unicode?
>
> > is the universal currency symbol perhaps for this
> > purpose in the future?
>
> Then perhaps the euro should have been called a "uni"! :-)
>
> -- Peter
> _________________________________________________________
> Dr. Peter D. Mosses International Fellow (*)
>
> Computer Science Laboratory mailto:mosses@csl.sri.com
> SRI International phone: +1 (650) 859-2200 ! CHANGED
> 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
> _________________________________________________________
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