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

% =================================================================
% 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 listmin(list(int),bool,int).     % 2nd: IsDef     3rd: min
:- mode listmin(in,out,out).
:- cata listmin/3-1.

listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).  % 0 can be any int.
listmin([H|T],IsDef,Min) :-
         constr( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H)) ),
         listmin(T,IsDefT,MinT).

% ---
:- 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),
    listmin(L,IsDefMinL,MinL), is_asorted(L,BL), 
    listmin(S,IsDefMinS,MinS),  is_asorted(S,BS),
    quicksort(L,S).

:- spec partition(P,Xs,Ls,Bs) ==> 
        listmin(Ls,IsDefMinLs,MinLs),  listmin(Bs,IsDefMinBs,MinBs), listmin(Xs,IsDefMinXs,MinXs), 
        is_asorted(Xs,B3), is_asorted(Ls,B4), is_asorted(Bs,B5) => constr(true).

:- spec concat4(Xs,Y,Ys,Zs) ==> 
     listmin(Xs,IsDefMinXs,MinXs), listmin(Ys,IsDefMinYs,MinYs), listmin(Zs,IsDefMinZs,MinZs), 
     is_asorted(Xs,B3), is_asorted(Ys,B4), is_asorted(Zs,B5) => constr(true).

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