next(0,(A,N):T,A,T,N) :- !.
next(M,A:T1,A,T1,N) :- !, M > 0, N is M - 1.
next(M,T1+_,A,T2,N) :- next(M,T1,A,T2,N). 
next(M,_+T1,A,T2,N) :- !,next(M,T1,A,T2,N).
next(N,T1|T2,A,T3|T2,M) :- next(N,T1,A,T3,M). 
next(N,T1|T2,A,T1|T3,M) :- next(N,T2,A,T3,M).
next(N,T1|T2,A,T3|T4,P) :- next(N,T1,A,T3,M), M > 0, next(M,T2,A,T4,P). 
next(N,T1|T2,A,T4|T3,P) :- !,next(N,T2,A,T3,M), M > 0, next(M,T1,A,T4,P). 
next(M,T1*T2,A,T3*T2,N) :- next(M,T1,A,T3,N).
next(M,T1*T2,A,T3,N) :- !,maybe_empty(T1), next(M,T2,A,T3,N).

maybe_empty(lambda) :- !.
maybe_empty(T1+T2) :- (maybe_empty(T1),!;maybe_empty(T2)).
maybe_empty(T1|T2) :- !,maybe_empty(T1),maybe_empty(T2).
maybe_empty(T1*T2) :- !,maybe_empty(T1),maybe_empty(T2).

not_empty(_:_).
not_empty(T1+T2) :- !,not_empty(T1),not_empty(T2).
not_empty(T1|T2) :- (not_empty(T1),!;not_empty(T2)).
not_empty(T1*T2) :- (not_empty(T1),!;not_empty(T2)).

accept(T1,[A|L]) :- next(0,T1,A,T2,0),accept(T2,L).
accept(T,[]) :- maybe_empty(T).

accept(_,T,[*]) :- maybe_empty(T).
accept(0,T,[]) :- !,not_empty(T).
accept(N,T1,[A|L]) :- next(0,T1,A,T2,0), M is N - 1,accept(M,T2,L).

%testFinAltBit(N) :- open('altBit2.txt',write,Str),M1M2=lambda+(m1:(lambda+(m2:(lambda+M1M2)))),M1A1=lambda+((m1,1):(lambda+((a1,0):(lambda+M1A1)))),M2A2=lambda+((m2,1):(lambda+((a2,0):(lambda+M2A2)))),T=(M1M2|M1A1|M2A2),length(IL,N),setof(IL,accept(T,IL),OL),write(OL),print_list(Str,OL),close(Str).

testAltBit(N) :- open('altBit2.txt',write,Str),M1M2=m1:m2:M1M2,M1A1=(m1,1):(a1,0):M1A1,M2A2=(m2,1):(a2,0):M2A2,T=(M1M2|M1A1|M2A2),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

%testFinAltBit3(N) :- open('altBit3.txt',write,Str),M1M2M3=lambda+(m1:(lambda+(m2:(lambda+(m3:(lambda+M1M2M3)))))),M1A1=lambda+((m1,1):(lambda+((a1,0):(lambda+M1A1)))),M2A2=lambda+((m2,1):(lambda+((a2,0):(lambda+M2A2)))),M3A3=lambda+((m3,1):(lambda+((a3,0):(lambda+M3A3)))),T=((M1M2M3|M1A1)|(M2A2|M3A3)),length(IL,N),setof(IL,accept(T,IL),OL),write(OL),print_list(Str,OL),close(Str).

testAltBit3(N) :- open('altBit3.txt',write,Str),M1M2M3=m1:m2:m3:M1M2M3,M1A1=(m1,1):(a1,0):M1A1,M2A2=(m2,1):(a2,0):M2A2,M3A3=(m3,1):(a3,0):M3A3,T=((M1M2M3|M1A1)|(M2A2|M3A3)),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

