% =================================================================
:- 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],[Y]). % error: Y --> 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,[],[X]).  %error: [X] -> [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 listmember(int,list(int),bool).
:- mode listmember(in,in,out).
:- cata listmember/3-2.

listmember(X,[],Res) :- constr(~Res).
listmember(X,[Y|Ys],B) :-
      constr( B=ite(X=Y,true,B1) ) ,
      listmember(X,Ys,B1).
  
% =================================================================
% Verification. 
% Property:
:- pred ff1.
ff1 :- 
   constr(~(LB=SB)), 
   listmember(X,L,LB), listmember(X,S,SB),  
   insertionsort(L,S).

%% contracts (postcondition: true)
%
%:- spec ord_ins(A,L1,L2) ==> listmember(X,L1,L1B), listmember(X,L2,L2B).

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

:- cata_abs list(int) ==> listmember(X,L1,L1B).

% ================================================================