% =================================================================
:- 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,L,false).
bubblesort(L,SL) :- swap(L,L1,true),
                    bubblesort(L1,SL).

:- pred swap(list(int),list(int),bool).   % bool is true if a swap has been done
:- mode swap(in,out,out).

swap([],[],false).
swap([X],[X],false).
swap([X,Y|Ys],[Y|Zs],true) :-
         constr(X > Y),
         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]).

% -------------------------------------
% catamorphism
:- pred count(int,list(int),int).
:- mode count(in,in,out).
:- cata count/3-2.

count(X,[],Res) :- constr( Res=0 ).
count(X,[Y|Ys],Res) :-
    constr( Res=ite(X=Y,(ResT+1),ResT) ),
    count(X,Ys,ResT).

% =================================================================
% Contract on bubblesort:
:- spec bubblesort(L,S) ==>
        count(X,L,CL), count(X,S,CS) =>
        constr( CL=CS ).

% Contract on swap:
:- spec swap(LA,LB,ToF) ==>                  % ToF: boolean variable (true or false)
        count(X,LA,CLA), count(X,LB,CLB)  =>
        constr( CLA = CLB ).

% Contract on cons:
:- spec cons(H,T,HT) ==>
       count(X,T,CT), count(X,HT,CHT) =>
       constr( CHT = ite(X=H, (CT+1), CT) ).

% =================================================================
% verification.
% Property:
:- pred ff1.
ff1 :-
   constr(~(CL = CS)),
   count(X,L,CL), count(X,S,CS),
   bubblesort(L,S).

:- pred ff2.
ff2 :-
   constr( ~(CLA = CLB) ),
   count(X,LA,CLA), count(X,LB,CLB),
   swap(LA,LB,ToF).

:- pred ff3.
ff3 :-
   constr( ~(CHT = ite(X=H, (CT+1), CT)) ),
   count(X,T,CT), count(X,HT,CHT),
   cons(H,T,HT).

% =================================================================
% NON-CATA predicates: bubblesort cons constr swap