% =================================================================
:- 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, Ls1). %error: (X, Xs, Ls, Ls1) ---> (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]).

% =================================================================
% catamorphism
:- pred listMax(list(int),bool,int).
:- 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).

%% =================================================================
%% Contract on quicksort:
%:- spec quicksort(L,S) ==>
%       listMax(L,IsDefL,MaxL), listMax(S,IsDefS,MaxS) =>
%       constr( ( (IsDefL = IsDefS) & (IsDefL => (MaxL=MaxS)) ) ).
%%
%%% Contract on partition:
%%:- spec partition(P,Ls,Smalls,Bigs) ==>
%%       listMax(Smalls,IsDefS,MSmalls), listMax(Bigs,IsDefB,MBigs), 
%%       listMax(Ls,IsDefL,MLs),
%%       constr( Max = ite(MSmalls>MBigs,MSmalls,MBigs) ) 
%%       =>
%%       constr( (((( IsDefS &  IsDefB )  => (  IsDefL & ( MLs=Max ) )) &
%%                ((  IsDefS & ~IsDefB )  => (  IsDefL & ( MLs=MSmalls ) ))) &
%%                (( ~IsDefS &  IsDefB )  => (  IsDefL & ( MLs=MBigs ) ))) &
%%                (( ~IsDefS & ~IsDefB )  =  ( ~IsDefL ))
%%              ). 
%%
%%% Contract on append:
%%:- spec append(Xs,Ys,Zs) ==>
%%       listMax(Xs,IsDefXs,MaxXs), listMax(Ys,IsDefYs,MaxYs),
%%       listMax(Zs,IsDefZs,MaxZs), 
%%       constr( Max = ite(MaxXs>MaxYs,MaxXs,MaxYs) )  
%%       =>
%%       constr( (((( IsDefXs &  IsDefYs )  => ( IsDefZs & ( MaxZs=Max ) )) &
%%               ((   IsDefXs & ~IsDefYs )  => ( IsDefZs & ( MaxZs=MaxXs ) ))) &
%%               ((  ~IsDefXs &  IsDefYs )  => ( IsDefZs & ( MaxZs=MaxYs ) ))) &
%%               ((  ~IsDefXs & ~IsDefYs )  =  ( ~IsDefZs ))
%%              ).

% =================================================================
% Verification.
% Property:
:- pred ff1.
ff1 :-
   constr(~( (IsDefL = IsDefS) & (IsDefL => (MaxL=MaxS)) )),
   listMax(L,IsDefL,MaxL), listMax(S,IsDefS,MaxS),
   quicksort(L,S).
%
%:- pred ff2.
%ff2 :-
%   constr( ~(((((    IsDefS &  IsDefB )  => (  IsDefL & ( MLs=Max ) )) &
%                 ((  IsDefS & ~IsDefB )  => (  IsDefL & ( MLs=MSmalls ) ))) &
%                 (( ~IsDefS &  IsDefB )  => (  IsDefL & ( MLs=MBigs ) ))) &
%                 (( ~IsDefS & ~IsDefB )  =  ( ~IsDefL ))
%              ) ),
%   listMax(Smalls,IsDefS,MSmalls), listMax(Bigs,IsDefB,MBigs), listMax(Ls,IsDefL,MLs),
%   constr( Max = ite(MSmalls>MBigs,MSmalls,MBigs) ), % max(MSmalls,MBigs,Max),
%   partition(X,Ls,Smalls,Bigs).
%
%:- pred ff3.
%ff3 :-
%   constr( ~(((((   IsDefXs &  IsDefYs ) => (  IsDefZs & ( MaxZs=Max ) )) &
%                ((  IsDefXs & ~IsDefYs ) => (  IsDefZs & ( MaxZs=MaxXs ) ))) &
%                (( ~IsDefXs &  IsDefYs ) => (  IsDefZs & ( MaxZs=MaxYs ) ))) &
%                (( ~IsDefXs & ~IsDefYs ) =  ( ~IsDefZs ))
%              ) ),
%   listMax(Xs,IsDefXs,MaxXs), listMax(Ys,IsDefYs,MaxYs),
%   listMax(Zs,IsDefZs,MaxZs), 
%   constr( Max = ite(MaxXs>MaxYs,MaxXs,MaxYs) ),    % max(MaxXs,MaxYs,Max),
%   append(Xs,Ys,Zs).

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

:- cata_abs list(int) ==> listMax(Xs,IsDefXs,MaxXs).

% =================================================================