% =================================================================
:- 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.
	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).

% =================================================================
% catamorphisms   weakly ascending-order sorting
:- 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=<HdT & ResT))).

% ---
:- pred hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Hd) :- constr( ~IsDef & Hd=0 ).    % 0 can be any int.
hd([H|T],IsDef,Hd) :- constr( IsDef & Hd=H ).


% =================================================================
% Verification. 
% Property:
    
:- pred ff1.
ff1 :-
    constr(~BS), 
    is_asorted(L,BL),  
    is_asorted(S,BS),
    quicksort(L,S).

:- spec partition(P,Xs,Ls,Bs) ==> 
        is_asorted(Xs,B3), is_asorted(Ls,B4), is_asorted(Bs,B5) => constr(true).

:- spec concat4(Xs,Y,Ys,Zs) ==> 
     is_asorted(Xs,B3), is_asorted(Ys,B4), is_asorted(Zs,B5) => constr(true).

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