% ====================================================
:- 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) :- 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: they are atomic constraints in LIA+Bool. 
  takedrop(N1,T,T1,L).  % No need for: constr(N>=1), instead of N>=1.

:- pred merge(list(int),list(int),list(int)).
:- mode merge(in,in,out).
merge([],L,L).                   % The non-linearity on head is ok.
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 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 grt_all(int,list(int),bool).
:- mode grt_all(in,in,out).
:- cata grt_all/3-2.
grt_all(N,[],B) :- constr(B).       
grt_all(N,[X|Xs],B) :-              %
	grt_all(N,Xs,B1),                 % N is greater ( > ) of all elements of list [X|Xs]
	constr(B = ((N>X) & B1)).

%----
:- pred leq_all(int,list(int),bool).
:- mode leq_all(in,in,out).
:- cata leq_all/3-2.
leq_all(N,[],B) :- constr(B).       %
leq_all(N,[Y|Ys],B) :-              % N is leq ( =< ) of all elements of list [Y|Ys]
	leq_all(N,Ys,B1),
	constr(B = ((N=<Y) & B1)).

%----
:- 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) ).


% ---
:- pred listmin(list(int),bool,int).    
:- mode listmin(in,out,out).
:- cata listmin/3-1.
listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).  % A can be any int.
listmin([H|T],IsDef,Min) :-
         constr( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H)) ),
         listmin(T,IsDefT,MinT).

% ====================================================
% Contract on quicksort:  (ascending order)
:- spec mergesort(L,S)
	 ==> is_asorted(S,B)
	    => constr(B).

% Contract on split:
:- spec split(Xs,Ys,Zs) ==>               % Xs = Ys @ Zs
        is_asorted(Xs,BXs), is_asorted(Ys,BYs), is_asorted(Zs,BZs),
        grt_all(N,Ys,SmallYs),  leq_all(N,Zs,BigZs) =>
        constr( (SmallYs & BigZs) => (BXs = (BYs & BZs)) ).

% Contract on takedrop:
:- spec takedrop(N,Ls,Ts,Ds) ==>
        is_asorted(Ls,BLs), is_asorted(Ts,BTs), is_asorted(Ds,BDs),
        grt_all(M,Ts,SmallTs),  leq_all(M,Ds,BigDs) =>
        constr( (SmallTs & BigDs) => (BLs = (BTs & BDs)) ).
        
% Contract on merge:
:- spec merge(Xs,Ys,Zs) ==>
        listmin(Xs,IsDefMinXs,MinXs), listmin(Ys,IsDefMinYs,MinYs), % no cata for Zs                              %
        hd(Xs,IsDefHXs,HXs), hd(Ys,IsDefHYs,HYs),                   % no cata for Zs
        is_asorted(Xs,BXs), is_asorted(Ys,BYs), is_asorted(Zs,BZs)
        =>
        constr( (BXs & BYs) => BZs).
         
% Contract on cons:
:- spec cons(X,Xs,Ys)    ==>        %   Ys=[X|Xs]            % Catas needed
	listmin(Xs,IsDefMinXs,MinXs), listmin(Ys,IsDefMinYs,MinYs),   
	is_asorted(Xs,B2), is_asorted(Ys,B3)
      => constr(((~IsDefMinXs => (B3 & MinYs=X)) & 
                (B3 => (MinYs=X))) &
                ((B2 & (X=<MinXs)) => B3)).

% Contract on cons (Version2):    % Not sufficient    
%:- spec cons(H,T,HT) ==>
%        is_asorted(T,BT),  is_asorted(HT,BHT), hd(T,IsDef,K) =>
%        constr( IsDef => (BHT = (BT & H=<K)) ).

% =================================================================
% verification. 
% Property:
:- pred ff1.
ff1 :-                              % mergesort
   constr( ~(B)), 
   is_asorted(S,B),
   mergesort(L,S).

:- pred ff2.
ff2 :-                              % split
   constr( ~((SmallYs & BigZs) => (BXs = (BYs & BZs))) ),
   is_asorted(Xs,BXs), is_asorted(Ys,BYs), is_asorted(Zs,BZs),
   grt_all(N,Ys,SmallYs),  leq_all(N,Zs,BigZs),
   split(Xs,Ys,Zs).

:- pred ff3.
ff3 :-                              % takedrop
   constr( ~((SmallTs & BigDs) => (BLs = (BTs & BDs))) ),
   is_asorted(Ls,BLs), is_asorted(Ts,BTs), is_asorted(Ds,BDs),
   grt_all(M,Ts,SmallTs),  leq_all(M,Ds,BigDs),
   takedrop(N,Ls,Ts,Ds).
   
:- pred ff4.
ff4 :-                              % merge
   constr( ~((BXs & BYs) => BZs)),
   listmin(Xs,IsDefMinXs,MinXs), listmin(Ys,IsDefMinYs,MinYs),  % no cata for Zs
   hd(Xs,IsDefHXs,HXs), hd(Ys,IsDefHYs,HYs),                    % no cata for Zs
   is_asorted(Xs,BXs), is_asorted(Ys,BYs), is_asorted(Zs,BZs),
   merge(Xs,Ys,Zs).

:- pred ff5.                        % cons
ff5 :- constr(~(((~IsDefMinXs => (B3 & MinYs=X)) & 
                (B3 => (MinYs=X))) &
                ((B2 & (X=<MinXs)) => B3))),
  listmin(Xs,IsDefMinXs,MinXs), listmin(Ys,IsDefMinYs,MinYs),
	is_asorted(Xs,B2), is_asorted(Ys,B3), 
  cons(X,Xs,Ys).

% More ffn's for variants of contracts which are not sufficient
%:- pred ff4.
%ff4 :-                              % merge
%   constr( ~((BXs & BYs) => BZs)),
%   is_asorted(Xs,BXs), is_asorted(Ys,BYs), is_asorted(Zs,BZs),
%   merge(Xs,Ys,Zs).
%   
%:- pred ff5. 
%ff5 :-                              % cons. Verified.
%    constr( ~( (BL1=>BL2) & ((BT & BL1) => BHT) ) ),
%    is_asorted(T,BT),  is_asorted(HT,BHT), leq_all(H,T,BL1), leq_all(H,HT,BL2),
%    cons(H,T,HT).
%
%:- pred ff51. 
%ff51 :-                         % cons Version2. Verified.
%   constr( ~(IsDef => ( BHT = (BT & H=<K))) ),
%   is_asorted(T,BT), is_asorted(HT,BHT), hd(T,IsDef,K),
%   cons(H,T,HT).

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