% =================================================================
:- 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([],[158]). % error: this clause should be removed
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 listMax(list(int),bool,int).              
:- mode listMax(in,out,out).
:- cata listMax/3-1.

listMax([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listMax([H|T],IsDef,Max) :-
         constr( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H )) ),
         listMax(T,IsDefT,MaxT).

% ====================================================
% verification.
% Property:
:- pred ff1.
ff1 :-                            % perm
   constr( ~( (IsDefMaxL=IsDefMaxLP) &  (IsDefMaxL => (MaxL=MaxLP))  )),
   listMax(L,IsDefMaxL,MaxL), listMax(LP,IsDefMaxLP,MaxLP),
   perm(L,LP).

:- pred ff2.
ff2 :-                              % delete(X,L,LD) succeeds iff X is a member of L
  constr( ~( (IsDefMaxL & ((X=MaxL) & IsDefMaxLD)) => (MaxL >= MaxLD) )),
  listMax(L,IsDefMaxL,MaxL), listMax(LD,IsDefMaxLD,MaxLD),
  delete(X,L,LD).

:- pred ff3.
ff3 :-                              % cons
  constr( ~( IsDefMaxHT &
            (IsDefMaxT => (MaxHT=ite(H<MaxT,MaxT,H) )) ) ),
  listMax(T,IsDefMaxT,MaxT), listMax(HT,IsDefMaxHT,MaxHT),
  cons(H,T,HT).

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