% ================================================================= :- pred constr(bool). :- mode constr(in). :- ignore constr/1. % ================================================================= % Program. ascending sorting :- pred bubblesort(list(int),list(int)). :- mode bubblesort(in,out). bubblesort(L,L) :- swap(L,L1,B), eqlist(L,L1), constr(~B). bubblesort(L,SL) :- swap(L,L1,B), constr(B), bubblesort(L1,SL). :- pred eqlist(list(int),list(int)). :- mode eqlist(in,in). eqlist(L,L). :- pred swap(list(int),list(int),bool). % bool is true if a swap has been done :- mode swap(in,out,out). swap([],[],B) :- constr(~B). swap([X],[X],B) :- constr(~B). swap([X,Y|Ys],[Y|Zs],B) :- constr(~B & (X > Y)), % error: ~B should be B cons(X,Ys,XYs), swap(XYs,Zs,B). swap([X,Y|Ys],[X|Zs],B) :- constr(X =< Y), cons(Y,Ys,YYs), swap(YYs,Zs,B). :- pred cons(int,list(int),list(int)). :- mode cons(in,in,out). cons(H,T,[H|T]). % ================================================================= % catamorphisms :- pred is_asorted(list(int),bool). :- mode is_asorted(in,out). :- cata is_asorted/2-1. is_asorted([],Res) :- constr(Res). is_asorted([H|T],Res) :- hd(T,IsDefT,HdT), is_asorted(T,ResT), constr(Res=(IsDefT => (H= (BLB & (~ToF)))) & ((~BLA) => ToF) ) ), is_asorted(LA,BLA), is_asorted(LB,BLB) , swap(LA,LB,ToF). :- pred ff3. ff3 :- constr( ~(( IsDefHT & ((IsDefT & (H= (BT = BHT))) & ((~IsDefT) => BHT)) ), is_asorted(T,BT), listMin(HT,IsDefHT,MinHT), is_asorted(HT,BHT), listMin(T,IsDefT,MinT), cons(H,T,HT). % ================================================================= :- query ff1/0. :- query ff2/0. :- query ff3/0. % =================================================================