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


% version for SWISH Prolog.
%partition(_, [], [], []).       
%partition(X, [Y | Ys], [Y | Ls], Bs) :- 
%      	X #>Y,    
%      	partition(X, Ys, Ls, Bs).
%partition(X, [Y | Xs], Ls, [Y | Bs]) :-  
%			      	X#=<Y,   
%  			partition(X, Xs, Ls, Bs).


% =================================================================
% catamorphisms

:- pred listMax(list(int),bool,int).
:- mode listMax(in,out,out).
:- cata listMax/3-1.

listMax([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listMax([H|T],IsDef,Max) :-
         constr( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H )) ),
         listMax(T,IsDefT,MaxT).

:- pred lastElem(list(int),bool,int).
:- mode lastElem(in,out,out).
:- cata lastElem/3-1.

lastElem([],IsDef,Last) :- constr( ((~IsDef) & (Last=0)) ).
lastElem([H|T],IsDef,Last) :-
         constr( IsDef & (Last=ite(IsDefT,LastT,H)) ),
         lastElem(T,IsDefT,LastT).

% =================================================================
% Contract on quicksort:
:- spec quicksort(L,S) ==>
       listMax(L,IsDefLMax,MaxL), listMax(S,IsDefSMax,MaxS), lastElem(S,IsDefSLast,LastS) =>
       constr( (( ((IsDefLMax = IsDefSMax) & 
                 (IsDefSMax = IsDefSLast))) & 
                 (IsDefLMax => (MaxL=LastS)))).

% Contract on partition.
% One would have desired to write two contracts, one for listMax and one for lastElem.
% Note listMax is defined iff lastElem is defined, i.e.,
% IsDefS = IsDefLSmalls,  IsDefB = IsDefLBigs, IsDefL = IsDefLastLs.

:- spec partition(P,Ls,Smalls,Bigs) ==>     % Ls = Smalls <> Bigs
			listMax(Smalls,IsDefS,MSmalls), listMax(Bigs,IsDefB,MBigs),          
       listMax(Ls,IsDefL,MaxLs),                                              
			constr( Max = ite(MBigs>MSmalls,MBigs,MSmalls) ),                   
       lastElem(Smalls,IsDefLSmalls,LastSmalls), lastElem(Bigs,IsDefLBigs,LastBigs),  
			lastElem(Ls,IsDefLastLs,LastLs)                                              
			=>
			constr(( ((( (IsDefS &    IsDefB )   => (  IsDefL & ( MaxLs=Max ) )) &
							 ((   IsDefS &  (~IsDefB) )  => (  IsDefL & ( MaxLs=MSmalls ) ))) &
							 (( (~IsDefS) &   IsDefB )   => (  IsDefL & ( MaxLs=MBigs ) ))) &
							 (( (~IsDefS) & (~IsDefB) )  =  ( ~IsDefL ))
						 ) &  ( 
((  (~IsDefLSmalls &  IsDefLBigs )  => (  IsDefLastLs & ( LastLs=LastBigs ) )) &
							 ((  IsDefLSmalls & (~IsDefLBigs) )  => (  IsDefLastLs & ( LastLs=LastSmalls ) ))) &
							 ( ((~IsDefLSmalls) & (~IsDefLBigs)) =  ( ~IsDefLastLs ))
							 )).

% Contract on concat:
:- spec concat(Xs,Y,Ys,Zs) ==>
       listMax(Xs,IsDefXs,MaxXs), listMax(Ys,IsDefYs,MaxYs),
       listMax(Zs,IsDefZs,MaxZs), 
       lastElem(Xs,IsDefLEXs,LastXs), lastElem(Ys,IsDefLEYs,LastYs),  % for lastElem
			 lastElem(Zs,IsDefLEZs,LastZs),
       constr( Max2=ite(MaxXs>MaxYs,MaxXs,MaxYs) & Max3=ite(Max2>Y,Max2,Y) ) 
       =>
       constr(( ((((IsDefXs &  IsDefYs )  => ( IsDefZs & ( MaxZs=Max3 ) )) &
               ((   IsDefXs & ~IsDefYs )  => ( IsDefZs & 
                                                ( MaxZs=ite(MaxXs>Y,MaxXs,Y) ) ))) &
               ((  ~IsDefXs &  IsDefYs )  => ( IsDefZs & 
                                                ( MaxZs=ite(MaxYs>Y,MaxYs,Y) ) ))) &
               ((  ~IsDefXs & ~IsDefYs )  => ( IsDefZs & ( MaxZs=Y )))
              )  &  ( IsDefLEZs & (
                (( IsDefLEYs)  => ( IsDefLEZs & ( LastZs=LastYs ))) &
                ((~IsDefLEYs)  => ( IsDefLEZs & ( LastZs=Y ))))
               )).

