% =================================================================
:- pred constr(bool).    
:- mode constr(in).
:- ignore constr/1.
% ===========================================================
% Program
:- pred rev(list(int),list(int)).
:- mode rev(in,out).

rev([],[X]). %error: [X] should be []
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 listmin(list(int),bool,int). 
:- mode listmin(in,out,out).  
:- cata listmin/3-1.

listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listmin([H|T],IsDef,Min) :-
         constr( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H )) ),
         listmin(T,IsDefT,MinT).
         
% ==================================================
% verification
:- pred ff1.
ff1 :- 
    constr( ~((IsDefLMin = IsDefRMin) & 
    ((IsDefLMin & IsDefRMin) => (LMin=RMin)) )), 
    listmin(L,IsDefLMin,LMin), listmin(R,IsDefRMin,RMin),
    rev(L,R). 
    
% contracts (postcondition: true)
%
%:- spec snoc(A,B,C) ==> listmin(A,B1,SA), listmin(C,B2,SC).

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

%  Catamorphic abstraction

:- cata_abs list(int) ==> listmin(L,IsDefLmin,N1).

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