% =================================================================
:- 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([],[],[X]). %error: delete clause 
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 listcount(int,list(int),int).
:- mode listcount(in,in,out).
:- cata listcount/3-2. 

listcount(X,[],N) :- constr( N=0).
listcount(X,[H|T],N) :-
  constr( (N=ite(X=H,(NT+1),NT)) ),
  listcount(X,T,NT).
  
:- pred listsize(list(int),int).
:- mode listsize(in,out).
:- cata listsize/2-1.

listsize([],L) :- L=0.
listsize([H|T],L) :-
  L=(LT+1),
  listsize(T,LT).

% ===========================================================
% Property to verify
:- pred ff1.
ff1 :- constr( ~( (N1=N2) & (LS=RS) ) ),
    listcount(X,L,N1), listcount(X,R,N2),
    listsize(L,LS), listsize(R,RS),
    revacc(L,R).
    
%    
%:- spec reva(L,Acc,RL) ==> listcount(X,L,SL), listcount(X,Acc,SAcc), listcount(X,RL,SRL),
%                           listsize(L,SL), listsize(Acc,SAcc), listsize(RL,SRL) => constr(true).
%
%:- spec emptylist(L) ==> listcount(X,L,SL), listsize(L,SL) => constr(true).
%
%:- spec cons(H,T,HT) ==> listcount(X,T,ST), listcount(X,HT,SHT),
%                         listsize(T,ST), listsize(HT,SHT) => constr(true).
%% ===========================================================
:- query ff1/0.
% ===========================================================
%  Catamorphic abstraction

:- cata_abs list(int) ==> listcount(X,L,LB), listsize(L,LS).

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