maude-help AT lists.cs.illinois.edu
Subject: Maude-help mailing list
List archive
- From: Tony Garnock-Jones <tonyg AT ccs.neu.edu>
- To: maude-help AT cs.uiuc.edu
- Subject: [Maude-help] Subsorts that... overlap? aren't working how I expect
- Date: Tue, 03 Sep 2013 09:20:01 -0400
- List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help/>
- List-id: <maude-help.cs.uiuc.edu>
-----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] Subsorts that... overlap? aren't working how I expect, Tony Garnock-Jones, 09/03/2013
- Re: [Maude-help] Subsorts that... overlap? aren't working how I expect, Steven Eker, 09/03/2013
- Re: [Maude-help] Subsorts that... overlap? aren't working how I expect, Tony Garnock-Jones, 09/03/2013
- Re: [Maude-help] Subsorts that... overlap? aren't working how I expect, Steven Eker, 09/03/2013
Archive powered by MHonArc 2.6.16.