% ====================================================
% ogni atomo ha tutte variabili distinte nel body. Nella testa non necessariamente.
:- 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]).          % constructors to do like this.

:- 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) :- constr(L=0).
length([H|T],L) :-
  constr( 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) :- 
  constr((N>=1) & (N1=(N-1))),   % ok also without constr: they are atomic constraints 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([X|Xs],[],[X|Xs]).
merge([X|Xs],[Y|Ys],[X|Zs]) :-
     constr(X=<Y), cons(Y,Ys,YYs),
     merge(Xs,YYs,Zs).
merge([X|Xs],[Y|Ys],[Y|Zs]) :-
     constr(X>Y), cons(X,Xs,XXs),
     merge(XXs,Ys,Zs).

% ====================================================
% catamorphisms  
:- pred count(int,list(int),bool). 
:- mode count(in,in,out).  
:- cata count/3-2.
count(X,[],Res) :- constr( (Res=0) ).
count(X,[Y|Ys],Res) :- 
    constr( Res=ite(X=Y,ResT+1,ResT) ),   
    count(X,Ys,ResT).   

% ====================================================
% Contract on mergesort:
:- spec mergesort(L,S) ==>
        count(X,L,CL), count(X,S,CS) =>
        constr( CL=CS ).

% Contract on split:
:- spec split(Xs,Ys,Zs) ==>    % X is existentially quantified in the premise
        count(X,Xs,NXs), count(X,Ys,NYs), count(X,Zs,NZs)  =>
        constr( NXs = (NYs+NZs) ).

% Contract on takedrop:
:- spec takedrop(N,Ls,Ts,Ds) ==>               
        count(X,Ls,NLs), count(X,Ts,NTs), count(X,Ds,NDs) =>
        constr( NLs = (NTs+NDs)).

% Contract on merge:
:- spec merge(Xs,Ys,Zs) ==>
        count(X,Xs,NXs), count(X,Ys,NYs), count(X,Zs,NZs)  =>
        constr( NZs = (NXs+NYs) ).
        
% Contract on cons:
:- spec cons(H,T,HT) ==>
        count(X,T,NXT), count(X,HT,NXHT)  =>
        constr( NXHT = ite(X=H,(NXT+1), NXT) ).

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

:- pred ff2.
ff2 :-                              % split
   constr( ~(NXs = (NYs+NZs)) ),
   count(X,Xs,NXs), count(X,Ys,NYs), count(X,Zs,NZs),
   split(Xs,Ys,Zs).

:- pred ff3.
ff3 :-                              % merge
   constr( ~(NZs = (NXs+NYs)) ),
   count(X,Xs,NXs), count(X,Ys,NYs), count(X,Zs,NZs),
   merge(Xs,Ys,Zs).

:- pred ff4.
ff4 :-                              % takedrop
   constr( ~(NLs = (NTs+NDs))),
   count(X,Ls,NLs), count(X,Ts,NTs), count(X,Ds,NDs),
   takedrop(N,Ls,Ts,Ds). 
   
:- pred ff5.
ff5 :-                              % cons
    constr( ~(NXHT = ite((X=H),(NXT+1), NXT)) ),
    count(X,T,NXT), count(X,HT,NXHT),
    cons(H,T,HT).

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