% =================================================================
:- 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 count(int,list(int),int).
:- mode count(in,in,out).
:- cata count/3-2. 

count(X,[],N) :- constr( N=0).
count(X,[H|T],N) :-
  constr( (N=ite(X=H,(NT+1),NT)) ),
  count(X,T,NT).

% ===========================================================
% contract for revacc
:- spec revacc(L,R) ==> 
    count(X,L,N1), count(X,R,N2) =>
    constr( N1=N2 ).

%contract on reva
:- spec reva(Xs,As,Ys) ==> 
    count(X,Xs,N1), count(X,As,N2), count(X,Ys,N3) =>
    constr( N3=(N1+N2) ).

% contract on cons
:- spec cons(H,T,HT) ==> 
    count(X,T,NT), count(X,HT,NHT) =>
    constr( NHT=ite(H=X,(NT+1),NT) ).

% ===========================================================
% Property to verify
:- pred ff1.
ff1 :- constr( ~( N1=N2) ),
    count(X,L,N1), count(X,R,N2),
    revacc(L,R).
    
:- pred ff2.
ff2 :- constr( ~( N3=(N1+N2)) ),
    count(X,Xs,N1), count(X,As,N2), count(X,Ys,N3),
    reva(Xs,As,Ys).

:- pred ff3.
ff3 :- constr(~(NHT=ite(H=X,(NT+1),NT) )),
    count(X,T,NT), count(X,HT,NHT), 
    cons(H,T,HT).
% ===========================================================
% NON-CATA predicates: cons constr reva revacc