% =================================================================
:- 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.
	concat(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 concat(list(int),int,list(int),list(int)).
:- mode concat(in,in,in,out).
concat([],Y,Ys,[Y|Ys]).
concat([X|Xs],Y,Ys,[X|Zs]) :-
	  concat(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(~B),
    quicksort(L,S),
    is_asorted(S,B).

% --- partition
:- pred ff2.
ff2 :-
      listmin(Ls,IsDefMinLs,MinLs), listmax(Ls,IsDefMaxLs,MaxLs),  
      listmin(Bs,IsDefMinBs,MinBs), listmax(Bs,IsDefMaxBs,MaxBs), 
      listmin(Xs,IsDefMinXs,MinXs), listmax(Xs,IsDefMaxXs,MaxXs),
      constr( ~(((       ((IsDefMinLs & (IsDefMaxLs & IsDefMinXs)) => ((P >  MaxLs) & (MinXs = MinLs)))   &  
                         ((IsDefMinBs & (IsDefMaxBs & IsDefMaxXs)) => ((P =< MinBs) & (MaxXs = MaxBs)))  ) & 
                         (IsDefMinXs = (IsDefMinLs v IsDefMinBs))    ) &
                         (IsDefMaxXs = (IsDefMaxLs v IsDefMaxBs))  )),
      partition(P,Xs,Ls,Bs).
 
% --- concat:
:- pred ff3.
ff3 :-    
     constr(~(     
     ((((   (IsDefMinXs=IsDefMaxXs) &
            (IsDefMinYs=IsDefMaxYs)) &
            ((((MaxXs =< Y) & (Y=<MinYs)) & (B3 & B4)) => B5)) &
            (((~IsDefMinXs) & (~IsDefMinYs)) => B5)) &
            ((( IsDefMinXs  & (~IsDefMinYs)) & ((MaxXs=<Y) & B3 )) => B5)) &
            ((((~IsDefMinXs) &  IsDefMinYs)  & ((Y=<MinYs) & B4 )) => B5 ) )),
     listmin(Xs,IsDefMinXs,MinXs), listmax(Xs,IsDefMaxXs,MaxXs),
     listmin(Ys,IsDefMinYs,MinYs), listmax(Ys,IsDefMaxYs,MaxYs),
     is_asorted(Xs,B3), is_asorted(Ys,B4), is_asorted(Zs,B5),
     concat(Xs,Y,Ys,Zs).

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