% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% =================================================================
% Program. ascending sorting  (ascending because we take the minimum) 2 =< 4 =< 7 =< ...
:- 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. 
  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]).

% ====================================================
% catamorphisms .Ascending-order sorting
:- 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 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 hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Hd) :- constr( (~IsDef) & (Hd=0) ).    % 0 can be any int
hd([H|T],IsDef,Hd) :- constr( IsDef & (Hd=H) ).

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

% Contract on delete   
:- spec delete(X,L,LD) ==>
        is_asorted(L,BL), is_asorted(LD,BLD), 
        listMin(L,IsDefL,MinL), listMin(LD,IsDefLD,MinLD)
        => constr(((IsDefLD => (( BL => BLD) & (MinLD >= MinL))) & 
                   (IsDefLD => IsDefL)) & 
                  ((IsDefL & (~IsDefLD)) => (X=MinL))
                  ).
%Contract on cons:
:- spec cons(H,T,HT)  ==>
     is_asorted(T,BT), listMin(T,IsDefT,MinT),     
     is_asorted(HT,BHT)  =>
     constr( ((BT & IsDefT) & (H=<MinT)) => BHT ). 

% =================================================================
% verification.
:- pred ff1.
ff1 :-
   constr(~(B)),
   is_asorted(S,B),
   selectionsort(L,S).
   
:- pred ff2.         
ff2:- delete(X,L,LD),
      is_asorted(L,BL), is_asorted(LD,BLD), 
      listMin(L,IsDefL,MinL), listMin(LD,IsDefLD,MinLD),
      constr( ~(((IsDefLD => (( BL => BLD) & (MinLD >= MinL))) & 
                 (IsDefLD => IsDefL)) & 
                ((IsDefL & (~IsDefLD)) => (X=MinL))
                )).

:- pred ff3.  
ff3 :-
 constr( ~( ((BT & IsDefT) & (H=<MinT)) => BHT ) ), 
 is_asorted(T,BT), listMin(T,IsDefT,MinT), is_asorted(HT,BHT),
 cons(H,T,HT).
  
% =================================================================
% NON-CATA predicates: cons constr delete selectionsort