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

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

insertionsort([],[X]).  % error: [X]  --> []
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 listmin(list(int),bool,int). 
:- mode listmin(in,out,out).  
:- cata listmin/3-1.
listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listmin([H|T],IsDef,Min) :-
         constr( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H )) ),
         listmin(T,IsDefT,MinT).
         
% =================================================================
% Verification. 
% Property:
:- pred ff1. 
ff1 :- 
     constr( ~((IsDefLMin = IsDefSMin) & 
     ((IsDefLMin & IsDefSMin) => (MinL=MinS)) )), 
     listmin(L,IsDefLMin,MinL),  
     listmin(S,IsDefSMin,MinS), 
     insertionsort(L,S).

% contracts (postcondition: true)

:- spec ord_ins(A,L1,L2) ==> listmin(L1,B1,SL1) , listmin(L2,B2,SL2).

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