% =================================================================
:- 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.
  cons(X,Bs,XBs),
	append(Ls, XBs, 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 append(list(int),list(int),list(int)).
:- mode append(in,in,out).
append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).
cons(H,T,[H|T]).

% =================================================================
% catamorphisms       
% --- min of a list
:- pred listmin(list(int),bool,int). 
:- mode listmin(in,out,out).  
:- cata listmin/3-1.

listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listmin([H|T],IsDef,Min) :-
         constr( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H )) ),
         listmin(T,IsDefT,MinT).
         
% =================================================================
% Verification. 
% Property:
:- pred ff1.
ff1 :- 
    constr( ~((IsDefLMin = IsDefSMin) & 
    ((IsDefLMin & IsDefSMin) => (LMin=SMin)) )), 
    listmin(L,IsDefLMin,LMin), listmin(S,IsDefSMin,SMin),
    quicksort(L,S).

% contracts (postcondition: true)

:- spec partition(X,Ls,Smalls,Bigs) ==> listmin(Ls,B1,SLs), listmin(Smalls,B2,SSmalls), 
                                        listmin(Bigs,B3,SBigs).

:- spec append(Xs,Ys,Zs) ==> listmin(Xs,B1,SXs), listmin(Ys,B2,SYs), listmin(Zs,B3,SZs).

:- spec cons(C,A,D) ==> listmin(A,B1,SA), listmin(D,B2,SD).

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