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

% =================================================================
% catamorphisms
%% checking the weakly ascending order in a list
:- pred is_asorted(list(int),bool).
:- mode is_asorted(in,out).
:- cata is_asorted/2-1.

is_asorted([],Res) :- constr(Res).
is_asorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    is_asorted(T,ResT),
    constr(Res=(IsDefT => (H=<HdT & ResT))).
% ---

:- pred grt_all(int,list(int),bool).
:- mode grt_all(in,in,out).
:- cata grt_all/3-2.

grt_all(N,[],B) :- constr(B).       % N is greater ( > ) of all elements of list [X|Xs]
grt_all(N,[X|Xs],B) :-              % grt_all(N,L,true): L is made out of *small* elements
	grt_all(N,Xs,B1),
	constr(B = ((N>X) & B1)).

%---

:- pred leq_all(int,list(int),bool).
:- mode leq_all(in,in,out).
:- cata leq_all/3-2.

leq_all(N,[],B) :- constr(B).       % N is leq ( =< ) of all elements of list [Y|Ys]
leq_all(N,[Y|Ys],B) :-              % leq_all(N,L,true): L is made out of *big* elements
	leq_all(N,Ys,B1),
	constr(B = (N=<Y & B1)).

% ---
:- pred hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Hd) :- constr( ~IsDef & (Hd=0) ).    % Any int value for Hd, instead of 0.
hd([H|T],IsDef,Hd) :- constr( IsDef & (Hd=H) ).


% =================================================================
% Contract on insertionsort:
:- spec insertionsort(L,S) ==>
        is_asorted(S,B) =>
        constr(B).

% Contract on ord_ins:
:- spec ord_ins(X,L,XL) ==>
        is_asorted(L,SL), is_asorted(XL,SXL)  =>
        constr( SL = SXL ).

% =================================================================
% verification.
% Property:
:- pred ff1.
ff1 :-
   constr(~B),
   is_asorted(S,B),
   insertionsort(L,S).

:- pred ff2.
ff2 :-
   constr( ~( SL = SXL ) ),
   is_asorted(L,SL), is_asorted(XL,SXL),
   ord_ins(X,L,XL).

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