Maude-help mailing list

[Lucian Bentea <lucianb AT ifi.uio.no>]

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