% ====================================================
:- pred constr(bool). 
:- mode constr(in). 
:- ignore constr/1.

% ====================================================
% Program. mergesorting in descending order.E.g., 8 >= 5 >= 5 >= 3 >= ...
:- pred mergesort(list(int),list(int)).
:- mode mergesort(in,out).
mergesort([], []).
mergesort([H], [H]).
mergesort([H,K|T],S) :-
   cons(K,T,KT),    
   cons(H,KT,HKT),        
   split(HKT,L1,L2),       
   mergesort(L1,S1),       
   mergesort(L2,S2),
   dmerge(S1,S2,S).        %  descending merging
   

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

:- pred split(list(int),list(int),list(int)).
:- mode split(in,out,out).
split(L,L1,L2) :- N1=(N div 2),      % div is integer division (in SMTLIB). 
     length(L,N),                    
     takedrop(N1,L,L1,L2).

:- pred length(list(int),int).
:- mode length(in,out).
length([],L) :- L=0.
length([H|T],L) :-
  L=(LT+1),
  length(T,LT).

:- pred takedrop(int,list(int),list(int),list(int)).
:- mode takedrop(in,in,out,out).
takedrop(N,[],[],[]).
takedrop(N,L,[],L) :- N=<0. 
takedrop(N,[H|T],[H|T1],L) :- 
  N>=1, N1=(N-1),   
  takedrop(N1,T,T1,L).
                                       
% --- DECREASING merge: the result is a --weakly descending-- list
% dmerge([8,6,4],[7,5,3],[8,7,6,5,4,3])
:- pred dmerge(list(int),list(int),list(int)).
:- mode dmerge(in,in,out).

dmerge([],L,L).                         
dmerge([X|Xs],[],[X|Xs]).               
dmerge([X|Xs],[Y|Ys],[X|Zs]) :-          
     X>Y, cons(Y,Ys,YYs),               % [Y|Ys] = YYs
     dmerge(Xs,YYs,Zs).                 
dmerge([X|Xs],[Y|Ys],[Y|Zs]) :-
     X=<Y, cons(X,Xs,XXs),              % [X|Xs] = XXs
     dmerge(XXs,Ys,Zs).

% ====================================================
% catamorphisms
:- pred listmin(list(int),bool,int). 
:- mode listmin(in,out,out).  
:- cata listmin/3-1.
listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ). % Any int value, instead of 0, is ok. 
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).
:- mode listmax(in,out,out).
:- cata listmax/3-1.
listmax([],B,Res) :- constr( ((~B) & Res=0) ).   % Any int value, instead of 0, is ok.
listmax([H|T],B,Res) :-
       constr( B & ( Res=ite(BT, ite(H>ResT,H,ResT), H) ) ),
       listmax(T,BT,ResT).

%---
:- 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).
         
%--- weakly descending ordered
:- pred is_dsorted(list(int),bool). 
:- mode is_dsorted(in,out).  
:- cata is_dsorted/2-1.

is_dsorted([],Res) :- constr(Res).
is_dsorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    is_dsorted(T,ResT),
    constr(Res=(IsDefT => ((H>=HdT) & ResT))).
    
% ---
:- pred hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Hd) :- constr( (~IsDef) & (Hd=0) ).    % Any int value, instead of 0, is ok.
hd([H|T],IsDef,Hd) :- constr( IsDef & (Hd=H) ).
           
%=================================================================   
% verification. 
% Property of mergesort
:- pred ff1. 
ff1 :- 
     constr( ~((IsDefLMin = IsDefSLast) & 
     ((IsDefLMin & IsDefSLast) => (MinL=LastS)) )), 
     listmin(L,IsDefLMin,MinL),  
     lastElem(S,IsDefSLast,LastS), 
     mergesort(L,S).
            
% Property of split   % Xs = (Ys @ Zs)
:- pred ff2.
ff2 :- 
      constr(~(((((( IsDefYs &  IsDefZs )  => (  IsDefXs & ( MXs=ite(MYs<MZs,MYs,MZs) ) )) &
     ((  IsDefYs & ~IsDefZs )  => (  IsDefXs & ( MXs=MYs ) ))) &
     (( ~IsDefYs &  IsDefZs )  => (  IsDefXs & ( MXs=MZs ) ))) &
     (( ~IsDefYs & ~IsDefZs )  =  ( ~IsDefXs )))
    &   ((( IsDefZsLE    => (  IsDefXsLE & ( LastXs=LastZs ) )) &
        ((  IsDefYsLE & ~IsDefZsLE ) => (  IsDefXsLE & ( LastXs=LastYs ) ))) &
        (( ~IsDefYsLE & ~IsDefZsLE ) =  ( ~IsDefXsLE )))
        )),
      listmin(Xs,IsDefXs,MXs), listmin(Ys,IsDefYs,MYs), listmin(Zs,IsDefZs,MZs),
      lastElem(Xs,IsDefXsLE,LastXs), lastElem(Ys,IsDefYsLE,LastYs), lastElem(Zs,IsDefZsLE,LastZs), 
      split(Xs,Ys,Zs).

:- pred ff3.
ff3 :-                              % takedrop Ls = Ts @ Ds 
   constr( ~( (IsDefLTs & IsDefHdDs) => (LTs >= HdDs => (BLs = (BTs & BDs))) ) ),
   constr( ~( (IsDefLTs & ~IsDefHdDs) =>  (BLs = BTs) ) ),
   constr( ~( (~IsDefLTs & IsDefHdDs) =>  (BLs = BDs) ) ),
   constr( ~( (~(IsDefLTs & IsDefHdDs)) => ((BLs = BTs) v (BLs = BDs)))),
   is_dsorted(Ls,BLs), is_dsorted(Ts,BTs), is_dsorted(Ds,BDs),
   lastElem(Ts,IsDefLTs,LTs), hd(Ds,IsDefHdDs,HdDs),
   takedrop(N,Ls,Ts,Ds).

% Property of dmerge
:- pred ff4.
ff4 :-                              % dmerge
   constr( ~((BXs & BYs) => BZs)),
   listmin(Xs,IsDefMinXs,MinXs), listmin(Ys,IsDefMinYs,MinYs),  
   listmin(Zs,IsDefMinZs,MinZs),
   is_dsorted(Xs,BXs), is_dsorted(Ys,BYs), is_dsorted(Zs,BZs),
   dmerge(Xs,Ys,Zs).
    
% Property of cons
 :- pred ff5.                        % cons    [X|Xs]=Ys
ff5 :- constr(~(
               (~IsDefMaxXs => ((B3 & MinYs=X) & MaxYs=X)) & 
               ( IsDefMaxXs => ((B2 & X>=MaxXs) = B3))
               )),            
 listmin(Xs,IsDefMinXs,MinXs),  listmin(Ys,IsDefMinYs,MinYs),  
 listmax(Xs,IsDefMaxXs,MaxXs),  listmax(Ys,IsDefMaxYs,MaxYs),
 is_dsorted(Xs,B2), is_dsorted(Ys,B3), 
 cons(X,Xs,Ys). 
%=================================================================   
:- query ff1/0.
:- query ff2/0.
:- query ff3/0.
:- query ff4/0.
:- query ff5/0.
%=================================================================