% =================================================================
:- pred constr(bool).    
:- mode constr(in).
:- ignore constr/1.
% ===========================================================

% Program
:- pred rev(list(int),list(int)).
:- mode rev(in,out).
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.  All variables in the head, except for the data structure
:- 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,(M+1),M) ),
  count(X,T,M).
% ===========================================================

% Contract on rev:
:- spec rev(L,R) ==>
        count(X,L,N1), count(X,R,N2) => constr( N1=N2 ).

% Contract on snoc:
:- spec snoc(A,B,C) ==>
        count(X,A,NA), count(X,C,NC) => constr( NC=ite(B=X,(NA+1),NA) ).
% ===========================================================

% Property
:- pred ff1.
ff1 :-
  constr( ~(N1=N2) ), 
  count(X,L,N1),
	rev(L,R),
  count(X,R,N2).

:- pred ff2.
ff2 :-
      constr(~( NC=ite(B=X,(NA+1),NA) )),
      count(X,A,NA), count(X,C,NC),
      snoc(A,B,C).

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


% NON-CATA predicates: constr rev snoc