Maude-help mailing list

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

Hi Marko, and Bartosz,

Thanks, Bartosz, for your answer. However, I believe the problem is somewhere 
else. One can use messages in any way one finds convenient. Marko was not 
trying to transform messages into Objects. One can have a hierarchy of 
messages Limit-Order < Order < Msg, no problem about that. I'm not going into 
whether it makes sense or not to have such hierarchy, or whether any of you 
had objects in mind. As I understand the spec was trying to keep them as 
messages. 

It is just a syntactic problem. Due to a wrong specification. Full Maude is 
not very good at providing error messages, something that must be improved. 
But the issue here is hidden by the fact that there are error messages than 
do not show up until some term is parsed. In your spec everything is parsed 
in a first shot (no eqs, no rls, no id elements, ...), and the module is not 
used for parsing until the red command is entered. Therefore, the error 
message is not about the term to be reduced, but actually, in this case, for 
the above reason, about the spec itself. Specifically, the sort Float is used 
without importing FLOAT. 

You can find the modified modules below. 

Cheers, 

Paco


(omod TRADE-ORDER is
    protecting STRING .
    protecting NAT .
    sorts Order Symbol CustomerId .
    subsort Order < Msg .
    subsorts String < Symbol CustomerId .
    msg buy_of_for_ : Nat Symbol CustomerId -> Order .
    msg sell_of_for_ : Nat Symbol CustomerId -> Order .
endom)

(omod LIMIT-ORDER is
    protecting TRADE-ORDER .
    pr FLOAT .
    sort Limit-Order .
    subsort Limit-Order < Order .
    msg _at_ : Order Float -> Limit-Order .
endom)

(red in LIMIT-ORDER : buy 5 of "T" for "C" at 1.2 .)

> On 9 Jun 2021, at 18:07, Bartosz Zieliński 
> <bartosz.zielinski AT uni.lodz.pl>
>  wrote:
> 
> I believe this is a slight misunderstanding of how objects are supposed to 
> work in Maude.
> Messages to not return objects (you really shouldn't do the subsort 
> Order < Msg since messeges and objects are instances of common sort 
> configuration.
> Also Order should not be a sort but a class. To have objects you have to 
> declare class and then you can construct objects with syntax < Oid : Class 
> | Attributes >. Messages and objects are put in the commutative associative 
> soup constructed with __  and you have rewrite rules which take 
> messages and objects and return other messages and objects. Incidentally, 
> Full Maude assumes that the first argument of the message is an Oid (object 
> id). So a rule like 
> 
> rl < X : Counter | val : Y > inc(X) => < X : Counter | val : Y + 1 > .
> 
> defines a message (method) of the Counter class which increases value of 
> the attribute val of objects of this class, object identifiers correlate 
> concrete objects identified with Oid's (like references in Java) with 
> messages.
> 
> So the whole code below (including TRADE-ORDER) makes no sense.
> I would rewrite TRADE-ORDER as (I did not test it) as
> 
> (omod TRADE-ORDER is
>     protecting STRING .
>     protecting NAT .
>     protecting QID.
>     sorts Symbol CustomerId .
>     subsort Qid < Oid .
>     class Order | amount : Int, product: Symbol, customer: CustomerId .
> endom)
> 
> and then you have order objects like < 'A : Order | amount : 10, product : 
> ...... >.
> 
> Best regards 
> 
> Bartosz Zielinski
> 
> 
> 
> Od: Marko Schuetz-Schmuck
> Wysłano: Środa, 09 Czerwiec 2021 17:24
> Do: 
> maude-help AT lists.cs.illinois.edu
> Temat: [[maude-help] ] extending message "format"
> 
> Dear All,
> 
> I'm still very new to Maude. I ran into something that has me
> puzzled. Say I define the module TRADE-ORDER: 
> 
> (omod TRADE-ORDER is
>     protecting STRING .
>     protecting NAT .
>     sorts Order Symbol CustomerId .
>     subsort Order < Msg .
>     subsorts String < Symbol CustomerId .
>     msg buy_of_for_ : Nat Symbol CustomerId -> Order .
>     msg sell_of_for_ : Nat Symbol CustomerId -> Order .
> endom)
> 
> and based on that I want to define a LIMIT-ORDER which is just a
> TRADE-ORDER with a limit (of course I didn't want to duplicate the parts
> of the message that are already in TRADE-ORDER). So I tried the
> following (which would have some drawbacks even if it would work,
> e.g. multiple nested "at"s):
> 
> (omod LIMIT-ORDER is
>     protecting TRADE-ORDER .
>     sort Limit-Order .
>     subsort Limit-Order < Order .
>     msg _at_ : Order Float -> Limit-Order .
> endom)
> 
> I was expecting to be able to write
> 
> (red in LIMIT-ORDER : buy 5 of "T" for "C" at 1.2 .)
> 
> but that results in "incorrect command". I have since changed this to
> objects and classes, but the syntax is not as plain as it would be with
> the above.
> 
> Best regards,
> 
> Marko