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

listmax([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).  % 0 can be any int.
listmax([H|T],IsDef,Max) :-
        constr( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H)) ),
        listmax(T,IsDefT,MaxT).

% ---
:- 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),  listmax(L,IsDefMaxL,MaxL),  
    %listmin(S,IsDefMinS,MinS), listmax(S,IsDefMaxS,MaxS),  
    %is_asorted(L,BL), 
    is_asorted(S,BS),
    quicksort(L,S).

:- spec partition(P,Xs,Ls,Bs) ==> 
        listmin(Ls,IsDefMinLs,MinLs), listmax(Ls,IsDefMaxLs,MaxLs), is_asorted(Ls,B3),
        listmin(Bs,IsDefMinBs,MinBs), listmax(Bs,IsDefMaxBs,MaxBs), is_asorted(Bs,B4),
        listmin(Xs,IsDefMinXs,MinXs), listmax(Xs,IsDefMaxXs,MaxXs), is_asorted(Xs,B5) 
       => constr(true).

:- spec concat4(Xs,Y,Ys,Zs) ==> 
     listmin(Xs,IsDefMinXs,MinXs), listmax(Xs,IsDefMaxXs,MaxXs),
     listmin(Ys,IsDefMinYs,MinYs), listmax(Ys,IsDefMaxYs,MaxYs),
     listmin(Zs,IsDefMinZs,MinZs), listmax(Zs,IsDefMaxZs,MaxZs),
     is_asorted(Xs,B3), is_asorted(Ys,B4), is_asorted(Zs,B5) => constr(true).

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