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

% =================================================================
% Program. ascending sorting
:- pred bubblesort(list(int),list(int)).
:- mode bubblesort(in,out).

bubblesort(L,L) :- swap(L,L1,B), constr(~B), eqlist(L,L1). 
bubblesort(L,SL) :- swap(L,L1,B), constr(B),           
                    bubblesort(L1,SL).   
bubblesort(L1,[X]). % error: erase clause
                    
:- pred eqlist(list(int),list(int)).
:- mode eqlist(in,in).
eqlist(L,L).  

:- pred swap(list(int),list(int),bool).   % bool is true if a swap has been done
:- mode swap(in,out,out).

swap([],[],B) :- constr(~B).
swap([X],[X],B) :- constr(~B). 
swap([X,Y|Ys],[Y|Zs],B) :-  
         constr(B & (X > Y)),
         cons(X,Ys,XYs),
         swap(XYs,Zs,B).
swap([X,Y|Ys],[X|Zs],B) :-
        constr(X =< Y),
        cons(Y,Ys,YYs),
        swap(YYs,Zs,B).

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).
cons(H,T,[H|T]).  

% =================================================================
% 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.
% Property:
:- pred ff1. 
ff1 :- 
     constr( ~((IsDefLMin = IsDefSMin) & 
     ((IsDefLMin & IsDefSMin) => (MinL=MinS)) )), 
     listmin(L,IsDefLMin,MinL),  
     listmin(S,IsDefSMin,MinS), 
     bubblesort(L,S).
     
%% contracts (postcondition: true)
%
%:- spec swap(L,L1,B) ==> listmin(L,LB,LM), listmin(L1,L1B,L1M).
%
%:- spec eqlist(L,L1) ==> listmin(L,LB,LM), listmin(L1,L1B,L1M).
%
%:- spec cons(H,T,HT) ==> listmin(T,TB,TM), listmin(HT,HTB,HTM).

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

%  Catamorphic abstraction

:- cata_abs list(int) ==> listmin(L,LB,LM).

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