% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.   

% =================================================================
% Program. descending sorting via selection sort
:- pred selectionsort(list(int),list(int)).
:- mode selectionsort(in,out).

selectionsort([],[X]).    % ERROR: [X] -> []S
selectionsort([H|T],[Max|T1]) :-
  cons(H,T,HT),        
  listMax(HT,IsDef,Max),             % HT is not empty. IsDef is true.     
  delete(Max,HT,L1),                 % Taking the maximum 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 maximum.

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).             
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,MaxHT) :-
         constr( IsDef & (MaxHT = 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).

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

lastElem([],IsDef,Last) :- constr( ((~IsDef) & (Last=0)) ).
lastElem([H|T],IsDef,Last) :-
         constr( IsDef & (Last=ite(IsDefT,LastT,H)) ),
         lastElem(T,IsDefT,LastT).

% =================================================================
% Verification.
% Property:
:- pred ff1.
ff1 :-         % listMin of unsorted equal lastElem of descending, selectionsortsorted list 
   constr( ~(( (IsDefLMin =  IsDefSMin) & 
               (IsDefLMin =  IsDefSLast)) & 
               (IsDefLMin => ((MinL=LastS) & (MinL=MinS))) )),
   listMin(L,IsDefLMin,MinL), listMin(S,IsDefSMin,MinS), 
   lastElem(S,IsDefSLast,LastS),
   selectionsort(L,S).


%% Contract on delete (for any X, not necessarily the maximum of L, but X in L): 
%% here is for deleting the maximum. 
%:- pred ff2.
%ff2 :-      
%    constr(~( ((IsDefMaxL=IsDefLastL) & 
%               (IsDefMaxLD=IsDefLastLD)) &
%              ((IsDefMaxL & X=MaxL) =>
%                                (((~IsDefMaxLD) => (MaxL=LastL)) &
%                                  (IsDefMaxLD   => ((MaxLD=<MaxL) & (LastLD=<LastL))))))),
%    listMax(L,IsDefMaxL,MaxL), lastElem(L,IsDefLastL,LastL), 
%    listMax(LD,IsDefMaxLD,MaxLD), lastElem(LD,IsDefLastLD,LastLD),
%    delete(X,L,LD).
%    
%:- pred ff3.
%ff3 :- 
%    constr(~((IsDefMinHT &
%             (MinHT=ite(IsDefMinT,ite(H<MinT,H,MinT), H) )))),                   
%    listMin(T,IsDefMinT,MinT), listMin(HT,IsDefMinHT,MinHT),
%    cons(H,T,HT).

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

%  Catamorphic abstraction

:- cata_abs list(int) ==> listMin(L,IsDefMaxL,MaxL), 
                        lastElem(L,IsDefLastL,LastL).

% =========================================================