% =================================================================
:- 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,HB,R).   %error: HB --> HA 
   
:- pred emptylist(list(int)).
:- mode emptylist(in).
emptylist([]). 

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

% Catamorphic Abstraction

:- cata_abs list(int) ==> is_asorted(L,B1), is_dsorted(L,B2).

% =================================================================