Maude-help mailing list

[Matthias Radestock <matthias AT sorted.org>]

I have come across a problem where changing an operator declaration from
total to partial causes Full Maude mode to behave weirdly.

The example is as follows:

(fmod PAIR{X :: TRIV, Y :: TRIV} is
    sort Pair{X, Y} .
    op <_;_> : X$Elt Y$Elt -> Pair{X, Y} .
    op 1st : Pair{X, Y} -> X$Elt .
    op 2nd : Pair{X, Y} -> Y$Elt .
    var A : X$Elt .
    var B : Y$Elt .
    eq 1st(< A ; B >) = A .
    eq 2nd(< A ; B >) = B .
endfm)

(view Pair{X :: TRIV, Y :: TRIV} from TRIV to PAIR{X,Y} is
    sort Elt to Pair{X,Y} .
endv)

(fmod ZIP{X :: TRIV, Y :: TRIV} is
    pr LIST{X} .
    pr LIST{Y} .
    pr PAIR{X,Y} .
    pr LIST{Pair{X,Y}} .

    op zip : List{X} List{Y} -> List{Pair{X,Y}} .

    var EX : X$Elt .
    var EY : Y$Elt .
    var LX : List{X} .
    var LY : List{Y} .

    eq zip(nil,nil) = nil .
    eq zip(EX LX, EY LY) = < EX ; EY > zip(LX, LY) .

endfm)

(fmod INT-BOOL-ZIP is
   pr ZIP{Int,Bool} .
endfm)

(rew zip(1 2 3, true false true) .)
(rew zip(1 2 3 4, true false true) .)

Loading the above into Full Maude produces 
    < 1 ; true > < 2 ; false > < 3 ; true >
and
    < 1 ; true > < 2 ; false > < 3 ; true > zip(4,nil)
for the two rewrites at the end, as expected.

However, if I change the operator declaration of zip to be partial
(i.e. use ~> instead of ->), then the rewrites produces no result - I
just get
  rewrites: 0 in 10ms cpu (10ms real) (0 rewrites/second)
  rewrites: 0 in 11ms cpu (11ms real) (0 rewrites/second)

Observing the output more closely, I discovered that Maude is no longer
printing the "Introduced module INT-BOOL-ZIP" message that it was
producing on the first run. So it looks like that evaluating the ZIP
module with the ~> zip declaration somehow breaks the INT-BOOL-ZIP
module declaration.


What am I doing wrong?


Matthias