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 >
Text File  |  2013-09-14  |  8KB  |  121 lines

  1. next(0,(A,N):T,A,T,N) :- !.
  2. next(M,A:T1,A,T1,N) :- !, M > 0, N is M - 1.
  3. next(M,T1+_,A,T2,N) :- next(M,T1,A,T2,N). 
  4. next(M,_+T1,A,T2,N) :- !,next(M,T1,A,T2,N).
  5. next(N,T1|T2,A,T3|T2,M) :- next(N,T1,A,T3,M). 
  6. next(N,T1|T2,A,T1|T3,M) :- next(N,T2,A,T3,M).
  7. next(N,T1|T2,A,T3|T4,P) :- next(N,T1,A,T3,M), M > 0, next(M,T2,A,T4,P). 
  8. next(N,T1|T2,A,T4|T3,P) :- !,next(N,T2,A,T3,M), M > 0, next(M,T1,A,T4,P). 
  9. next(M,T1*T2,A,T3*T2,N) :- next(M,T1,A,T3,N).
  10. next(M,T1*T2,A,T3,N) :- !,maybe_empty(T1), next(M,T2,A,T3,N).
  11.  
  12. maybe_empty(lambda) :- !.
  13. maybe_empty(T1+T2) :- (maybe_empty(T1),!;maybe_empty(T2)).
  14. maybe_empty(T1|T2) :- !,maybe_empty(T1),maybe_empty(T2).
  15. maybe_empty(T1*T2) :- !,maybe_empty(T1),maybe_empty(T2).
  16.  
  17. not_empty(_:_).
  18. not_empty(T1+T2) :- !,not_empty(T1),not_empty(T2).
  19. not_empty(T1|T2) :- (not_empty(T1),!;not_empty(T2)).
  20. not_empty(T1*T2) :- (not_empty(T1),!;not_empty(T2)).
  21.  
  22. accept(T1,[A|L]) :- next(0,T1,A,T2,0),accept(T2,L).
  23. accept(T,[]) :- maybe_empty(T).
  24.  
  25. accept(_,T,[*]) :- maybe_empty(T).
  26. accept(0,T,[]) :- !,not_empty(T).
  27. accept(N,T1,[A|L]) :- next(0,T1,A,T2,0), M is N - 1,accept(M,T2,L).
  28.  
  29. %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).
  30.  
  31. 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).
  32.  
  33. %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).
  34.  
  35. 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).
  36.  
  37. testAltBit3bis(N) :- open('altBit3bis.txt',write,Str),
  38.     AltBit3 = (m1,0) : S1,
  39.     S1 = ((m2,0) : S2 ) + ((a1,0) : (m2,0) : S6 ),
  40.     S2 = ((a1,0) : S6 ) + ((a2,0) : S4 ) + ((m3,0) : S3 ),
  41.     S3 = ((a1,0) : S7 ) + ((a2,0) : S8 ) + ((a3,0) : S5 ),
  42.     S4 = ((a1,0) : (m3,0) : (a3,0) : AltBit3 ) + ((m3,0) : S8 ),
  43.     S5 = ((a1,0) : (a2,0) : AltBit3 ) + ((a2,0) : (a1,0) : AltBit3 ),
  44.     S6 = ((m3,0) : S7 ) + ((a2,0) : (m3,0) : (a3,0) : AltBit3),
  45.     S7 = ((a3,0) : (a2,0) : AltBit3 ) + ((a2,0) : (a3,0) : AltBit3 ),
  46.     S8 = ((a1,0) : (a3,0) : AltBit3 ) + ((a3,0) : (a1,0) : AltBit3 ),
  47.     setof(IL,accept(N,AltBit3,IL),OL),write(OL),print_list(Str,OL),close(Str).
  48.  
  49. %%% the following two types are equivalent
  50.  
  51. 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).
  52.  
  53. %%% the following two types are equivalent
  54.  
  55. 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).
  56.  
  57. 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,
  58. 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).
  59.  
  60. %%% the following two types are equivalent
  61.  
  62. 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).
  63.  
  64. 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,
  65. 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).
  66.  
  67. %%% the following two types are equivalent
  68.  
  69. 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).  
  70.  
  71. 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).  
  72.  
  73. 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).  
  74.  
  75. gen_offer(0,L,L) :- !.
  76. gen_offer(N,L1,L2) :- P is N-1,gen_offer(P,[offer|L1],L2).
  77.  
  78. 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).  
  79. 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).  
  80.  
  81. %%% the following two types are equivalent
  82.  
  83. testRegularPlus(N) :- open('regularPlus.txt',write,Str),
  84. %T=((((a,0):lambda)+lambda)|(((b,0):lambda)+lambda)|(((c,0):lambda)+lambda)|(((d,0):lambda)+lambda)),
  85. 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))),
  86. P=lambda+((a,1):P)+((b,1):P)+((c,1):P)+((d,1):P)+((e,1):P)+((f,1):P),
  87. setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).
  88.  
  89. testRegularPlusBis(N) :- open('regularPlusBis.txt',write,Str),
  90. %T=((((a,0):lambda)+lambda)|(((b,0):lambda)+lambda)|(((c,0):lambda)+lambda)|(((d,0):lambda)+lambda)),
  91. 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))),
  92. P=lambda+(a:P)+(b:P)+(c:P)+(d:P)+(e:P)+(f:P),
  93. setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).
  94.  
  95. %%%%%%  a^nb^nc^n ok, but in some cases error detection is delayed. 
  96. %%%%%%  Example:[a, a, a, a, a, b, b, c, c]
  97.  
  98. testContextSensitive(N) :- open('contextSensitive.txt',write,Str),
  99. AB = lambda + (((a,0):AB)*((b,1):lambda)),
  100. BC = lambda + ((b:BC)*((c,0):lambda)),
  101. T = (AB | BC),
  102. setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).
  103.  
  104. %%%%%%  a^nb^nc^n, errors are blocked as soon as possible
  105.  
  106. testContextSensitiveDet(N) :- open('contextSensitiveDet.txt',write,Str),
  107. AB = lambda + (((a,0):AB2)*((b:c:lambda))),
  108. AB2 = lambda + (((a,0):AB2)*(b:lambda)),
  109. BC = lambda + BC2, 
  110. BC2 = (b,1):(((c,1):lambda)+BC2*((c,0):lambda)),
  111. T = (AB | BC),
  112. setof(IL,accept(N,T,IL),OL),write(OL),print_list(Str,OL),close(Str).
  113.  
  114. %%%%%% reviewer1 example 
  115.  
  116. 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).
  117.  
  118. print_list(_,[]).
  119. print_list(S,[X|L]) :- write(S,X),write(S,'\n'),print_list(S,L).
  120.  
  121.