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

% listMin(List,B,Res):  if B then Res is the minimum element of List
:- pred listMin(list(int),bool,int).
:- mode listMin(in,out,out).
:- cata listMin/3-1.

listMin([],B,Res) :- constr( ((~B) & Res=0) ).
listMin([H|T],B,Res) :-
          constr( B & ( Res=ite(BT, ite(H<ResT,H,ResT), H) ) ),
          listMin(T,BT,ResT).

% listMax(List,B,Res):  if B then Res is the maximun element of List
:- pred listMax(list(int),bool,int).
:- mode listMax(in,out,out).
:- cata listMax/3-1.

listMax([],B,Res) :- constr( ((~B) & Res=0) ).
listMax([H|T],B,Res) :-
        constr( B & ( Res=ite(BT, ite(H>ResT,H,ResT), H) ) ),
        listMax(T,BT,ResT).

% isASorted: list sorted on weak-ascending order  
:- 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( ~(((( (((((BMXs & BNYs) & BXs) & BYs) & M=<N) => BZs )) &
           ( (((BMXs & ~BNYs) & BXs) => (BYs & BZs)) )) &
           ( (((~BMXs & BNYs) & BYs) => (BXs & BZs)) )) &
           ( ((~BMXs & ~BNYs) => ((BXs & BYs) & BZs)) ))),
       isASorted(Xs,BXs), isASorted(Ys,BYs), isASorted(Zs,BZs),
       listMax(Xs,BMXs,M),  listMin(Ys,BNYs,N),
       append(Xs,Ys,Zs).

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