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


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


% ======================================================================
% Contracts.
% ---------
% Behaviour of listMin over append

:- spec append(Xs,Ys,Zs) ==>                                       
     listMin(Xs,BXs,NXs), listMin(Ys,BYs,NYs), listMin(Zs,BZs,NZs) =>
     constr((((((BXs & BYs)  => (BZs & NZs=ite(NXs<NYs,NXs,NYs))) &
               ((BXs & ~BYs) => (BZs & (NZs=NXs)) )) &
              ((~BXs & BYs ) => (BZs & (NZs=NYs) ) )) &
              ((~BXs & ~BYs) =  (~BZs) ))).

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

:- pred ff1.
ff1 :-
       constr(~(((((BXs & BYs)  => (BZs & NZs=ite(NXs<NYs,NXs,NYs))) &
                 ((BXs & ~BYs) => (BZs & (NZs=NXs)) )) &
                ((~BXs & BYs ) => (BZs & (NZs=NYs) ) )) &
                ((~BXs & ~BYs) =  (~BZs) )) ),
       listMin(Xs,BXs,NXs), listMin(Ys,BYs,NYs), listMin(Zs,BZs,NZs),
       constr(N=ite(NXs<NYs,NXs,NYs)),
       append(Xs,Ys,Zs).


% =================================================================
% NON-CATA predicates: append constr