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

% ====================================================
% Program. mergesorting in ascending order.E.g., 3 =< 5 =< 5 =< 8 =< ...
:- pred mergesort(list(int),list(int)).
:- mode mergesort(in,out).
mergesort([], []).
mergesort([H], [H,X]).  % error: [H,X] -> [H]
mergesort(HKT,S) :-
   length(HKT,N), N>=2,       
   split(HKT,L1,L2),       
   mergesort(L1,S1),       
   mergesort(L2,S2),
   merge(S1,S2,S).         % 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),     
     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).

:- pred merge(list(int),list(int),list(int)).
:- mode merge(in,in,out).
merge([],L,L).                         
merge(L,[],L).               
merge([X|Xs],[Y|Ys],[X|Zs]) :-        
   X=<Y, cons(Y,Ys,YYs),
   merge(Xs,YYs,Zs).              
merge([X|Xs],[Y|Ys],[Y|Zs]) :-
   X>Y, cons(X,Xs,XXs), 
   merge(XXs,Ys,Zs).
  
% ====================================================
% 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 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:
:- pred ff1.
ff1 :-                              % mergesort
   constr( ~(B)), 
   is_asorted(S,B),
   mergesort(L,S). 

%:- pred ff2.
%ff2 :-                              % merge
%      constr(~((BL1 & BL2) => BL12)),  
%      is_asorted(L1,BL1), is_asorted(L2,BL2), is_asorted(L12,BL12), 
%      merge(L1,L2,L12). 
%
%:- pred ff3.                        % cons 
%ff3 :-
%constr(~((IsDefHdXXs & HdXXs=X) & 
%         (IsDefHdXs => ((B2 & (X =< HdXs)) => B3)))), %
%hd(Xs,IsDefHdXs,HdXs), hd(XXs,IsDefHdXXs,HdXXs),   
%is_asorted(Xs,B2), is_asorted(XXs,B3), 
%cons(X,Xs,XXs).

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

%  Catamorphic abstraction

:- cata_abs list(int) ==> is_asorted(T,ResT).

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