% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% =================================================================
% Program

% rev(L,R):
% list R is the reversal of list L
:- pred rev(list(int),list(int)).
:- mode rev(in,out).

rev([],[X,Y]) :- constr(X<Y).
rev([H|T],R) :-  % Error
 rev(T,S),
 snoc(S,H,R).

% snoc(L,X,S):
% list S is obtained by adding element X at the end of list L
:- pred snoc(list(int),int,list(int)).
:- mode snoc(in,in,out).

snoc([],X,[X]).
snoc([X|Xs],Y,[X|Zs]) :-
  snoc(Xs,Y,Zs).


% =================================================================
% Catamorphisms

% ------ hd(L,IsDef,Hd): IsDef is true iff L is a nonempty list and
% if IsDef=true then Hd is the head of L
:- pred hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Hd) :- constr(~IsDef & (Hd=0)).   % 0 can be any int.
hd([H|T],IsDef,Hd) :- constr(IsDef & (Hd=H)).

% ------ isASorted(L,Res):
% Res= true iff L is weakly-ascending.
:- 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))).

% ------ isDSorted(L,Res):
% Res= true iff L is weakly-descending.
:- 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))).

% ------ listMin(L,IsDef,Min):  IsDef=true iff L is a nonempty list and
%    if IsDef then Min is the minimum element on the list L
:- pred listMin(list(int),bool,int).
:- mode listMin(in,out,out).
:- cata listMin/3-1.

listMin([],IsDef,Min) :- constr( ~IsDef & Min=0 ).   % 0 can be any int.
listMin([H|T],IsDef,Min) :-
     listMin(T,IsDefT,MinT),
     constr( (IsDef & (Min = ite(IsDefT, ite(H<MinT, H ,MinT), H ) ) ) ).  

% ------ leq_all(N,L,B):    B=true  iff forall element X of L,  N=<X.
:- pred leq_all(int,list(int),bool).
:- mode leq_all(in,in,out).
:- cata leq_all/3-2.

leq_all(N,[],B) :-
  constr( B ).
leq_all(N,[X|Xs],B) :-
  constr( B = (N=<X & B1) ),
  leq_all(N,Xs,B1).

% =================================================================
% ------ Verification of contract on rev:
% If list R is the reverse of list L then 
% L is weakly-ascending iff R is weakly-descending    
% weakly-ascending sequence:  1=<2=<3=<...
% weakly-descending sequence: 9>=8>=7>=...                
:- pred ff1.
ff1 :-
  constr( ~(BL=>BR) ),
  isASorted(L,BL),
  rev(L,R),
  isDSorted(R,BR).

% ------ Verification of contract on snoc:
:- pred ff2.
ff2 :-                                                 
  constr( ~((BA & BE) => BC) ),
  isDSorted(A,BA),
  leq_all(X,A,BE),
  snoc(A,X,C),
  isDSorted(C,BC).
  
% ==========================================================
:- query ff1/0.
:- query ff2/0.
% ==========================================================