% ====================================================
:- 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([], [X]). %error: [X] ---> []
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). 
     listlength(L,N),                    
     takedrop(N1,L,L1,L2).

:- pred listlength(list(int),int).
:- mode listlength(in,out).
listlength([],L) :- L=0.
listlength([H|T],L) :-
  L=(LT+1),
  listlength(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 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).
    
%=================================================================   
% verification. 
% Property of mergesort
% Property:
:- pred ff1.
ff1 :-                               
    constr( ~((IsDefLMin = IsDefSLast) & 
    ((IsDefLMin & IsDefSLast) => (MinL=LastS)) )), 
    listmin(L,IsDefLMin,MinL),  
    listmin(S,IsDefSMin,MinS), 
    lastElem(L,IsDefLLast,LastL),  
    lastElem(S,IsDefSLast,LastS), 
    mergesort(L,S).
    
% contracts (postcondition: true)

:- spec dmerge(A,C,E) ==> listmin(A,B1,B), listmin(C,B2,D), listmin(E,B3,F),
         lastElem(A,B4,LEA), lastElem(C,B5,LEC), lastElem(E,B6,LEE)
         => constr(true).

:- spec split(E,A,C) ==> listmin(E,B1,SE), listmin(A,B2,SA), listmin(C,B3,SC),
         lastElem(E,B4,LEE), lastElem(A,B5,LEA), lastElem(C,B6,LEC)
         => constr(true).
         
:- spec listlength(L,N) ==> listmin(L,B1,ML), lastElem(L,B2,LEL)
         => constr(true).

:- spec cons(C,A,D) ==> listmin(A,B1,MA), listmin(D,B2,MD),
         lastElem(A,B4,LEA), lastElem(D,B5,LED) => constr(true).

:- spec takedrop(G,A,E,C) ==> listmin(A,B1,B), listmin(E,B2,F), listmin(C,B3,D),
         lastElem(A,B4,LEA), lastElem(E,B6,LEE), lastElem(C,B5,LEC)
         => constr(true).

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