% ================================================================= 
:- pred constr(bool). 
:- mode constr(in).
:- ignore constr/1.
% ====================================================
% Program. sorting in ascending order.E.g., 3 =< 5 =< 5 =< 8 =< ...
:- pred selectionsort(list(int),list(int)).
:- mode selectionsort(in,out).
selectionsort([],[]).
selectionsort([H|T],[Min|T1]) :- 
  cons(H,T,HT),    
  listMin(HT,IsDef,Min),             % HT is not empty. IsDef is true.     
  delete(Min,HT,L1),                 % Taking the minimum away from list HT.
  selectionsort(L1,T1).

:- pred delete(int,list(int),list(int)).
:- mode delete(in,in,in).
%delete(X,[],[]).                    % delete in not total
delete(X,[Y|T],T) :- constr(X=Y).    % Taking X away from [Y|T]. 
delete(X,[Y|T],[Y|TD]) :-            % Deleting exactly one copy of X only. 
  constr(~(X=Y)). % constr(~(X=Y)),       % The list is not ordered. 
  %error: uncomment following clause.  Correct: . ---> , above
 % delete(X,T,TD).                    % The element X need not be the minimum.

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).             
cons(H,T,[H|T]).

% ====================================================
% catamorphisms .Ascending-order sorting
:- pred listMin(list(int),bool,int).
:- mode listMin(in,out,out).
:- cata listMin/3-1.

listMin([],B,Res) :- constr((~B) & (Res=0)). % 0 can be any int.
listMin([H|T],B,Res) :-
          constr( B & ( Res=ite(BT, ite(H<ResT,H,ResT), H) ) ),
          listMin(T,BT,ResT).
          
:- 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).

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

:- pred ff2.
ff2 :- 
    constr( ~((A=MinL) => (SLD=(SL-MinL)) )), 
    sum(L,SL), sum(LD,SLD), listMin(L,IsDef,MinL),
    delete(A,L,LD).
    % Contract on delete (for any A, not necessarily the minimum of L)

:- pred ff3.
ff3 :- 
  constr( ~(SHT=(ST+H)) ), 
  sum(T,ST), sum(HT,SHT),
  cons(H,T,HT).
% =================================================================
:- query ff1/0.
:- query ff2/0.
:- query ff3/0.
% =================================================================0.