[CASL] concrete syntax - mixfix, imports

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

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!

> 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.

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.

> 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.

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?

> 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
_________________________________________________________