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

:- 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,HA,R).

:- 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).
 
% ===========================================================
% contract on revacc
:- spec revacc(L,R) ==> 
        is_asorted(L,ABL), is_dsorted(R,DBR),
        is_dsorted(L,DBL), is_asorted(R,ABR) => 
        constr( (ABL=DBR) & (DBL=ABR) ).
        
%contract on reva
:- spec reva(L,A,R) ==> 
       is_empty(A,BA),
       is_asorted(L,ABL), is_dsorted(R,DBR),
       is_dsorted(L,DBL), is_asorted(R,ABR) => 
       constr( BA => ((ABL=DBR) & (DBL=ABR)) ). 

% contract on cons
:- spec cons(H,T,HT) ==>
        is_asorted(T,ABT), is_asorted(HT,ABHT),
        listMin(T,IsDefMinT,MinT), 
        is_dsorted(T,DBT), is_dsorted(HT,DBHT),
        listMax(T,IsDefMaxT,MaxT) => 
        constr((( (IsDefMinT=IsDefMaxT) &
               ((~IsDefMinT) => (((ABT & DBT) & ABHT) & DBHT))) & 
               ((IsDefMinT & (H=<MinT)) => (ABT=ABHT))) &
               ((IsDefMinT & (H>=MaxT)) => (DBT=DBHT))).
          
% ===========================================================
:- 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( ~( BA => ((ABL=DBR) & (DBL=ABR) )) ),
    is_empty(A,BA), 
    is_asorted(L,ABL), is_dsorted(R,DBR), is_dsorted(L,DBL), is_asorted(R,ABR),
    reva(L,[],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).

% ===========================================================
% NON-CATA predicates: cons constr reva revacc