% ================================================================= 
:- pred constr(bool). 
:- mode constr(in).
:- ignore constr/1.
% ================================================================= 
% Program. ascending sorting  (ascending because we take the minimum)
:- pred selectionsort(list(int),list(int)).
:- mode selectionsort(in,out).
selectionsort([],[158]).   %error:  [158] should be []
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)),                    % The list is not ordered. 
  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,T).    %error: it should be cons(H,T,[H|T]).

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

listMax([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ). % 0 can be any int.
listMax([H|T],IsDef,Max) :-
         constr( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H )) ),
         listMax(T,IsDefT,MaxT).
         
:- pred listMin(list(int),bool,int).
:- mode listMin(in,out,out).                  
:- cata listMin/3-1.
 
listMin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ). % 0 can be any int.
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(~( (IsDefL = IsDefS) & (IsDefL => (MaxL=MaxS)) )),
   listMax(L,IsDefL,MaxL), listMax(S,IsDefS,MaxS),
   selectionsort(L,S).

% Contract on delete (for any X, not necessarily the minimum of L): 
:- pred ff2.
ff2 :- 
    constr(~(  (   IsDefL  & 
               (  (IsDefLD & (X<MaxL)) => (MaxL = MaxLD) ))  & 
               (( ~IsDefLD) => (MaxL=X))
             )),
    listMax(L,IsDefL,MaxL), listMax(LD,IsDefLD,MaxLD),
    delete(X,L,LD).

:- pred ff3.
ff3 :- 
   constr(~( IsDefHT & ( MaxHT=ite(IsDefT,ite(H>MaxT,H,MaxT),H) ) )),
   listMax(T,IsDefT,MaxT), listMax(HT,IsDefHT,MaxHT),
   cons(H,T,HT).
% =================================================================
:- query ff1/0.
:- query ff2/0.
:- query ff3/0.
% =================================================================