[Maude-help] Checking sorts of arguments of polymorphic binary operators
lucianb at ifi.uio.no
Fri Feb 3 11:18:38 CST 2012
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?
More information about the Maude-help