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

% ====================================================
% Program. sorting in ascending order 1 =< 2 =< 3=<...
:- 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 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 insertionsort(L,S)
         ==> listMax(L,IsDefL,MaxL), listMax(S,IsDefS,MaxS)  
             => constr( (IsDefL = IsDefS) & (IsDefL => (MaxL=MaxS)) ).

% Contract on ord_ins:
:- spec ord_ins(X,LA,LB) ==>
        listMax(LA,IsDefMaxLA,MaxLA), listMax(LB,IsDefMaxLB,MaxLB)
        =>
           constr(    IsDefMaxLB &
               MaxLB = ite(IsDefMaxLA, ite(X>MaxLA,X,MaxLA) , X) ).
% ================================================================= 
% verification. 
% Property:
:- pred ff1.
ff1 :-
   constr(~( (IsDefL = IsDefS) & (IsDefL => (MaxL=MaxS)) )),
   listMax(L,IsDefL,MaxL), listMax(S,IsDefS,MaxS),
   insertionsort(L,S).

:- pred ff2.
ff2 :-
      constr(~( IsDefMaxLB &
                MaxLB = ite(IsDefMaxLA, ite(X>MaxLA,X,MaxLA), X))),
      listMax(LA,IsDefMaxLA,MaxLA), listMax(LB,IsDefMaxLB,MaxLB),
      ord_ins(X,LA,LB).

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