Maude-help mailing list

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

Maude only supports simple sorts, not union sorts or in your case 
intersection sorts. At one point we had union sorts and we have 
discussed intersection sorts but they are a performance bottle neck - if 
you want them you must add them manually:

sort X-and-Y .
subsort X-and-Y < X Y .
mb a | a : X-and-Y .

Memberships compute a least sort, but a term has multiple least sorts, 
which one you get is unpredictable, but reproducible.

Steven

On 9/3/13 6:20 AM, Tony Garnock-Jones wrote:
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Hi all,
>
> I'm afraid I've run into what must be an obvious problem, but that
> does seem to be discussed anywhere I can find.
>
> In https://gist.github.com/tonyg/6419046, I've defined the following:
>
> fmod T is
>      var XX : X .
>      var YY : Y .
>      var TT : Thing .
>
>      sort Thing .
>      op a : ->  Thing [ctor] .
>      op b : ->  Thing [ctor] .
>      op _|_ : Thing Thing ->  Thing [ctor] .
>
>      sort X .
>      subsort X<  Thing .
>      mb a | TT : X .
>
>      sort Y .
>      subsort Y<  Thing .
>      mb TT | a : Y .
> endfm
>
> The problem is that Maude is willing to classify the term
>
>      a | a
>
> as a Y, but *not* as an X, despite it clearly meeting the membership
> criterion. See, for example, the outputs of
>
> match [5] XX<=? a | a . *** expected: solution. got: nothing.  BAD
> match [5] YY<=? a | a . *** expected: solution. got: solution. OK
>
> Worse, if I comment out anything mentioning Y, then suddenly X starts
> to behave as expected.
>
> Sorry if this is a FAQ; I hope there's an answer somewhere out there :-)
>
> Regards,
>    Tony
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.11 (Darwin)
> Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/
>
> iQIcBAEBAgAGBQJSJeIBAAoJEGFBh8TOtT4M9sQQAIx45W0uCCPgGSfn16NOpw5m
> EKVVtKLTOa56w9rmcRQs6LH+mW7oEmTE+u29c3qV9VI9RcrM9RM8hIqnr+qtluT4
> sR738Xh1KHz8h5lieJQsnlJ/ysaAxMMazvo3UsuQRTmbIyIcle1VPfpkejmG5Uxt
> a+9tv0D3hQDPcDaryeQUtLSqkyaXBUGmW9q3nz5LeDaFyxUoaCgjT+1OwD/gIX1z
> 2ukJIsLv0rAsCebydm/glG0+9Dvex4y7xU7TxxJ4coTfpTN/czRHJwoSi8AL7/OQ
> zobMKQecNA1xSBrIPJ6HeaeJSKQNGDgDO84EylBTEAh1V7PWc6/lQpo6/XMB3MV6
> PVSfrxFX2Q7ZRCE3Yg0+DgKL48D5t6sSWc57qnzMlOr1Empq5FOLc1KFGniVM0lH
> PNbTKW6QAOyqYElDOCn8lIY1RwzY5vLf6z4HCWm70R7IcbvZT5fcO+towSj0CmXL
> irvC12WuTp1O599gGyPb2T+kWKLO66jJXHyZezo0Ku9rayQIPFYjebDPAQUX4YCx
> xHGzYoBWajs+cT/ScNf/44P6SfAgEtnaUv5FoX9Vzkl2eh25XuNfjKHowqS/lZaw
> T/xtsCiLFa0wBsfsPwjxV1AfrDbf0PAJst2aBzLWm0O71dV7HHYP2iz3QTnHuoC3
> ooTF4NOsfiXtuG6kaNft
> =Jvc8
> -----END PGP SIGNATURE-----
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help