% =================================================================
:- 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,[],R).  
revacc(L,R) :- reva(L,EL,R), emptylist(EL).

:- pred reva(list(int),list(int),list(int)).  % reva([1,2], [7,9,8], F).  F=[2,1,  7,9,8].
:- 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). 

%:- pred is_empty(list(int),bool).
%:- mode is_empty(in,out).
%:- cata is_empty/2-1.
%
%is_empty([],Res) :- constr(Res).
%is_empty([H|T],Res) :- constr(~Res).
 
% ---
% 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))).

% ---
:- pred listMin(list(int),bool,int).     
:- mode listMin(in,out,out).   
:- cata listMin/3-1.
listMin([],IsDef,A) :- constr( (~IsDef) & (A=0) ). % 0 can be any int.
listMin([H|T],IsDef,Min) :-
         constr( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H )) ),
         listMin(T,IsDefT,MinT).

% ---
:- pred listMax(list(int),bool,int).     
:- mode listMax(in,out,out).            
:- cata listMax/3-1.

listMax([],IsDef,A) :- constr( (~IsDef) & (A=0) ). % 0 can be any int.
listMax([H|T],IsDef,Max) :-
         constr( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H )) ),
         listMax(T,IsDefT,MaxT).
 
% ===========================================================

:- 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 & (IsDefMinL & (IsDefMaxA & (MinL>=MaxA))))) => DBR) 
%     & ((DBL & (ABA & (IsDefMaxL & (IsDefMinA & (MaxL=<MinA))))) => ABR)) ),
%     listMin(L,IsDefMinL,MinL), listMax(A,IsDefMaxA,MaxA),  %
%     listMax(L,IsDefMaxL,MaxL), listMin(A,IsDefMinA,MinA),  %
%     is_asorted(L,ABL), is_dsorted(A,DBA), is_dsorted(R,DBR),
%     is_dsorted(L,DBL), is_asorted(A,ABA), is_asorted(R,ABR),
%     reva(L,A,R).
%
%:- pred ff3.
%ff3 :- 
%    constr(~((( (IsDefMinT=IsDefMaxT) &
%               ((~IsDefMinT) => (((ABT & DBT) & ABHT) & DBHT))) & 
%               ((IsDefMinT & (H=<MinT)) => (ABT=ABHT))) &
%               ((IsDefMinT & (H>=MaxT)) => (DBT=DBHT)))
%             ),
%        is_asorted(T,ABT), is_asorted(HT,ABHT),
%        listMin(T,IsDefMinT,MinT), 
%        is_dsorted(T,DBT), is_dsorted(HT,DBHT),
%        listMax(T,IsDefMaxT,MaxT),
%    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), listMin(L,IsDef,Min), listMax(L,IsDefMaxT,MaxT).

% =================================================================s