% =================================================================
:- 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, [], [], [X]).  % error: [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([],Y,Y).
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
:- 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 listmax(list(int),bool,int).
:- mode listmax(in,out,out).
:- cata listmax/3-1.

listmax([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ). % A 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 listmin(list(int),bool,int).    
:- mode listmin(in,out,out).
:- cata listmin/3-1.

listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ). % A 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) ).      % Hd can be any int.
hd([H|T],IsDef,Hd) :- constr( IsDef & (Hd=H) ).
% =================================================================
% Verification.
% Property:
:- pred ff1.
ff1 :-
   constr(~( B)),
   is_asorted(S,B),
   quicksort(L,S).
 
:- pred ff2.    % partition  
ff2 :-
  constr(~(
          (((((( IsDefMaxS &  IsDefMaxB ) => ( IsDefMaxL & ( MaxLs=ite(MaxSmalls>MaxBigs,MaxSmalls,MaxBigs) ) )) &
                ((  IsDefMaxS & ~IsDefMaxB )  => (  IsDefMaxL & ( MaxLs=MaxSmalls ) ))) &
                (( ~IsDefMaxS &  IsDefMaxB )  => (  IsDefMaxL & ( MaxLs=MaxBigs ) ))) &
                (( ~IsDefMaxS & ~IsDefMaxB )  =  ( ~IsDefMaxL ))
              ) &
              ((((( IsDefMinS &  IsDefMinB )  => (  IsDefMinL & ( MinLs=ite(MinSmalls<MinBigs,MinSmalls,MinBigs) ) )) &
                ((  IsDefMinS & ~IsDefMinB )  => (  IsDefMinL & ( MinLs=MinSmalls ) ))) &
                (( ~IsDefMinS &  IsDefMinB )  => (  IsDefMinL & ( MinLs=MinBigs ) ))) &
                (( ~IsDefMinS & ~IsDefMinB )  =  ( ~IsDefMinL ))
              )) &
         (( (((IsDefMinS & IsDefMaxS) => ((X > MaxSmalls) & (MinLs = MinSmalls)))  &
             ((IsDefMinB & IsDefMaxB) => ((X =< MinBigs) & (MaxLs = MaxBigs))) ) &
              (IsDefMinL = (IsDefMinS v IsDefMinB)) ) &
              (IsDefMaxL = (IsDefMaxS v IsDefMaxB)) ))),    
  listmax(Smalls,IsDefMaxS,MaxSmalls), listmax(Bigs,IsDefMaxB,MaxBigs), listmax(Ls,IsDefMaxL,MaxLs),
  listmin(Smalls,IsDefMinS,MinSmalls), listmin(Bigs,IsDefMinB,MinBigs), listmin(Ls,IsDefMinL,MinLs),
  partition(X,Ls,Smalls,Bigs).

:- pred ff3.   % append
ff3 :-
 constr(~((((((((   IsDefMaxXs &  IsDefMaxYs ) => (  IsDefMaxZs & ( MaxZs=ite(MaxXs>MaxYs,MaxXs,MaxYs) ) )) &
                ((  IsDefMaxXs & ~IsDefMaxYs ) => (  IsDefMaxZs & ( MaxZs=MaxXs ) ))) &
                (( ~IsDefMaxXs &  IsDefMaxYs ) => (  IsDefMaxZs & ( MaxZs=MaxYs ) ))) &
                (( ~IsDefMaxXs & ~IsDefMaxYs ) =  ( ~IsDefMaxZs ))
              ) ) & 
              (((((IsDefMaxXs & (IsDefMinYs & MaxXs=<MinYs)) v ~IsDefMaxXs) v ~IsDefMinYs) 
                   => (B3 & B4) = B5))  
              ) &
            (((((   IsDefMinXs &  IsDefMinYs ) => (  IsDefMinZs & ( MinZs=ite(MinXs<MinYs,MinXs,MinYs) ) )) &
                ((  IsDefMinXs & ~IsDefMinYs ) => (  IsDefMinZs & ( MinZs=MinXs ) ))) &
                (( ~IsDefMinXs &  IsDefMinYs ) => (  IsDefMinZs & ( MinZs=MinYs ) ))) &
                (( ~IsDefMinXs & ~IsDefMinYs ) =  ( ~IsDefMinZs ))
              ))), 
   listmax(Xs,IsDefMaxXs,MaxXs), listmax(Ys,IsDefMaxYs,MaxYs), listmax(Zs,IsDefMaxZs,MaxZs), 
   listmin(Xs,IsDefMinXs,MinXs), listmin(Ys,IsDefMinYs,MinYs), listmin(Zs,IsDefMinZs,MinZs), 
   is_asorted(Xs,B3), is_asorted(Ys,B4), is_asorted(Zs,B5),  
   append(Xs,Ys,Zs).
   
:- pred ff4.  % cons
ff4 :-
  constr( ~( ((IsDefMinYs) & ((IsDefMinXs & (X=<MinXs)) => ( (MaxXs = MaxYs) & (X=<MinYs))) ) & 
            (~IsDefMinYs => ((X=MinYs) & (X=MaxYs)) ) ) ),
	listmin(Xs,IsDefMinXs,MinXs), listmin(Ys,IsDefMinYs,MinYs), 
  listmax(Xs,IsDefMaxXs,MaxXs), listmax(Ys,IsDefMaxYs,MaxYs), 
  cons(X,Xs,Ys).

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