:m-and infinite loop

[Norbert Preining]

The following code send cafeobj (compiled from current git) into an infinite loop after outputting the expansion:

mod! SET(X :: TRIV) {
[Elt.X < Set]
op empty : -> Set {constr} .
op (_ _) : Set Set -> Set {constr assoc comm id: empty} .
eq E:Elt E = E .
}
mod NAT-SET-PRED {pr(SET(NAT)*{sort Set -> NatSet})
pred p1 : Nat Nat NatSet Nat Nat NatSet .
op q1 : NatSet NatSet -> Bool .
eq [:m-and]: q1 ( ( N1:Nat N2:Nat NS:NatSet ) , ( N3:Nat N4:Nat NS2:NatSet ) ) 
                  = p1(N1,N2,NS,N3,N4,NS2) .
}
open NAT-SET-PRED .
red q1( ( 1 2 3 ) , ( 4 5 6 ) ) .

Running this through cafeobj I get the proper expansion, but then it hangs, CPU at 100%:

:m-and[=>] (p1(3,2,1,6,5,4) and (p1(3,2,1,5,6,4) and (p1(3,2,1,6,4,5) and (p1(3,2,1,5,4,6) and (p1(3,2,1,4,6,5) and (p1(3,2,1,4,5,6) and (p1(2,3,1,6,5,4) and (p1(2,3,1,5,6,4) and (p1(2,3,1,6,4,5) and (p1(2,3,1,5,4,6) and (p1(2,3,1,4,6,5) and (p1(2,3,1,4,5,6) and (p1(3,1,2,6,5,4) and (p1(3,1,2,5,6,4) and (p1(3,1,2,6,4,5) and (p1(3,1,2,5,4,6) and (p1(3,1,2,4,6,5) and (p1(3,1,2,4,5,6) and (p1(2,1,3,6,5,4) and (p1(2,1,3,5,6,4) and (p1(2,1,3,6,4,5) and (p1(2,1,3,5,4,6) and (p1(2,1,3,4,6,5) and (p1(2,1,3,4,5,6) and (p1(1,3,2,6,5,4) and (p1(1,3,2,5,6,4) and (p1(1,3,2,6,4,5) and (p1(1,3,2,5,4,6) and (p1(1,3,2,4,6,5) and (p1(1,3,2,4,5,6) and (p1(1,2,3,6,5,4) and (p1(1,2,3,5,6,4) and (p1(1,2,3,6,4,5) and (p1(1,2,3,5,4,6) and (p1(1,2,3,4,6,5) and p1(1,2,3,4,5,6)))))))))))))))))))))))))))))))))))):Bool^C
Error: Received signal number 2 (Interrupt)
  [condition type: interrupt-signal]

All the best

Norbert

[Toshimi Sawada]

Thanks for the report.

I think this is not a bug, but is a problem of the performance of AC-rewriting, i.e., the size of 'p1 and p2 and ... and pn' exceeds the ability of the current system.

I think for expansion purpose, 'p1 and p2 and ... and pn' can be rephrased by 'p1 and-also p2 and-also ... and-also pn' . If so, this will not cause the size problem because 'and-also' is an operator without any equational theory, it simply evaluates its argument from left to right.

I will prepare this version soon and inform you.

Best

Toshimi Sawada

[Norbert Preining]

I confirm that the current implementation from git solves this problem. Thus, I close this issue.