% ====================================================
:- 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(A,Ys,Zs). %error: A --> Xs

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

% isASorted(L,Res): 
% 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))).

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

:- pred ff1.
ff1 :-                                                
  constr( ~((B1 & B2) => ((BXs & BYs) = BZs)) ),    
  isASorted(Xs,BXs), isASorted(Ys,BYs), isASorted(Zs,BZs),
  all_leq(Xs,K,B1), all_grt(Ys,K,B2),
  append(Xs,Ys,Zs).

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

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

%  Catamorphic abstraction

:- cata_abs list(int) ==> isASorted(Ys,BYs), all_leq(Ys,K,B1), 
                          all_grt(Ys,K,B2).

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