% =================================================================
:- 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), eqlist(L,L1), constr(~B). % error: ~B should be B
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|Ys],[Y|Zs],B) :-  % error here: X should be X,Y
         constr(B & (X > Y)), 
         cons(X,Ys,XYs),
         swap(XYs,Zs,B).
swap([Y|Ys],[X|Zs],B) :-  % error here: Y should be X,Y
        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 sum(list(int),int).
:- mode sum(in,out).
:- cata sum/2-1.

sum([],S) :- constr((S=0)).
sum([H|T],S) :-
  constr( S=(H+ST) ),
  sum(T,ST).

% =================================================================
% verification of contracts.
:- pred ff1.
ff1 :-
   constr(~(SL=SS)),
   sum(L,SL), sum(S,SS),
   bubblesort(L,S).

:- pred ff2.
ff2 :-
    constr( ~( SLA = SLB ) ),
    sum(LA,SLA), sum(LB,SLB),
    swap(LA,LB,ToF).

:- pred ff3.
ff3 :-
   constr( ~( SHT = (H+ST) ) ),
   sum(T,ST), sum(HT,SHT),
   cons(H,T,HT).

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