% ====================================================
% 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], []).  % error: [] -> [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) :-constr(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 w/o constr(...): it is a constraint in LIA+Bool
  takedrop(N1,T,T1,L).

:- pred merge(list(int),list(int),list(int)).
:- mode merge(in,in,out).
merge([],L,L).                  % non-linearity on head is ok
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).
     
% ====================================================
% catamorphism
% 
:- pred lengthcata(list(int),int).
:- mode lengthcata(in,out).
:- cata lengthcata/2-1.

lengthcata([],L) :- L=0.
lengthcata([H|T],L) :-
  L=(LT+1),
  lengthcata(T,LT). 
  
% ====================================================
  
% Contract on mergesort:
:- spec mergesort(L,S)
         ==> lengthcata(L,CL), lengthcata(S,CS) 
             => constr( CL=CS ). 
             
%% Contract on length:
%:- spec length(L,N) 
%        ==> lengthcata(L,N1)
%         => N=N1.
%         
%:- spec merge(A,C,E) ==> 
%          lengthcata(A,B), lengthcata(C,D), lengthcata(E,F) => true.
%          
%:- spec split(A,C,E) ==> lengthcata(A,B), lengthcata(C,D), lengthcata(E,F) => true.
%
%:- spec takedrop(G,C,E,A) ==> lengthcata(A,B), lengthcata(E,F), lengthcata(C,D)
%         => true.
%         
%:- spec cons(E,C,A) ==> lengthcata(A,B), lengthcata(C,D) => true.
% -------------------------------------
% verification. 
% Property:
:- pred ff1.
ff1 :-                               % mergesort
   constr( ~(CL=CS)), 
   lengthcata(L,CL), lengthcata(S,CS),  
   mergesort(L,S).

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

:- cata_abs list(int) ==>  lengthcata(A,B).

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