% =================================================================
:- 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([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 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 listmin(list(int),bool,int). 
:- mode listmin(in,out,out).  
:- cata listmin/3-1.

listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listmin([H|T],IsDef,Min) :-
         constr( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H )) ),
         listmin(T,IsDefT,MinT).

% ===========================================================
% Property to verify
:- pred ff1. 
ff1 :- 
     constr( ~((IsDefLMin = IsDefSMin) & 
     ((IsDefLMin & IsDefSMin) => (MinL=MinS)) )), 
     listmin(L,IsDefLMin,MinL),  
     listmin(S,IsDefSMin,MinS), 
     revacc(L,S).

% contracts (postcondition: true)

:- spec reva(L,Acc,RL) ==> listmin(L,B1,SL), listmin(Acc,B2,SAcc), listmin(RL,B3,SRL)
             => constr(true).

:- spec emptylist(L) ==> listmin(L,B1,SL) => constr(true).

:- spec cons(H,T,HT) ==> listmin(T,B1,ST), listmin(HT,B2,SHT) => constr(true).
    
% ===========================================================
:- query ff1/0.
% ===========================================================