% =================================================================
:- pred constr(bool).    
:- mode constr(in).
:- ignore constr/1.
% ===========================================================
% Program
:- pred rev(list(int),list(int)).
:- mode rev(in,out).
rev([X],[]).  % error: [X] ---> []
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
%-----  listsum --- sum of integers in nodes of the given list.
:- pred listsum(list(int),int).
:- mode listsum(in,out).
:- cata listsum/2-1.

listsum([],S) :- S=0.
listsum([H|T],S) :-
  S=(H+ST),
  listsum(T,ST).
  
         
% ==================================================
% verification
:- pred ff1.
ff1 :- 
     constr( ~(LS=RS)), 
     listsum(L,LS),  
     listsum(R,RS), 
     rev(L,R). 
    
% contracts (postcondition: true)

:- spec snoc(A,B,C) ==> listsum(A,SA), listsum(C,SC).

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