Maude-help mailing list

[Marko Schuetz-Schmuck <MarkoSchuetz AT web.de>]

Dear All,

say I have a sort with constructors one, two, and three. I also have a
class with attributes one, two, and three. Now I would like to use the
constructors to match attributes. For example, 

load full-maude
(omod TEST0 is
    protecting NAT .
    sort Slot .
    ops one two three : -> Slot [ctor] .
    class Pool | one : Nat, two : Nat, three : Nat .
    class Item | kind : Slot .
    msg add : Oid Oid -> Msg . *** Item Pool
    vars I P : Oid .
    var N : Nat .
    rl [doAddone] :
        < I : Item | kind : one >
        < P : Pool | one : N >
        add(I, P)
      => < P : Pool | one : N + 1 > .
    rl [doAddtwo] :
        < I : Item | kind : two >
        < P : Pool | two : N >
        add(I, P)
      => < P : Pool | two : N + 1 > .
    rl [doAddthree] :
        < I : Item | kind : three >
        < P : Pool | three : N >
        add(I, P)
      => < P : Pool | three : N + 1 > .
endom)

I would like to fold the three rules into one:

(omod TEST1 is
    protecting NAT .
    sort Slot .
    subsort Slot < Attribute .
    ops one two three : -> Slot [ctor] .
    class Pool | one : Nat, two : Nat, three : Nat .
    class Item | kind : Slot .
    msg add : Oid Oid -> Msg . *** Item Pool
    vars I P : Oid .
    var N : Nat .
    var S : Slot .
    rl [doAdd] :
        < I : Item | kind : S >
        < P : Pool | S : N >
        add(I, P)
      => < P : Pool | S : N + 1 > .
endom)

but this does not parse. What am I missing?

Thanks and best regards,

Marko

Attachment: signature.asc
Description: PGP signature