% ====================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% =================================================================
% Program
:- pred append(list(int),list(int),list(int)).
:- mode append(in,in,out).

append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

% =================================================================
% Catamorphisms.
% -------------
% head of a list. For hd(List,B,Res) we have B=false iff List=[]
:- pred hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Res) :- constr( ((~IsDef) & Res=0)).
hd([H|T],IsDef,Res) :- constr( (IsDef & Res=H) ).

% all_leq(List,N,Res) Res iff all elements of List are =< N
:- pred all_leq(list(int),int,bool).
:- mode all_leq(in,in,out).
:- cata all_leq/3-1.

all_leq([],N,Res) :- constr( Res ).
all_leq([Y|Ys],N,Res) :- constr( Res=ite(Y=<N,ResYs,false) ), all_leq(Ys,N,ResYs).

% all_grt(List,N,Res) Res iff all elements of List are >= N
:- pred all_grt(list(int),int,bool).
:- mode all_grt(in,in,out).
:- cata all_grt/3-1.

all_grt([],N,Res) :- constr( Res ).
all_grt([Y|Ys],N,Res) :- constr( Res=ite(Y>=N,ResYs,false) ), all_grt(Ys,N,ResYs).

% Res=true iff L is weakly-ascending-sorted:  e.g., 1=<2=<3=<...
:- pred isASorted(list(int),bool).
:- mode isASorted(in,out).
:- cata isASorted/2-1.

isASorted([],Res) :- constr( Res ).
isASorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    isASorted(T,ResT),
    constr(Res = (IsDefT => (H=<HdT & ResT))).

% Res=true iff L is weakly-descending-sorted: e.g., 9>=8>=7>=...
:- pred isDSorted(list(int),bool).
:- mode isDSorted(in,out).
:- cata isDSorted/2-1.

isDSorted([],Res) :- constr( Res ). 
isDSorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    isDSorted(T,ResT),
    constr(Res = (IsDefT => (H>=HdT & ResT))).

% =================================================================
% ------ Verification of contract on append:

:- pred ff1.
ff1 :-
  	 constr( ~(((((B01 & B02) => B03)  &                         % --- (1)
                 ((B11 & B12) => B13)) &												 % --- (2)
                 ((B21 & B22) => ((BXs2 & BYs2) = BZs2))) &      % --- (3)
                 ((B31 & B32) => ((BXs3 & BYs3) = BZs3)))        % --- (4)
							 ),

		 all_leq(Xs,K,B01), all_leq(Ys,K,B02), all_leq(Zs,K,B03),    % --- (1)
		 %
		 all_grt(Xs,K1,B11), all_grt(Ys,K1,B12), all_grt(Zs,K1,B13), % --- (2)
		 %
		 isASorted(Xs,BXs2), isASorted(Ys,BYs2), isASorted(Zs,BZs2), % --- (3)
		 all_leq(Xs,K2,B21), all_grt(Ys,K2,B22),
		 %
		 isDSorted(Xs,BXs3), isDSorted(Ys,BYs3), isDSorted(Zs,BZs3), % --- (4)
		 all_grt(Xs,K3,B31), all_leq(Ys,K3,B32),
		 append(Xs,Ys,Zs).

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

%  Catamorphic abstraction

:- cata_abs list(int) ==> isDSorted(Xs,BYs), isDSorted(Xs,BXs2),
                          all_grt(Xs,K,B1), all_leq(Xs,K,B2).

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