% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% ====================================================
% Program.
:- pred perm(list(int),list(int)).
:- mode perm(in,in).               % in,in: perm is not functional
perm([],[]).
perm([X|Xs],[H|Perm]):-            % a permutation
      cons(X,Xs,XXs),
      delete(H,XXs,Rest),
      perm(Rest,Perm).

:- pred delete(int,list(int),list(int)).
:- mode delete(in,in,in).          % delete is not total
delete(X,[Y|T],T) :- constr(X=Y).  % Taking X away from [Y|T]. Deleting exactly one copy of X.
delete(X,[Y|T],[Y|TD]) :-          % The list need not be ordered. Element X need not be the minimum.
  constr(~(X=Y)),                  % delete(X,L,LD) succeeds **IFF** X is a member of L.
  delete(X,T,TD).

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).
cons(H,T,[H|T]).
% ====================================================
% catamorphisms       
% --- min of a list
:- pred listmin(list(int),bool,int). 
:- mode listmin(in,out,out).  
:- cata listmin/3-1.

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).

% ====================================================
% verification.
% Property:
:- pred ff1.
ff1 :- 
    constr( ~((IsDefLMin = IsDefLPMin) & 
    ((IsDefLMin & IsDefLPMin) => (LL=LLP)) )),                             
    listmin(L,IsDefLMin,LL), listmin(LP,IsDefLPMin,LLP),
    perm(L,LP).
   
% contracts (postcondition: true)

:- spec delete(H,L,LD) ==> listmin(L,B1,SL), listmin(LD,B2,SLD).

:- spec cons(H,T,HT) ==> listmin(T,B1,ST), listmin(HT,B2,SHT).

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