% =================================================================
:- 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).
                    
:- 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 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).
% ---
:- pred lastElem(list(int),bool,int).              
:- mode lastElem(in,out,out).
:- cata lastElem/3-1.

lastElem([],IsDef,Last) :- constr( ((~IsDef) & (Last=0)) ).
lastElem([H|T],IsDef,Last) :-
         constr( IsDef & (Last=ite(IsDefT,LastT,H)) ),
         lastElem(T,IsDefT,LastT).

% =================================================================
% Verification.
:- pred ff1.
ff1 :-     % listMax of unsorted list is equal to lastElem of quicksorted, ascending list
     constr( ~( ( ((IsDefMaxL = IsDefMaxS) &
                   (IsDefMaxL = IsDefLastS))) &
                   (IsDefMaxL => (MaxL=LastS)))),
     listMax(L,IsDefMaxL,MaxL), listMax(S,IsDefMaxS,MaxS), lastElem(S,IsDefLastS,LastS),
     bubblesort(L,S).

:- pred ff2.
ff2 :-
    constr( ~( ((IsDefMaxLA = IsDefMaxLB) & (IsDefMaxLA = IsDefLastLB)) &
                  ((IsDefMaxLA & (~ToF)) => (MaxLB=LastLB)))),
    listMax(LA,IsDefMaxLA,MaxLA), listMax(LB,IsDefMaxLB,MaxLB), lastElem(LB,IsDefLastLB,LastLB),
    swap(LA,LB,ToF).

:- pred ff3.
ff3 :-
    constr( ~(  (((IsDefMaxHT & IsDefLastHT) & (IsDefMaxT=IsDefLastT)) &
                 ( IsDefMaxT  => (MaxHT = ite(H>MaxT,H,MaxT)  & (LastT=LastHT)) )) &
               ( (~IsDefMaxT)  => ((MaxHT=H) & (LastHT=H)) ) )),
    listMax(T,IsDefMaxT,MaxT), listMax(HT,IsDefMaxHT,MaxHT),
    lastElem(T,IsDefLastT,LastT), lastElem(HT,IsDefLastHT,LastHT),
    cons(H,T,HT).
% =================================================================
:- query ff1/0.
:- query ff2/0.
:- query ff3/0.
% =================================================================