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

bubblesort([X,Y],[X,Y]). %error: erase this clause
bubblesort(L,L) :- swap(L,L1,B), constr(~B), eqlist(L,L1). 
bubblesort(L,SL) :- swap(L,L1,B), constr(B),           
                    bubblesort(L1,SL).
                    
:- 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]).

% =================================================================
% catamorphisms

:- pred is_asorted(list(int),bool).
:- mode is_asorted(in,out).
:- cata is_asorted/2-1.

is_asorted([],Res) :- constr(Res).
is_asorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    is_asorted(T,ResT),
    constr(Res=(IsDefT => (H=<HdT & ResT))).

% ---
:- pred hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Hd) :- constr( ~IsDef & Hd=0 ).    % 0 can be any int.
hd([H|T],IsDef,Hd) :- constr( IsDef & Hd=H ).
% =================================================================
% Verification.
% Property:
:- pred ff1.
ff1 :- 
   constr(~(SS)), 
   is_asorted(L,SL), is_asorted(S,SS),  
   bubblesort(L,S).
     
% contracts (postcondition: true)

:- spec swap(L,L1,B) ==> is_asorted(L,LS), is_asorted(L1,L1S) => constr(true).

:- spec eqlist(L,L1) ==> is_asorted(L,LS), is_asorted(L1,L1S) => constr(true).

:- spec cons(H,T,HT) ==> is_asorted(T,TS), is_asorted(HT,HTS) => constr(true).

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