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

% =================================================================
% Program
:- pred quicksort(list(int),list(int)).
:- mode quicksort(in,out).

quicksort([H], [H,K]). %error: [H,K] --> [H]
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.
  concat4(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 concat4(list(int),int,list(int),list(int)).
:- mode concat4(in,in,in,out).
concat4([],Y,Ys,[Y|Ys]).
concat4([X|Xs],Y,Ys,[X|Zs]) :-
	concat4(Xs,Y,Ys,Zs).


% =================================================================
% catamorphism
:- pred sum(list(int),int).
:- mode sum(in,out).
:- cata sum/2-1.

sum([],S) :- constr((S=0)).
sum([H|T],S) :-
  constr( S=(H+ST) ),
  sum(T,ST).

% =================================================================
% Verification. 
% Property:
:- pred ff1.
ff1 :- 
   constr(~(SL=SS)), 
   sum(L,SL), sum(S,SS),  
   quicksort(L,S).

%:- pred ff2.
%ff2 :- 
%   constr( ~(SLs = (SSmalls+SBigs)) ), 
%   sum(Smalls,SSmalls), sum(Bigs,SBigs), sum(Ls,SLs), 
%   partition(P,Ls,Smalls,Bigs).
%
%:- pred ff3.
%ff3 :- 
%   constr( ~(SZs = (SXs+Y+SYs)) ), 
%   sum(Xs,SXs),  sum(Ys,SYs), sum(Zs,SZs), 
%   concat4(Xs,Y,Ys,Zs).

% =================================================================
:- query ff1/0.
%:- query ff2/0.
%:- query ff3/0.
% =================================================================

%  Catamorphic abstraction

:- cata_abs list(int) ==> sum(Xs,SXs).

% =================================================================