% =================================================================
:- 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,L,B), constr(~B).
bubblesort(L,SL) :- swap(L,L1,B), constr(B),           
                    bubblesort(L1,SL).

:- 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 ).    % Any int value for Hd
hd([H|T],IsDef,Hd) :- constr( IsDef & Hd=H ).

% ---
:- 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).

% -------------------------------
% Contract on bubblesort:      Sort in ascending order.
:- spec bubblesort(L,S) ==>
	   is_asorted(S,B) =>    
	   constr(B).

% Contract on swap:   
:- spec swap(LA,LB,ToF) ==>                  % ToF: boolean variable (True or False)
        is_asorted(LA,BLA), is_asorted(LB,BLB)  =>
        constr( ((ToF = ~BLA)  &  (BLA => (BLB & ~ToF))) & (~BLA => ToF) ).

% Contract on cons: 
:- spec cons(H,T,HT) ==>
       is_asorted(T,BT),  is_asorted(HT,BHT),
       listMin(T,IsDefT,MinT), listMin(HT,IsDefHT,MinHT) =>
       constr(( IsDefHT & 
              ((IsDefT & (H=<MinT)) => (BT = BHT))) & 
              ((~IsDefT) => BHT)).

% -------------------------------------
% verification. 
:- pred ff1.
ff1 :- 
   constr(~B), 
   is_asorted(S,B),  
   bubblesort(L,S).

:- pred ff2.
ff2 :-
   constr( ~( ((ToF = ~(BLA))  &  (BLA => (BLB & (~ToF)))) & ((~BLA) => ToF) ) ), 
   is_asorted(LA,BLA), is_asorted(LB,BLB) , 
   swap(LA,LB,ToF).

:- pred ff3.
ff3 :-
   constr( ~(( IsDefHT & ((IsDefT & (H=<MinT)) => (BT = BHT))) & ((~IsDefT) => BHT)) ), 
   is_asorted(T,BT), listMin(HT,IsDefHT,MinHT), is_asorted(HT,BHT), listMin(T,IsDefT,MinT),
   cons(H,T,HT).

% --------------------------------------------------
% NON-CATA predicates: bubblesort cons constr swap