:mand infinite loop
Issue #2
resolved
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 NATSETPRED {pr(SET(NAT)*{sort Set > NatSet})
pred p1 : Nat Nat NatSet Nat Nat NatSet .
op q1 : NatSet NatSet > Bool .
eq [:mand]: q1 ( ( N1:Nat N2:Nat NS:NatSet ) , ( N3:Nat N4:Nat NS2:NatSet ) )
= p1(N1,N2,NS,N3,N4,NS2) .
}
open NATSETPRED .
red q1( ( 1 2 3 ) , ( 4 5 6 ) ) .
Running this through cafeobj I get the proper expansion, but then it hangs, CPU at 100%:
:mand[=>] (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: interruptsignal]
All the best
Norbert
Comments (2)

repo owner 
reporter  changed status to resolved
I confirm that the current implementation from git solves this problem. Thus, I close this issue.
 Log in to comment
Thanks for the report.
I think this is not a bug, but is a problem of the performance of ACrewriting, 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 andalso p2 andalso ... andalso pn' . If so, this will not cause the size problem because 'andalso' 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