Re: concrete syntax problems in arch spec and views

[mosses@csl.sri.com]

Dear Frederic,

Thanks for your valuable feedback regarding the finalization of the
CASL concrete syntax.

> Here is a short list of the current problems with the concrete syntax
> for Casl. I did not have the opportunity to check with Christophe the
> completeness of the list below, but for basic items it seems to work...
> The major problem comes with the proposed syntax for architectural
> specs and views. A message from Christophe in July mentioned many problems
> brought by the new proposal and the solution proposed by Peter and
> Michel (restricting in various places specification to named specifications
> or "bracketed" specifications) does not solve all of them, mainly some
> problems related to symbol maps... I'm currently investigating what
> can be done.. (about 60 shift-reduce conflicts come from the new
> features...)

I.e., from the possibility of interspersing the keywords "sorts",
"ops", and "preds" between the symbol maps?

> There are also problems with the syntax of PATHs when naming specifications.

I don't see anything called PATH in the grammars in the Summary v0.99;
I guess you mean the use of "/" in LIB-ID?  Notice that this is not
allowed when referring to a spec, only to a library.

> By being more restrictive (i.e. using a lexical convention...).

(I couldn't quite parse that sentence!  Anyway:) I don't understand
why there should be a problem here: something like "A/B/C" should get
lexically analysed as a sequence of SIMPLE-IDs, i.e., WORDSs,
separated by the literals "/" (which also may be used as a TOKEN, but
not in a SIMPLE-ID).  Please clarify where the problem occurs.

> Maybe we can live without that feature for the current version ??

I'd prefer not to remove the possibility of hierarchical library names
in CASL v1.0. If the concrete syntax of LIB-ID in CASL v0.99 is
problematic, kindly suggest how it might be adjusted to facilitate
parsing.  (This is admittedly a very minor detail of the language; but
one of the benefits of your work is in revealing such problems with
details, so we should try to resolve the issue now, if possible.)

> Frederic
> ------------------------------------------------------
> 
> Micro-problems/ambiguities in the current document
> 
> - In a definition by extension, spaces are needed around the '.'
>   NO: 	Odd = {n:Nat.odd n}  %% Note that ".odd" is a valid token
>   Yes:	Odd = {n:Nat . odd n}

I see the need for the second space, but not for the first one: while
"Odd = {n:Nat .odd n}" should probably be invalid, I'd expect 
"Odd = {n:Nat. odd n} to be valid.

Moreover, isn't it just the same situation as with QUANTIFICATION:
"forall n:Nat.odd n" and LOCAL-VAR-AXIOMS: "var n:Nat.odd n"?  
Why should SUBSORT-DEFN be special in this respect?

Of course, some might prefer to remove the rather odd-looking
DOT-WORDS from the language altogether, since it also prevents using
"." as in infix operation, and might hinder the introduction of the
notorious "dot-notation" in extensions of CASL.  But let's not waste
our precious time on this relatively minor issue, which has already
been debated at considerable length - extensions will in any case have
to restrict the CASL lexical syntax for ID so as to reserve new
keywords, and they might just as well be allowed to remove DOT-WORDS
at the same time.

> - <Sort> is defined as <TokenId>. Probably it should be a <SimpleId>

NO!  In structured specs, TOKEN-ID allows for compound ids, such as
"List[Elem]", whereas SIMPLE-ID is still merely WORDS.

> - Are both ->? and -> ? needed ? Or which form is the right one ?

For the ASF+SDF CASL v0.99 parser (see ftp://ftp.brics.dk/Projects/CoFI/
Documents/CASL/SyntaxExamples/ASF+SDF/ZCasl-BasicItems.syn) Bjarke
only allowed "->?".  (I recall rationalizing this once, in connection
with extensions to higher-order, but I'm not sure that my arguments
were so compelling...)

> - The "display annotations" must probably be allowed also for symbols
>   declared in renamings, not only in "declarations"

Right - because new symbols can be introduced there too.  Thanks,
I hadn't noticed that.  The same goes for fittings in instantiations;
so I suggest to provide these annotations uniformly for SYMB-MAP-ITEMS.

> - the tokens -> and ->? are not described as being complete reserved tokens

Neither is "*"; presumably the treatment of these symbols should be
analogous?  Perhaps the explanation in App. C.4:

  `(since they all have to be recognized as terminal symbols)'

is misleading.  As far as I can see, one needs to make sure that a
terminal symbol which can terminate an ID, TERM, or FORMULA cannot
also be a valid complete TOKEN.  That motivates reserving:

  :  :?  =  =>  <=>  .  |  |->  \/  /\  {  }  [  ]

as well as most of the keywords.  (Maybe "::=" should be left
unreserved, although I can't imagine anyone wanting to use it.)  I
don't see any *technical* reason for reserving tokens such as "*" and
"->", since when they are used in FUN-TYPE in TERM, they always follow
a SORT, which is a single TOKEN-ID.  

However, perhaps "->" and "->?" should be reserved to avoid problems
with parsing arising in a higher-order extension of CASL (where the
distinction between SORT and TERM may disappear).  The question is
then whether "*" should be reserved too - I hope not!  In fact I'd
prefer to regard all of "->", "->?" and "*" as ordinary tokens usable
as infix operators (but getting a predefined interpretation when
applied to types in HO-CASL).

Bernd, Till, et al.: please correct me if there are problems with the
above. 

> - Is the operator {{ __ }} allowed, since in an application like
>   {{ ( a ) }}, from a grammatical point of view we have different IDs
>   "{{" and "}}" and the reference manual aks each ID to have balanced
>   occurrences of {.. } (or [... ]).

I don't understand your "grammatical" point of view: "{{" and "}}" are
simply separate TOKENs, and *not* valid as complete IDs.  The ID 
"{{ __ }}" is allowed, and since it is balanced wrt "{" and "}", so is
any TERM (or FORMULA) built from it.

> - I have doubts about the possibility of allowing [ and ] in IDs since
>   the symbols are also used for marking compound ids.

I had hoped that e.g. "[ __ ]" and "__ [ __ ]" would be a valid IDs,
but that may well lead to problems when trying to group a list of IDs
into a TERM.  E.g., whether "f[elem]" is a constant compound ID or
mixfix notation for "__[__](f,elem)" cannot be determined
context-freely.  

However, a solution there may be for context-free parsers to leave the
recognition of compound ids to the static analysis.  After all,
"f[elem]" is only legal as a compound id when it has been declared as
such (possibly by the renaming that is implicit in the instantiation
of a generic spec); in specs not using compound ids at all, e.g.,
those arising from translation of OBJ3 specs, it would be annoying to
have unnecessary restrictions on mixfix symbols.  

In a CASL sublanguage not allowing mixfix notation, however, terms
should be fully parsed, context-freely, including compound ids.  Maybe
a parser annotation could be provided, to declare whether mixfix
notation is to be used in a spec or not.

I hope it doesn't cause more confusion than it manages to resolve!
Unfortunately, I won't be able to react to any questions about the
above (or anything else) until I return to the net at the end of
September...

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

Computer Science Laboratory     mailto:mosses@csl.sri.com
SRI International               phone: +1 (650)  859-5067
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
    affiliated also to CS Department, Stanford University
_________________________________________________________