% ================================================================= 
:- 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([],[]).
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,[H|T]).

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

:- pred count(int,list(int),int).
:- mode count(in,in,out).
:- cata count/3-2.
count(X,[],Res) :- constr( Res=0 ).
count(X,[Y|Ys],Res) :- 
    constr( Res=ite(X=Y,(ResT+1),ResT) ),
    count(X,Ys,ResT).   

% ================================================================= 
% Contract on selectionsort:
:- spec selectionsort(L,S) ==>
        count(X,L,CL), count(X,S,CS) =>
        constr( CL=CS ).

% Contract on delete:   
:- spec delete(A,L,LD) ==>                       
        % cons(H,T,L), 
        count(X,L,CL), count(X,LD,CLD)
        => constr( (IsDefL) & (CLD = ite(A=X, (CL-1), CL)) ).

% Contract on cons:   
:- spec cons(H,T,HT)  ==>                       
       count(X,T,CT), count(X,HT,CHT)
       => constr( CHT = ite(X=H, (CT+1), CT) ).

% ================================================================= 
% verification. 
% Property:
:- pred ff1.
ff1 :- 
   constr( ~(CL=CS) ), 
   count(X,L,CL), count(X,S,CS),  
   selectionsort(L,S).

:- pred ff2.
ff2 :- 
   constr( ~( CLD = ite(A=X, (CL-1), CL) )), 
   % cons(H,T,L), 
   count(X,L,CL), count(X,LD,CLD),
   delete(A,L,LD).

:- pred ff3.
ff3 :- 
  constr( ~(CHT = ite(X=H, (CT+1), CT)) ), 
  count(X,T,CT), count(X,HT,CHT), 
  cons(H,T,HT).

% --------------------------------------------------
% NON-CATA predicates: cons constr delete selectionsort