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

% =================================================================
%Program
:- pred revacc(list(int),list(int)).  
:- mode revacc(in,out).            
                                     
revacc(L,R) :- reva(L,EL,R), emptylist(EL). 

:- pred reva(list(int),list(int),list(int)).  % reva([11,12], [9,7,5], F).  F=[12,11,  9,7,5].
:- mode reva(in,in,out).            % the accumulator remains "as is" at the right end
                                    % of the reversed list.
reva([],A,A).
reva([H|T],A,R) :- 
   cons(H,A,HA),
   reva(T,HA,R).
   
:- pred emptylist(list(int)).
:- mode emptylist(in).
emptylist(Y).  % error: Y -> []

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).
cons(H,T,[H|T]).          

% ===========================================================
%Catamorphisms
:- 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). 
 
% ---
% is_asorted(L,Res): 
% Res=true iff L is weakly-ascending-sorted: e.g., 3 =< 5 =< 8 =<...
:- pred is_asorted(list(int),bool).
:- mode is_asorted(in,out).
:- cata is_asorted/2-1.

is_asorted([],Res) :- constr(Res).  
is_asorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    is_asorted(T,ResT),
    constr(Res=(IsDefT => ((H=<HdT) & ResT))).

% ---
% is_dsorted(L,Res): 
% Res=true iff L is weakly-descending-sorted: e.g., 9 >= 8 >= 7 >=...
:- pred is_dsorted(list(int),bool).
:- mode is_dsorted(in,out).
:- cata is_dsorted/2-1.

is_dsorted([],Res) :- constr(Res).
is_dsorted([H|T],Res) :-
    hd(T,IsDefT,HdT), 
    is_dsorted(T,ResT),
    constr(Res = (IsDefT => ((H>=HdT) & ResT))).
    
% ===========================================================
% Contracts
% Queries
:- pred ff1.
ff1 :-  
     constr( ~((ABL=DBR) & (DBL=ABR))),
     is_asorted(L,ABL), is_dsorted(R,DBR),
     is_dsorted(L,DBL), is_asorted(R,ABR),
     revacc(L,R).

:- pred ff2.
ff2 :- 
     constr( ~(((ABL & (DBA & (NotEmptyL & (NotEmptyA & (HdL>=HdA))))) => DBR) 
     & (((DBL & (ABA & (NotEmptyL & (NotEmptyA & (HdL=<HdA))))) => ABR))) ),
     is_asorted(L,ABL), is_dsorted(A,DBA), is_dsorted(R,DBR),
     is_dsorted(L,DBL), is_asorted(A,ABA), is_asorted(R,ABR),
     hd(A,NotEmptyA,HdA), hd(L,NotEmptyL,HdL), 
     reva(L,A,R). 

:- pred ff3.
ff3 :-  
      constr( ~(((DBT & (NotEmptyT & (H>=HdT))) => DBHT) &
      ((ABT & (NotEmptyT & (H=<HdT))) => ABHT)) ), 
      is_dsorted(T,DBT), is_dsorted(HT,DBHT),
      is_asorted(T,ABT), is_asorted(HT,ABHT),
      hd(T,NotEmptyT,HdT),
      cons(H,T,HT).
% ===========================================================
:- query ff1/0.
:- query ff2/0.
:- query ff3/0.
% ===========================================================