Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

You can't get the result you are looking for, for a couple of reasons:
(1) Maude's design is that built-in semantics override default semantics, and only defer to default semantics if the built-in semantics can't do a reduction. This is baked in to the implementation as C++ class inheritance.
(2) Even if it were possible to given priority to user semantics for built-in operators, in your example 1 + 2 is a proper subterm that is evaluated eagerly before your rule equations for _-_ are considered.

Steven

On 3/11/13 1:02 PM, Yiming Li wrote: Dear Maude-Help,

    I have a question about operations. As follows, there are some arithmetic operations and when I load them(ZZ.maude) into maude, I use "red -(1+2)" to test with setting trace on. In my mind, it should be "-1 + -2" and then "-3". However, it is "3" firstly and then "-3" using building-in function. Do we have any other way to define user's function overriding building-in ones.

    Thanks.

========================================================================

fmod ZZ is protecting INT . *** using Maude's built-in integers vars I J K L : Int . *** properties of arithmetic operations eq 0 + I = I . eq I + - I = 0 . eq -(I + J) = - I + - J . eq I - J = I + (- J) . eq 0 * I = 0 . eq - I * J = -(I * J) . eq I * (J + K) = I * J + I * K . eq (I + J) * K = I * K + J * K . cq I * J = (I - 1)* J + J if I > 0 .

endfm

=================================================================

--
Best regards,
Yiming (Nathan)
-----------------------------------------------------------------------------------------------------
Department of Computer Science
University of Liverpool

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help