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

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

listmember(X,[],Res) :- constr(~Res).
listmember(X,[H|T],Res) :-
  constr( (Res=ite(X=H,true,ResT)) ),
  listmember(X,T,ResT).
         
% ==================================================
% verification
:- pred ff1.
ff1 :- 
     constr( ~(LB => RN>=1)), % obviously, also RN>=0 is sat
     listmember(X,L,LB),
     listmember(X,R,RB),
     listcount(X,L,LN), 
     listcount(X,R,RN), 
     rev(L,R). 
    
% contracts (postcondition: true)

:- spec snoc(A,B,C) ==> listcount(X,A,SA), listcount(X,C,SC),
                        listmember(X,A,AB), listmember(X,C,CB) => constr(true).

% ==================================================
:- query ff1/0.
% ==================================================