Maude-help mailing list

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

That's not a bug, it's a feature!

You can check how your equations are parsed with the commands:

set print with parens on .
show eqs .

And sure enough:

  ceq (f(x,y,r)) = r if (x >= y) = true /\ (x =/= 0) = true /\ (x <= r) = 
true .

vs

  ceq (f(x,y,r)) = r if ((x >= (x /\ y)) =/= ((0.0 /\ x) <= r)) = true .

The difference arises because Rat belongs to the Nat hierarchy which
has _>=_ operator declared in the prelude:

  op _>=_ : Nat Nat -> Bool [prec 37 ...] .

vs

  op _>=_ : Float Float -> Bool [prec 51 ...] .

for Float. The reasons are historic; many of the conventions are taken
from OBJ3 so that early versions of Maude could run OBJ3 programs for
comparison.

You can see the default attributes given to your operators with the 
command:

show ops .

Here the _/\_ gets a precedence that falls between 37 and 51, explaining
different parsing:

  op _/\_ : Rat Rat -> Rat [assoc comm prec 41 gather (e E)] .

So what you need to do is the give _/\_ a prec smaller than 37 or
greater than 51 depending on which parsing you prefer.

Steven

On Friday 09 July 2010 10:24:39 am Marc Boyer wrote:
> Dear all,
> 
> I have a strange behavior of the parsing. Here is a minimal example.
> All comes from the overloading of /\ (not a good idea in Maude,
> but in my domain, /\ denote minimum).
> 
> fmod BUG is
> protecting RAT .
> 
> op _ /\ _ : Rat Rat -> Rat [assoc comm] .
> vars a b : Rat .
> ceq a /\ b = a if a <= b .
> 
> vars x y r : Rat .
> op   f( _ , _ , _ ) : Rat Rat Rat -> Rat .
> ceq  f( x , y , r ) = r
> if  x >= y /\ x =/= 0  /\  x <= r  .
> eq   f( x , y , r ) = -1 [owise] .
> endfm
> 
> red f( 1 , 0 , 5 ) .
> 
> The conditional equation is parsed as
> (x >= y) /\ (x =/= 0)  /\  (x <= r)
> and the test term reduces into 1.
> 
> But when using the same module with Float instead of Rat, the
> conditional equation is parsed as
> ( x >= (y /\ x) ) =/= ( (0  /\  x ) <= r )
> and the test term redudes into -1.0
> 
> fmod BUG is
> protecting FLOAT .
> 
> op _ /\ _ : Float Float -> Float [assoc comm] .
> vars a b : Float .
> ceq a /\ b = a if a <= b .
> 
> vars x y r : Float .
> op   f( _ , _ , _ ) : Float Float Float -> Float .
> ceq  f( x , y , r ) = r
> if  x >= y /\ x =/= 0.0  /\  x <= r  .
> eq   f( x , y , r ) = -1.0 [owise] .
> 
> endfm
> 
> red f( 1.0 , 0.0 , 5.0 ) .
> 
> And there is no warning at all...
> 
> Regards,
> Marc Boyer
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>