% =================================================================
:- 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]):-
      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. The 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       
:- pred length(list(int),int).
:- mode length(in,out).
:- cata length/2-1.

length([],L) :- L=0.
length([H|T],L) :-
  L=(LT+1),
  length(T,LT).

% ====================================================
% Contract on perm:
:- spec perm(L,LP) ==>
        length(L,LL), length(LP,LLP)   =>
        constr( LL=LLP ).

% Contract on delete:         % delete(X,L,LD) succeeds iff X is a member of L.
:- spec delete(H,L,LD) ==>    % L is assumed to be not empty.
        length(L,LL), length(LD,LLD) =>
        constr( LLD = (LL-1) ). 
        
% Contract on cons:
:- spec cons(H,T,HT) ==>
		 length(T,LT), length(HT,LHT) =>
		 constr( LHT =(LT+1)    ).

% ====================================================
% verification.
% Property:
:- pred ff1.
ff1 :-                              % perm
   constr( ~(LL=LLP)),
   length(L,LL), length(LP,LLP),
   perm(L,LP).

:- pred ff2.
ff2 :-                              % delete.   ***  L is assumed to be not empty.
   constr( ~(LLD = (LL-1)) ),
   length(L,LL), length(LD,LLD),
   delete(H,L,LD).                  % delete(X,L,LD) succeeds iff X is a member of L.

:- pred ff3.
ff3 :-                              % cons
  constr( ~(LHT =(LT+1)) ),
  length(T,LT), length(HT,LHT),
  cons(H,T,HT).

% ====================================================
% NON-CATA predicates: cons constr delete perm
% ====================================================