% =================================================================
% Verification. 
% Property:
:- pred ff1.
ff1 :-        % listMax of unsorted equal lastElem of ascending, quicksorted list 
   constr( ~((    (IsDefLMax = IsDefSMax) & 
                  (IsDefSMax = IsDefSLast)) & 
                  (IsDefLMax => ((MaxL=LastS) & (MaxL=MaxS))) )),
   listMax(L,IsDefLMax,MaxL), listMax(S,IsDefSMax,MaxS), 
   lastElem(S,IsDefSLast,LastS),
   quicksort(L,S).

:- pred ff2.
ff2 :-      % listMax and lastElem on partition
   constr( ~(( ((((  IsDefS &  IsDefB )  => (  IsDefL & ( MaxLs=Max ) )) &
								 ((  IsDefS & ~IsDefB )  => (  IsDefL & ( MaxLs=MSmalls ) ))) &
								 (( ~IsDefS &  IsDefB )  => (  IsDefL & ( MaxLs=MBigs ) ))) &
								 (( ~IsDefS & ~IsDefB )  =  ( ~IsDefL ))
							 )
           &  (  (((~IsDefLSmalls &  IsDefLBigs ) => (  IsDefLastLs & ( LastLs=LastBigs ) )) &
								 ((  IsDefLSmalls & ~IsDefLBigs ) => (  IsDefLastLs & ( LastLs=LastSmalls ) ))) &
								 (( ~IsDefLSmalls & ~IsDefLBigs ) =  ( ~IsDefLastLs ))
 							 ) )),
   listMax(Smalls,IsDefS,MSmalls), listMax(Bigs,IsDefB,MBigs),          % for listMax
   listMax(Ls,IsDefL,MaxLs),                                            % for listMax
   constr( Max = ite(MBigs>MSmalls,MBigs,MSmalls) ),                    % for listMax
   lastElem(Smalls,IsDefLSmalls,LastSmalls), lastElem(Bigs,IsDefLBigs,LastBigs),  % for lastElem
 	 lastElem(Ls,IsDefLastLs,LastLs),
   partition(P,Ls,Smalls,Bigs).

:- pred ff3.
ff3 :-     % listMax and lastElem on concat   
   constr(~(( ((((IsDefXs &  IsDefYs )  => ( IsDefZs & ( MaxZs=Max3 ) )) &
               ((   IsDefXs & ~IsDefYs )  => ( IsDefZs & 
                                                ( MaxZs=ite(MaxXs>Y,MaxXs,Y) ) ))) &
               ((  ~IsDefXs &  IsDefYs )  => ( IsDefZs & 
                                                ( MaxZs=ite(MaxYs>Y,MaxYs,Y) ) ))) &
               ((  ~IsDefXs & ~IsDefYs )  => ( IsDefZs & ( MaxZs=Y )))
              )  &  ( IsDefLEZs & (
                (( IsDefLEYs)  => ( IsDefLEZs & ( LastZs=LastYs ))) &
                ((~IsDefLEYs)  => ( IsDefLEZs & ( LastZs=Y ))))
               ))),
       listMax(Xs,IsDefXs,MaxXs), listMax(Ys,IsDefYs,MaxYs),
       listMax(Zs,IsDefZs,MaxZs), 
       lastElem(Xs,IsDefLEXs,LastXs), lastElem(Ys,IsDefLEYs,LastYs),  % for lastElem
			 lastElem(Zs,IsDefLEZs,LastZs),
       constr( Max2=ite(MaxXs>MaxYs,MaxXs,MaxYs) & Max3=ite(Max2>Y,Max2,Y) ),    
       concat(Xs,Y,Ys,Zs).

%:- pred ff3.
%ff3 :-     % listMax and lastElem on append
%   constr( ~(( ((((   IsDefXs &  IsDefYs )  => (  IsDefZs & ( MaxZs=Max ) )) &
%                ((    IsDefXs & ~IsDefYs )  => (  IsDefZs & ( MaxZs=MaxXs ) ))) &
%                ((   ~IsDefXs &  IsDefYs )  => (  IsDefZs & ( MaxZs=MaxYs ) ))) &
%                ((   ~IsDefXs & ~IsDefYs )  =  ( ~IsDefZs ))
%               )
%            &  ( ((((( IsDefYs_LE )                => (  IsDefZs_LE & ( LastZs=LastYs ) )) &
%                 ((    IsDefXs_LE & ~IsDefYs_LE )  => (  IsDefZs_LE & ( LastZs=LastXs ) )))) &
%                 ((   ~IsDefXs_LE & ~IsDefYs_LE )  =  ( ~IsDefZs_LE )))
%              ))
%         ),
%   listMax(Xs,IsDefXs,MaxXs), listMax(Ys,IsDefYs,MaxYs),
%   listMax(Zs,IsDefZs,MaxZs), 
%   constr( Max = ite(MaxXs>MaxYs,MaxXs,MaxYs) ), 
%   lastElem(Xs,IsDefXs_LE,LastXs), lastElem(Ys,IsDefYs_LE,LastYs),
%   lastElem(Zs,IsDefZs_LE,LastZs),   
%   append(Xs,Ys,Zs).


% =================================================================
% NON-CATA predicates: concat constr partition quicksort