% ================================================================= 
:- 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 is 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 listMin(list(int),bool,int).     
:- mode listMin(in,out,out).

listMin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listMin([H|T],IsDef,Min) :-
        constr(IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H)) ),
        listMin(T,IsDefT,MinT).

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).             
cons(H,T,[H|T]).
% ====================================================
:- 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 ).
  
% ====================================================
% verification. 
% Property:
:- pred ff1.
ff1 :- 
     constr( ~(SS)), 
     is_asorted(L,LS),  
     is_asorted(S,SS), 
     selectionsort(L,S).

% contracts (postcondition: true)

:- spec delete(X,YT,T) ==> is_asorted(YT,SYT), is_asorted(T,ST).

:- spec listMin(L,B,M) ==> is_asorted(L,LS).

:- spec cons(H,T,HT) ==> is_asorted(T,ST), is_asorted(HT,SHT).

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