testAltBit3bis(N) :- open('altBit3bis.txt',write,Str),
    AltBit3 = (m1,0) : S1,
    S1 = ((m2,0) : S2 ) + ((a1,0) : (m2,0) : S6 ),
    S2 = ((a1,0) : S6 ) + ((a2,0) : S4 ) + ((m3,0) : S3 ),
    S3 = ((a1,0) : S7 ) + ((a2,0) : S8 ) + ((a3,0) : S5 ),
    S4 = ((a1,0) : (m3,0) : (a3,0) : AltBit3 ) + ((m3,0) : S8 ),
    S5 = ((a1,0) : (a2,0) : AltBit3 ) + ((a2,0) : (a1,0) : AltBit3 ),
    S6 = ((m3,0) : S7 ) + ((a2,0) : (m3,0) : (a3,0) : AltBit3),
    S7 = ((a3,0) : (a2,0) : AltBit3 ) + ((a2,0) : (a3,0) : AltBit3 ),
    S8 = ((a1,0) : (a3,0) : AltBit3 ) + ((a3,0) : (a1,0) : AltBit3 ),
    setof(IL,accept(N,AltBit3,IL),OL),write(OL),print_list(Str,OL),close(Str).

%%% the following two types are equivalent

testAltBitXor3(N) :- open('altBitXor3.txt',write,Str),M1M2M3=m1:m2:m3:M1M2M3,M1A1=(m1,1):(a1,1):M1A1,M2A2=(m2,1):(a2,1):M2A2,M3A3=(m3,2):(a3,0):M3A3,AM=(a1:(m3:(a2:AM)))+(a2:(m3:(a1:AM))),T=((M1A1|M2A2)|(M3A3|M1M2M3)|AM),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

%%% the following two types are equivalent

testAltBitOr3(N) :- open('altBitOr3.txt',write,Str),M1M2M3=(m1:m2:m3:M1M2M3),M1A1=(m1,1):(a1,1):M1A1,M2A2=(m2,1):(a2,1):M2A2,M3A3=(m3,2):(a3,0):M3A3,AM=(a1:m3:a2:AM)+(a2:m3:a1:AM)+(a1:a2:m3:AM)+(a2:a1:m3:AM),T=((M1A1|M2A2)|(M3A3|M1M2M3)|AM),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

testAltBitOr3bis(N) :- open('altBitOr3bis.txt',write,Str),M1M2M3=(m1:m2:m3:M1M2M3),M1A1=(m1,1):(a1,1):M1A1,M2A2=(m2,1):(a2,1):M2A2,M3A3=(m3,2):(a3,0):M3A3,
AMbis=(((a1:((a2:lambda)|(m3:lambda)))+(a2:((a1:lambda)|(m3:lambda))))*AMbis),T=((M1A1|M2A2)|(M3A3|M1M2M3)|AMbis),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

%%% the following two types are equivalent

testAltBitAnd3(N) :- open('altBitAnd3.txt',write,Str),M1M2M3=m1:m2:m3:M1M2M3,M1A1=(m1,1):(a1,1):M1A1,M2A2=(m2,1):(a2,1):M2A2,M3A3=(m3,3):(a3,0):M3A3,AM=(((a1:m3:lambda)|(a2:m3:lambda))*AM),T=((M1A1|M2A2)|(M3A3|M1M2M3)|AM),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

testAltBitAnd3bis(N) :- open('altBitAnd3bis.txt',write,Str),M1M2M3=m1:m2:m3:M1M2M3,M1A1=(m1,1):(a1,1):M1A1,M2A2=(m2,1):(a2,1):M2A2,M3A3=(m3,2):(a3,0):M3A3,
AMbis=((a1:lambda)|(a2:lambda))*(m3:AMbis),T=((M1A1|M2A2)|(M3A3|M1M2M3)|AMbis),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

%%% the following two types are equivalent

testAfter3times(N) :- open('after3times.txt',write,Str),T=(offer,0):(offer,0):(offer,0):OB,OB = ((buy,0):lambda)+((offer,0):OB),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).  

testAfterKtimes(N) :- open('afterKtimes.txt',write,Str),T=((O * ((buy,3):lambda)) | OB), O = lambda+((offer,0):O)+((offer,1):O), OB = ( lambda + (offer:((buy:lambda) | OB))),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).  

