Problems and questions about CASL concrete syntax

[Axel Schairer <schairer@dai.ed.ac.uk>]

Dear Peter, 

Thanks for clarifying most of my questions.  Below is one question I
still don't see the answer to and a further very specific technical
issue concerning `?' as a complete token.

----------------------------------------------------------------------
Axel Schairer writes:
> > - There seems to me to be a problem with the definition of symbol
> > items: Should
> > 
> > 	{ ... } hide zero: nat
> > 
> > hide the unary predicate zero on naturals or the nullary function
> > (constant) zero of sort nat?  I think the concrete grammar allows
> > both.

Peter Mosses writes:
> The ambiguity here is supposed to be resolved by a later phase.
> Unfortunately that may involve transforming an OP-TYPE into a
> PRED-TYPE, but this is not the only situation where a transformation
> is required (e.g., MIXFIX to TERM).

> Could you persuade bison to prefer one parse to the other?  If not, we
> may have to reconsider a previously-rejected proposal to use the same
> syntax for qualified symbols in such lists of symbols as in terms,

I can persuade my tools to prefer one or the other, so the concrete
syntax and the intermediate representation are not the real issues.
The issue is that I would not know how to postprocess the intermediate
AST correctly.  Three possibilities I have come across so far are:

	1) the example is incorrect as it is ambiguous; it should
	   either be `op zero: nat' or `pred zero: nat'.  However
	   `... hide op f, g, zero: nat' would also be OK since the
	   op's scope extends over the `zero' item.

	2) the example is OK if there is either a predicate or a
	   constant but not both for zero, and the one that exists is
	   hidden  in the result

	3) the example is OK if there is a predicate or a constant or
	   both for zero, and both are hidden in the result

----------------------------------------------------------------------

  Axel Schairer writes:
> > - The Summary (on C-10) says that `<', `*', `?', and `!' should be
> > recognized as complete tokens.  So there is a rule saying that
> > 	TOKEN ::= ... | `<' | `*' | ... 

Peter Mosses writes:
> I'm afraid that this complication arising from the double usage of
> symbols such as `<' is something we have to accept.

I appreciate this, it just took me some time to figure out how to
handle it.  I would only like to point to one specific technical
consequence concerning the token `?' and deterministic parsers with
one symbol lookahead:

Since `?' and `*' are both accepted as a token, and a sort name can be
expanded to a token, `?' and `*' are both valid sort names.  Now

	op f: ?		is a constant of sort `?'
	op f: ? *	is a `partial constant' of sort `*'
	op f: ? * s ...	is an operation from `?' * `s' * ... -> ...

This means that whether the `?' should be reduced to a TOKEN (and then
to a TOKEN-ID and then a SORT as in the first and third example but
not the second) cannot be decided by looking at the next token in
general: If the next token is a `*' and the `*' is followed by
something that starts a SORT then the `?'  reduces to a TOKEN,
otherwise it is the terminal introducing a partial nullary operation.

This might be solvable (with one symbol lookahead) by heavily
rewriting the grammar, but when I tried to do this I soon lost the
overview whether the resulting grammar would accept the same terminal
strings as the original one because the number of productions simply
exploded.  I think this is what Frederic experienced as well:
 
Frederic Voisin writes:
> I'm afraid that Axel will have a much larger list of productions
> that he probably expect.

If I remove the rule TOKEN --> "?" from my grammar, everything is
fine, except of course that now `?' is no longer a token.
Incidentally removing TOKEN --> "*" removes the conflict as well, but
then `*' is no longer a token and somehow this seems to be even worse.

I suppose this is only a problem if one is dedicated to deterministic
parsing with only one symbol lookahead. 

----------------------------------------------------------------------

Best regards,

Axel