% ====================================================
:- 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),         % Every atom in the body has all distint variables 
   split(HKT,L1,L2),       % and no ADTs.  This may not hold for the head atom.
   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),      % integer division is div 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)),   % ok senza constr: sono constraint atomici in LIA+Bool
  takedrop(N1,T,T1,L).

:- pred merge(list(int),list(int),list(int)).
:- mode merge(in,in,out).
merge([],L,L).                    % ok non linearity on head
%merge(L,[],L).                   % ok non linearity on head. clause not needed.
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).

% ====================================================
% catamorphism
:- pred sum(list(int),int).
:- mode sum(in,out).
:- cata sum/2-1.

sum([],S) :- S=0.
sum([H|T],S) :-
  S=(H+ST),
  sum(T,ST).

% ================================================================= 
% Contract on mergesort:
:- spec mergesort(L,S)
    ==> sum(L,SL), sum(S,SS) 
        => constr(SL=SS).

% Contract on split:
:- spec split(Xs,Ys,Zs)   
        ==> sum(Xs,SXs), sum(Ys,SYs), sum(Zs,SZs)
            => constr( SXs = (SYs+SZs) ).

% Contract on takedrop:
:- spec takedrop(N,Ls,Ts,Ds) 
        ==> sum(Ls,SLs), sum(Ts,STs), sum(Ds,SDs)
            => constr( SLs = (STs+SDs) ).
     
% Contract on merge:
:- spec merge(Xs,Ys,Zs) 
      ==> sum(Xs,SXs),  sum(Ys,SYs), sum(Zs,SZs)  
          => constr( SZs = (SXs+SYs) ).

% Contract on cons:
:- spec cons(H,T,HT) ==>
        sum(T,ST), sum(HT,SHT)  =>
        constr( SHT = (ST+H)).
% ================================================================= 
% verification. 
% Property:

:- pred ff1.
ff1 :-
   constr( ~(SL = SS)), 
   sum(L,SL), sum(S,SS),
   mergesort(L,S).

:- pred ff2.
ff2 :- 
    constr( ~(SXs = (SYs+SZs)) ),
    sum(Xs,SXs), sum(Ys,SYs), sum(Zs,SZs),
    split(Xs,Ys,Zs).

:- pred ff3.
ff3 :- 
    constr( ~(SXs = (SYs+SZs)) ),
    sum(Xs,SXs), sum(Ys,SYs), sum(Zs,SZs),
    constr( N1=(N div 2) ), length(Xs,N),
    takedrop(N1,Xs,Ys,Zs).

:- pred ff4.
ff4 :- 
   constr( ~(SZs = (SXs+SYs)) ), 
   sum(Xs,SXs),  sum(Ys,SYs), sum(Zs,SZs), 
   merge(Xs,Ys,Zs).

:- pred ff5.
ff5 :- 
   constr(~( SHT = (ST+H))),
   sum(T,ST), sum(HT,SHT), 
   cons(H,T,HT).

% ================================================================= 
% NON-CATA predicates: cons constr length merge mergesort split takedrop