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

% ====================================================
% catamorphism
:- pred listMax(list(int),bool,int).     
:- mode listMax(in,out,out).             
:- cata listMax/3-1.

listMax([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listMax([H|T],IsDef,Max) :-
         constr( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H )) ),
         listMax(T,IsDefT,MaxT).

% ================================================================= 
% Contract on mergesort:
:- spec mergesort(L,S)
         ==> listMax(L,IsDefMaxL,MaxL), listMax(S,IsDefMaxS,MaxS)  
             => constr( ((IsDefMaxL = IsDefMaxS) & (IsDefMaxS => (MaxL=MaxS))) & 
                ((~IsDefMaxS) => true) ).

% Contract on split:
:- spec split(Xs,Ys,Zs)   
        ==>  
            listMax(Xs,IsDefXs,MXs), listMax(Ys,IsDefYs,MYs), listMax(Zs,IsDefZs,MZs),
            constr( Max = ite(MYs>MZs,MYs,MZs) )  
            => 
            constr( 
                (((( IsDefYs &  IsDefZs )  => (  IsDefXs & ( MXs=Max ) )) &
                 ((  IsDefYs & ~IsDefZs )  => (  IsDefXs & ( MXs=MYs ) ))) &
                 (( ~IsDefYs &  IsDefZs )  => (  IsDefXs & ( MXs=MZs ) ))) &
                 (( ~IsDefYs & ~IsDefZs )  =  ( ~IsDefXs ))
                  ).

% Contract on takedrop:
:- spec takedrop(N,Ls,Ts,Ds) 
        ==> listMax(Ls,IsDefLs,MLs), listMax(Ts,IsDefTs,MTs), listMax(Ds,IsDefDs,MDs),
            constr( Max = ite(MTs>MDs,MTs,MDs) )
            =>
            constr( 
                 (((( IsDefTs &  IsDefDs )  => (  IsDefLs & ( MLs=Max ) )) &
                 ((   IsDefTs & ~IsDefDs )  => (  IsDefLs & ( MLs=MTs ) ))) &
                 ((  ~IsDefTs &  IsDefDs )  => (  IsDefLs & ( MLs=MDs ) ))) &
                 ((  ~IsDefTs & ~IsDefDs )  =  ( ~IsDefLs ))
                  ).
     
% Contract on merge:
:- spec merge(Xs,Ys,Zs) 
         ==> listMax(Xs,IsDefXs,MaxXs), listMax(Ys,IsDefYs,MaxYs),
             listMax(Zs,IsDefZs,MaxZs), 
             constr( Max = ite(MaxXs>MaxYs,MaxXs,MaxYs) )  
             =>
             constr( (((( IsDefXs &  IsDefYs )  => (  IsDefZs & ( MaxZs=Max ) )) &
                     ((   IsDefXs & ~IsDefYs )  => (  IsDefZs & ( MaxZs=MaxXs ) ))) &
                     ((  ~IsDefXs &  IsDefYs )  => (  IsDefZs & ( MaxZs=MaxYs ) ))) &
                     ((  ~IsDefXs & ~IsDefYs )  =  ( ~IsDefZs & ( MaxZs=0 ) ))
               ).

% Contract on cons:
:- spec cons(H,T,HT) ==>
      listMax(T,IsDefMaxT,MaxT), listMax(HT,IsDefMaxHT,MaxHT) =>
      constr(~( MaxHT = ite(IsDefMaxT,ite(H>MaxT,H,MaxT),H))).
% ================================================================= 
% verification. 
% Property:
:- pred ff1.
ff1 :-
   constr(~( ((IsDefMaxL = IsDefMaxS) & (IsDefMaxS => (MaxL=MaxS))) & 
     ((~IsDefMaxS) => true) )),
   listMax(L,IsDefMaxL,MaxL), listMax(S,IsDefMaxS,MaxS),
   mergesort(L,S).


:- pred ff2.
ff2 :- 
   constr( ~((((( IsDefYs &  IsDefZs )  => (  IsDefXs & ( MXs=Max ) )) &
            ((    IsDefYs & ~IsDefZs )  => (  IsDefXs & ( MXs=MYs ) ))) &
            ((   ~IsDefYs &  IsDefZs )  => (  IsDefXs & ( MXs=MZs ) ))) &
            ((   ~IsDefYs & ~IsDefZs )  =  ( ~IsDefXs ))
          )),
    listMax(Xs,IsDefXs,MXs), listMax(Ys,IsDefYs,MYs), listMax(Zs,IsDefZs,MZs),
    constr( Max = ite(MYs>MZs,MYs,MZs) ), 
    split(Xs,Ys,Zs).

:- pred ff3.
ff3 :- 
   constr( ~((((( IsDefYs &  IsDefZs )  => (  IsDefXs & ( MXs=Max ) )) &
            ((    IsDefYs & ~IsDefZs )  => (  IsDefXs & ( MXs=MYs ) ))) &
            ((   ~IsDefYs &  IsDefZs )  => (  IsDefXs & ( MXs=MZs ) ))) &
            ((   ~IsDefYs & ~IsDefZs )  =  ( ~IsDefXs ))
          )),
    listMax(Xs,IsDefXs,MXs), listMax(Ys,IsDefYs,MYs), listMax(Zs,IsDefZs,MZs),
    constr( Max = ite(MYs>MZs,MYs,MZs) ), 
    constr( N1=(N div 2) ), length(Xs,N),
    takedrop(N1,Xs,Ys,Zs).

:- pred ff4.
ff4 :- 
   constr( ~(((((   IsDefXs &  IsDefYs ) => (  IsDefZs & ( MaxZs=Max ) )) &
                ((  IsDefXs & ~IsDefYs ) => (  IsDefZs & ( MaxZs=MaxXs ) ))) &
                (( ~IsDefXs &  IsDefYs ) => (  IsDefZs & ( MaxZs=MaxYs ) ))) &
                (( ~IsDefXs & ~IsDefYs ) =  ( ~IsDefZs & ( MaxZs=0 ) ))
              ) ),
   listMax(Xs,IsDefXs,MaxXs), listMax(Ys,IsDefYs,MaxYs), listMax(Zs,IsDefZs,MaxZs),
   constr(Max = ite(MaxXs>MaxYs,MaxXs,MaxYs)),
   merge(Xs,Ys,Zs).

:- pred ff5.
ff5 :- 
   constr(~( MaxHT = ite(IsDefMaxT,ite(H>MaxT,H,MaxT),H))),
   listMax(T,IsDefMaxT,MaxT), listMax(HT,IsDefMaxHT,MaxHT), 
   cons(H,T,HT).

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