% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.

% =================================================================
% Program. ascending sorting
:- pred insertionsort(list(int),list(int)).
:- mode insertionsort(in,out).

insertionsort([],[]).
insertionsort([X|Xs],S) :- ord_ins(X,TS,S),
         insertionsort(Xs,TS).

:- pred ord_ins(int,list(int),list(int)).  
:- mode ord_ins(in,in,out).

ord_ins(A,[],[A]).
ord_ins(A,[B|Xs],[A,B|Xs]) :- constr( A=<B ).
ord_ins(A,[B|Xs],[B|AXs]) :- constr( A>B ), 
     ord_ins(A,Xs,AXs).


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

% ================================================================= 
% Contract on bubblesort:
:- spec insertionsort(L,S)
    ==> sum(L,SL), sum(S,SS) 
        => constr(SL=SS).

% Contract on ord_ins:
:- spec ord_ins(X,LA,LB) ==>
        sum(LA,SLA), sum(LB,SLB)
        =>
        constr( (SLA+X)=SLB ).


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

:- pred ff2.
ff2 :-
      constr( ~((SLA+X)=SLB) ), 
      sum(LA,SLA), sum(LB,SLB),
      ord_ins(X,LA,LB).

% ================================================================= 
% NON-CATA predicates: constr insertionsort ord_ins