Maude-help mailing list

[Marc Boyer <Marc.Boyer AT onera.fr>]

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