Maude-help mailing list

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

Dear Francisco,

thanks for the rich response. It gives me lots to process!

Best regards,

Marko

Paco Durán 
<duran AT lcc.uma.es>
 writes:

> 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 
> (http://maude.lcc.uma.es/maude31-manual-html/maude-manualch22.html#x117-32500022.8),
>  or even the object-based chapter 
> (http://maude.lcc.uma.es/maude31-manual-html/maude-manualch8.html#x57-1280008),
>  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
>

-- 
Prof. Dr. Marko Schütz-Schmuck
Department of Computer Science and Engineering
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681

Attachment: signature.asc
Description: PGP signature