Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi,

The reason that ad hoc overloading is not allowed between operators
with the same arity kinds but different coarity kinds is precisely in
order to ensure unique, unambiguous meta-term representations -
otherwise meta-programming becomes very painful because when
constructing a new meta-term you would have to ensure there was
enought context for disambiguation.

The current release version of Maude quietly allows you to break this
rule at the object level because there is a full context free parser,
and any ambiguities are discovered and reported. This has caused much
confusion with users wondering while code that was accepted at the
object level fails at the metalevel so future releases will complain
about illegal overloading - the next version of Core Maude is actually
ready but is being held up until the use of illegal overloading is
removed from Full Maude.

You might think that subsort information should be used to
disambiguate your first example, but in fact it is important that
terms such as 1 / X:Rat which can only be sorted at the kind level are
parsed by the context free parser, so context free parsing is done on
kinds rather than sorts.

The are a number of problems with getting Maude to parse the concrete
syntax of another language. I don't have any good solutions; some
people use preprocessing scripts. In your example, I would be inclined
to put Fun and Token in different classes.

Ultimately we plan to have something like ASF+SDF's parsing but
integrating this nicely with Maude features, especially the metalevel,
is challenging.

Best regards,

Steven Eker