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


%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( ~((((((((BNXs & BMYs) & BXs) & BYs) & N>=M) => BZs)  &
               (((BNXs & ~BMYs) & BXs) => (BYs & BZs))) &
               (((~BNXs & BMYs) & BYs) => (BXs & BZs))) &
               ((~BNXs & ~BMYs) => ((BXs & BYs) & BZs))) ),
       isDSorted(Xs,BXs), isDSorted(Ys,BYs), isDSorted(Zs,BZs),
       listMin(Xs,BNXs,N),  listMax(Ys,BMYs,M),
       append(Xs,Ys,Zs).

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