home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
ftp.disi.unige.it
/
2015-02-11.ftp.disi.unige.it.tar
/
ftp.disi.unige.it
/
pub
/
.person
/
AnconaD
/
FundamentaInformaticaeTests.pl
< prev
next >
Wrap
Text File
|
2013-09-14
|
8KB
|
121 lines
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).