% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% =================================================================
% Program. 
% Delete multiple copies on lists leaving one copy only.
% example: [3,2,3,4,2] --> [3,2,4]
:- pred list_deletecopies(list(int),list(int)).
:- mode list_deletecopies(in,out).

list_deletecopies([],[]).
list_deletecopies([X],[X]).
list_deletecopies([X,X|T], ResT) :- cons(X,T,XT), 
      list_deletecopies(XT,ResT).
list_deletecopies([X,Y|T], [X|ResT]) :- constr(~(X=Y)), 
      cons(Y,T,YT), list_deletecopies(YT,ResT1), deleteall(X,ResT1,ResT).


% all elements X are deleted from a list, producing a new list.
:- pred deleteall(int,list(int),list(int)).
:- mode deleteall(in,in,out).

deleteall(X,[],[]).
deleteall(X,[X|T],Res) :- deleteall(X,T,Res).
deleteall(X,[H|T],[H|ResT]) :- constr(~(X=H)), deleteall(X,T,ResT).

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).
cons(H,T,[H|T]).

% =================================================================
% catamorphism
:- pred listcount(int,list(int),int).
:- mode listcount(in,in,out).
:- cata listcount/3-2.

listcount(X,[],N) :- N=0.
listcount(X,[H|T],N) :-
  constr( (N=ite(X=H,(NT+1),NT)) ),
  listcount(X,T,NT).

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

listmember(X,[],Res) :- constr(~Res).
listmember(X,[H|T],Res) :-
  constr( (Res=ite(X=H,true,ResT)) ),
  listmember(X,T,ResT).
  
% =================================================================
% Verification.
% Property:
:- pred ff1.
ff1 :- 
  constr(~(B => SN=1)), 
  listmember(X,L,B),  listcount(X,L,LN),    % all four X
  listmember(X,S,SB), listcount(X,S,SN),
  list_deletecopies(L,S).
%  
%:- spec deleteall(X,L,L1) ==> listmember(Y,L,LB), listcount(Y,L,LS),  % all four Y
%                              listmember(Y,L1,L1B), listcount(Y,L1,L1S)
%                               => constr(true).
%
%:- spec cons(H,T,HT) ==> listmember(X,T,TB), listcount(X,T,TN),       % all four X
%                         listmember(X,HT,HTB), listcount(X,HT,HTN) => constr(true).

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

%  Catamorphic abstraction

:- cata_abs list(int) ==> listmember(X,L,B),  listcount(X,L,LN).

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