Maude-help mailing list

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

The polymorphic operator feature is very limited - it only exists so 
that built-in operators can be handled in a generic way by the metalevel.

The implementation works by adding an instance of operator syntax for 
each kind to the grammar and then instantiating the operator template on 
a kind when a given instance is parsed. Obviously if an operator could 
take different kinds for each of its polymorphic arguments then this 
approach would be horribly inefficient.

There are other ways of implementing polymorphism with mixfix syntax but 
the current approach works well enough for the very limited application 
for which it was intended.

Steven

On 2/3/12 9:18 AM, Lucian Bentea wrote:
>   Hi everyone,
>
>   I would have a question related to how Maude parses polymorphic binary
>   operators. Consider the following example:
>
>   sorts S S' Mapping .
>
>   ops a b : ->  S [ctor] .
>   ops x y : ->  S' [ctor] .
>
>   op _->_ : Universal Universal ->  Mapping [poly (1 2)] .
>
>   I would like to use the binary operator ->  to represent the mapping of
>   elements of some arbitrary sort, to elements of another _possibly
>   different_ arbitrary sort.
>
>   The expressions "a ->  b" and "x ->  y" are both parsed without any
>   errors. However, if I try to reduce "a ->  x", I get the error: didn't
>   expect token x: a ->  x<---*HERE*
>
>   My question is: does Maude first check that both arguments "a" and "x"
>   are of the same sort before reducing "a ->  x"? If this is the case, is
>   there an easy way to define in Maude a polymorphic operator ->  which can
>   take arguments of arbitrary, but different sorts?
>
>   Best regards,
>   Lucian Bentea
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help