Re: [CoFI] Ambiguity in CASL concrete syntax

[Frederic.Voisin@lri.fr (Frederic Voisin)]

Dear all,

There is still some kind of ambiguity in the concrete syntax of CASL
due to the fact that in some contexts a symbol can refer either to a
sort name or to a constant name (this kind of overloading is not
forbidden) and we do not have the syntax to let the user makes the
difference.  For instance this happen in mappings and more generally
in morphisms (renaming, hiding...)

[In fact the CASL abstract syntax (and the semantics) need to
distinguish between sorts, function symbols, and predicate symbols,
so the current concrete syntax is definitely inadequate here.  --PDM]

Consider the following example, somewhat pathological, but not forbidden

{.... sort S; op S : T ....} renaming S into V

In that case we do not know what kind of renaming is intended: sort ?
operation ?  What means do we offer to disambiguate the renaming (or
do we force the user to change the spec ???) ?

When the renaming of the operation was intended, the user can use
the alternative syntax provided by QUAL-OP-NAME -- i.e. something like
"renaming (op S : T) into V " that is currently in the syntax. But if
the sort renaming was intended, no such means exists...

Maybe we should ALLOW in such morphisms "sort ID" (or a list thereof)
in addition of ID to solve this problem.

One can even be more strict and always INSISTS on having it (that was
part of an early version of Paris'proposal !). 

Any reaction ??

frederic

[Perhaps one could then be more uniform with the concrete syntax of
 declarations, always using keywords to introduce "sections", e.g.:
   SP renaming sorts s1|-> s1',...,sn |-> sn', 
               ops   o |-> o',..., 
               preds p |-> p',...
 and similarly in the case of restrictions.  After all, it would only
 cost up to 3 keywords each time, and may have methodological advantages.
--PDM]

Orthogonal remark: currently QUAL-OP-NAME and QUAL-PRED-NAME insist on having
the profile of an operation/predicate. I can imagine of the use of such syntax
when going from a mixfix syntax to a functional syntax in case when
no ambiguity occur w.r.t. the profile. e.g. (op __+__) (a, b) and I see
no reason for having to give the profile. Shouldn't we allow the
profile to be omitted (in this does not raise parsing problems) ?

[Currently, we allow __+__(a,b) in the case that the profile is
omitted.  It seems that Frederic is proposing to replace this by
(op __+__) (a, b)  --PDM]