% =================================================================
:- pred constr(bool).    
:- mode constr(in).
:- ignore constr/1.

% =================================================================
% Program
:- pred quicksort(list(int),list(int)).
:- mode quicksort(in,out).
quicksort([], []).
quicksort([X | Xs], ResL) :-
	partition(X, Xs, Smalls, Bigs),   % partition of the tail Xs 
	quicksort(Smalls, Ls),            % with respect to the pivot X.
	quicksort(Bigs, Bs),              % X is NOT in Xs.
  concat(Ls,X,Bs,ResL).

:- pred partition(int,list(int),list(int),list(int)).
:- mode partition(in,in,out,out).
partition(X, [], [], []).
partition(X, [Y | Ys], [Y | Ls], Bs) :- 
      	constr( (X>Y) ),    
      	partition(X, Ys, Ls, Bs).
partition(X, [Y | Xs], Ls, [Y | Bs]) :-  
				constr( (X=<Y)  ),   
  			partition(X, Xs, Ls, Bs).

:- pred concat(list(int),int,list(int),list(int)).
:- mode concat(in,in,in,out).
concat([],X,Ys,[X|Ys]).
concat([X|Xs],Y,Ys,[X|Zs]) :-
	concat(Xs,Y,Ys,Zs).

% =================================================================
% 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 quicksort:
:- spec quicksort(L,S) ==>
       count(X,L,CL), count(X,S,CS) =>
       constr( CL=CS ).

% Contract on partition:    Y is existentially quantified in the premise
:- spec partition(X,Ls,Smalls,Bigs) ==>
        count(Y,Smalls,CSmalls), count(Y,Bigs,CBigs), count(Y,Ls,CLs)  =>
        constr( CLs = (CSmalls+CBigs) ).

% Contract on concat:
:- spec concat(Xs,Y,Ys,Zs) ==>
        count(X,Xs,NXs), count(X,[Y],NY), count(X,Ys,NYs), count(X,Zs,NZs)   =>
        constr( (NZs = (NXs+NY+NYs)) ).

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

:- pred ff2.
ff2 :- 
   constr( ~(CLs = (CSmalls+CBigs)) ), 
   count(Y,Smalls,CSmalls), count(Y,Bigs,CBigs), count(Y,Ls,CLs), 
   partition(X,Ls,Smalls,Bigs).

:- pred ff3.
ff3 :- 
   constr( ~(NZs = (NXs+NY+NYs)) ), 
   count(X,Xs,NXs), count(X,[Y],NY), count(X,Ys,NYs), count(X,Zs,NZs), 
   concat(Xs,Y,Ys,Zs).

% --------------------------------------------------
% NON-CATA predicates: concat constr partition quicksort