% =================================================================
:- 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).
% ===========================================================
% Catamorphism
:- pred listlength(list(int),int).
:- mode listlength(in,out).    
:- cata listlength/2-1.

listlength([],L) :- constr(L=0).
listlength([H|T],L) :-
  constr( L=(LT+1) ),
  listlength(T,LT).
% ==================================================
% verification
:- pred ff1.
ff1 :-
  constr( ~(L1=L2) ), 
  listlength(L,L1),
	rev(L,R),
  listlength(R,L2).

%:- pred ff2.
%ff2 :-
%      constr(~( LC=(LA+1) )),
%      listlength(A,LA), listlength(C,LC),
%      snoc(A,B,C).
% ==================================================
:- query ff1/0.
%:- query ff2/0.
% ==================================================

%  Catamorphic abstraction

:- cata_abs list(int) ==> listlength(Ys,LYs).

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