Maude-help mailing list

[Paco Durán <duran AT lcc.uma.es>]

Hi Marko, 

You are confusing Attribute and attribute names. Your declaration subsort 
Slot < Attribute does not help. 

I'm afraid that to do that you're going to have to used the equivalent system 
representation. You can see Section 22.8 of the manual for further 
explanations 
(https://urldefense.com/v3/__http://maude.lcc.uma.es/maude31-manual-html/maude-manualch22.html*x117-32500022.8__;Iw!!DZ3fjg!qo07G6pFZf_dKs0FyOo-h4FMCXN9S0o-2piSeuGTyHdrjPd5xoklclxhdpo5KTtC65iDVdbCWAqG$
 ), or even the object-based chapter 
(https://urldefense.com/v3/__http://maude.lcc.uma.es/maude31-manual-html/maude-manualch8.html*x57-1280008__;Iw!!DZ3fjg!qo07G6pFZf_dKs0FyOo-h4FMCXN9S0o-2piSeuGTyHdrjPd5xoklclxhdpo5KTtC65iDVbs-h8KA$
 ), but basically, OO modules are just syntactic sugar that is internally 
transformed into system modules. By using the corresponding object notation 
you could introduce your own syntax for attributes. 

Best,

Francisco

mod TEST1 is
   inc CONFIGURATION .
   protecting NAT .
   sort Slot .
   ops one two three : -> Slot [ctor] .
   ---- class Pool | one : Nat, two : Nat, three : Nat .
   sort Pool .
   subsort Pool < Cid .
   op Pool : -> Pool .
   op _:_ : Slot Nat -> Attribute [ctor prec 15 gather (e &)] .
   ---- class Item | kind : Slot .
   sort Item .
   subsort Item < Cid .
   op Item : -> Item .
   op kind`:_ : Slot -> Attribute [ctor gather (&)] .
   ---- msg add : Oid Oid -> Msg . *** Item Pool
   op add : Oid Oid -> Msg .
   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 > .
endm

rew < I:Oid : Item | kind : one > < P:Oid : Pool | one : 5 > add(I:Oid, 
P:Oid) .
---- rewrite in TEST1 : (add(I, P) < P : Pool | one : 5 >) < I : Item | kind 
: one > .
---- rewrites: 2 in 0ms cpu (1ms real) (13157 rewrites/second)
---- result Object: < P : Pool | one : 6 >


> On 8 Jul 2021, at 16:59, Marko Schuetz-Schmuck 
> <MarkoSchuetz AT web.de>
>  wrote:
> 
> 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