% =================================================================
:- 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,false).
bubblesort(L,SL) :- swap(L,L1,true),
                    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([],[],false).
swap([X],[X],false).
swap([X,Y|Ys],[Y|Zs],true) :-
         constr(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 listMax(list(int),bool,int).              
:- mode listMax(in,out,out).
:- cata listMax/3-1.

listMax([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listMax([H|T],IsDef,Max) :-
         constr( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H )) ),
         listMax(T,IsDefT,MaxT).

% =================================================================
% Contract on bubblesort:
:- spec bubblesort(L,S)
         ==> listMax(L,IsDefL,MaxL), listMax(S,IsDefS,MaxS)
             => constr( (IsDefL = IsDefS) & (IsDefL => (MaxL=MaxS)) ).

% Contract on swap:
:- spec swap(Xs,Ys,ToF)
        ==>
        listMax(Xs,IsDefXs,MXs), listMax(Ys,IsDefYs,MYs)
            =>
            constr( (IsDefXs = IsDefYs) & (IsDefXs => (MXs=MYs)) ).

% Contract on cons:
:- spec cons(H,T,HT) ==>
       listMax(T,IsDefMT,MT), listMax(HT,IsDefMHT,MHT) =>
       constr( (( IsDefMT => (IsDefMHT & (MHT = ite(H>MT,H,MT))) )
               & (~(IsDefMT) => (H=MHT)) )).

% =================================================================
% verification.
% Property:
:- pred ff1.
ff1 :-
   constr(~( (IsDefL = IsDefS) & (IsDefL => (MaxL=MaxS)) )),
   listMax(L,IsDefL,MaxL), listMax(S,IsDefS,MaxS),
   bubblesort(L,S).

:- pred ff2.
ff2 :-
      constr(~( (IsDefXs = IsDefYs) & (IsDefXs => (MXs=MYs)) )),
      listMax(Xs,IsDefXs,MXs), listMax(Ys,IsDefYs,MYs),
      swap(Xs,Ys,ToF).

:- pred ff3.
ff3 :-
       constr( ~(( IsDefMT => (IsDefMHT & (MHT = ite(H>MT,H,MT))) )
               & (~(IsDefMT) => (H=MHT)) )),
       listMax(T,IsDefMT,MT), listMax(HT,IsDefMHT,MHT),
       cons(H,T,HT).

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