testAfterKtimesDet(N) :- open('afterKtimesDet.txt',write,Str),O=(lambda+((offer,1):(((O|((buy:lambda)+lambda)))))),B=(offer:B)+((buy,3):lambda),T=(O|B),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).  

gen_offer(0,L,L) :- !.
gen_offer(N,L1,L2) :- P is N-1,gen_offer(P,[offer|L1],L2).

testAfterKtimesDetFail(N) :- gen_offer(N,[],L),O=(lambda+((offer,1):(((O|((buy:lambda)+lambda)))))),B=(offer:B)+((buy,3):lambda),T=(O|B),accept(T,L).  
testAfterKtimesDetSucc(N) :- gen_offer(N,[buy],L),O=(lambda+((offer,1):(((O|((buy:lambda)+lambda)))))),B=(offer:B)+((buy,3):lambda),T=(O|B),accept(T,L).  
 
%%% the following two types are equivalent

testRegularPlus(N) :- open('regularPlus.txt',write,Str),
%T=((((a,0):lambda)+lambda)|(((b,0):lambda)+lambda)|(((c,0):lambda)+lambda)|(((d,0):lambda)+lambda)),
T=(((a:lambda)+lambda)|((b:lambda)+lambda)|((c:lambda)+lambda)|((d:lambda)+lambda)|((e:lambda)+lambda)|((f:lambda)+lambda)|(((a,1):P)+((b,1):P)+((c,1):P)+((d,1):P)+((e,1):P)+((f,1):P))),
P=lambda+((a,1):P)+((b,1):P)+((c,1):P)+((d,1):P)+((e,1):P)+((f,1):P),
setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

testRegularPlusBis(N) :- open('regularPlusBis.txt',write,Str),
%T=((((a,0):lambda)+lambda)|(((b,0):lambda)+lambda)|(((c,0):lambda)+lambda)|(((d,0):lambda)+lambda)),
T=((((a,1):lambda)+lambda)|(((b,1):lambda)+lambda)|(((c,1):lambda)+lambda)|(((d,1):lambda)+lambda)|(((e,1):lambda)+lambda)|(((f,1):lambda)+lambda)|((a:P)+(b:P)+(c:P)+(d:P)+(e:P)+(f:P))),
P=lambda+(a:P)+(b:P)+(c:P)+(d:P)+(e:P)+(f:P),
setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

%%%%%%  a^nb^nc^n ok, but in some cases error detection is delayed. 
%%%%%%  Example:[a, a, a, a, a, b, b, c, c]

testContextSensitive(N) :- open('contextSensitive.txt',write,Str),
AB = lambda + (((a,0):AB)*((b,1):lambda)),
BC = lambda + ((b:BC)*((c,0):lambda)),
T = (AB | BC),
setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

%%%%%%  a^nb^nc^n, errors are blocked as soon as possible
 
testContextSensitiveDet(N) :- open('contextSensitiveDet.txt',write,Str),
AB = lambda + (((a,0):AB2)*((b:c:lambda))),
AB2 = lambda + (((a,0):AB2)*(b:lambda)),
BC = lambda + BC2, 
BC2 = (b,1):(((c,1):lambda)+BC2*((c,0):lambda)),
T = (AB | BC),
setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

%%%%%% reviewer1 example 

testAltBitReviewer1(N) :- open('altBitReviewer1.txt',write,Str),M1M2=m1:m2:M1M2,M1A1=(m1,1):(a1,0):M1A1,M2A2=(m2,1):(a2,0):M2A2,M3M4=m3:m4:M3M4,M3A3=(m3,1):(a3,0):M3A3,M4A4=(m4,1):(a4,0):M4A4,T=((M1M2|M1A1)|(M2A2|M3M4)|(M3A3|M4A4)),setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).

print_list(_,[]).
print_list(S,[X|L]) :- write(S,X),write(S,'\n'),print_list(S,L).

