% =================================================================
:- pred constr(bool).    
:- mode constr(in).
:- ignore constr/1.
% ===========================================================
% Program
:- pred rev(list(int),list(int)).
:- mode rev(in,out).

rev([X],[]).     % rev([X],[]). ---> rev([],[]).
rev([H|T],R) :-
  rev(T,S),
  snoc(S,H,R).

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

% ===========================================================
% verification. 
:- pred ff1.
ff1 :-
  constr( ~((((IsDefLmin=IsDefRmin) & (IsDefLmin=IsDefLmax)) & 
                  (IsDefLmax=IsDefRmax)) &
           (IsDefLmin => ((N1=N2) & (M1=M2))))),     
  listMin(L,IsDefLmin,N1), listMax(L,IsDefLmax,M1),
	rev(L,R),
  listMin(R,IsDefRmin,N2), listMax(R,IsDefRmax,M2).

%:- pred ff2.
%ff2 :-
%      constr(~( ((((IsDefAmin=IsDefAmax) &
%                    (IsDefCmin=IsDefCmax)) & 
%                     IsDefCmin) &
%                    (N2=ite(IsDefAmin, ite(B<N1,B,N1), B))) & 
%                    (M2=ite(IsDefAmax, ite(B>M1,B,M1), B)) 
%                )),
%      listMin(A,IsDefAmin,N1), listMin(C,IsDefCmin,N2),
%      listMax(A,IsDefAmax,M1), listMax(C,IsDefCmax,M2),
%      snoc(A,B,C).
% ===========================================================
:- query ff1/0.
%:- query ff2/0.
% ===========================================================

%  Catamorphic abstraction

:- cata_abs list(int) ==> 
           listMin(L,IsDefLmin,N1), listMax(L,IsDefLmax,M1).

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