% ====================================================
:- 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]).
mergesort([H,K|T],S) :-
   cons(K,T,KT),          
   cons(H,KT,HKT),          
   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) :- constr(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([X|Xs],[],[X|Xs]).
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 listcount(int,list(int),int). 
:- mode listcount(in,in,out).  
:- cata listcount/3-2.
listcount(X,[],Res) :- constr( (Res=0) ).
listcount(X,[Y|Ys],Res) :- 
    constr( Res=ite(X=Y,ResT+1,ResT) ),   
    listcount(X,Ys,ResT).   

  
% ====================================================
% verification. 
% Property:
:- pred ff1.
ff1 :-                              % mergesort
   constr( ~(CL=CS)), 
   listcount(X,L,CL), listcount(X,S,CS),  
   mergesort(L,S).

%% contracts (postcondition: true)
%
%:- spec merge(A,C,E) ==> listcount(X,A,B), listcount(X,C,D), listcount(X,E,F).
%
%:- spec split(E,A,C) ==> listcount(X,E,SE), listcount(X,A,SA), listcount(X,C,SC).
%
%:- spec cons(C,A,D) ==> listcount(X,A,SA), listcount(X,D,SD).
%
%:- spec takedrop(G,A,E,C) ==> listcount(X,A,B), listcount(X,E,F), listcount(X,C,D).

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

:- cata_abs list(int) ==> listcount(X,L,LB).

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