% File 'member.pl'
%----
:- ensure_loaded(typeops).

% member in various list
% unification
% unique insertion of an element into a list

 
%+++++++++++++++++++++++++++++ type definitions +++++++++++++++++++++++ 

:- type int.
:- type nat.
:- subtype negint < int.
:- subtype nat < int.
:- subtype posint < nat.
:- subtype zero < nat.
:- type posint --> 1;2.
:- type zero --> 0.
:- type negint --> -1; -2.

:- type list(T) --> [ T | list(T) ].
:- suptype list(T) > elist(T).
:- type elist(T) --> [].


 
%+++++++++++++++++++++++++++++ predicates  +++++++++++++++++++++++ 

% pred member(@T1,list(@T2)) -> T1 =< T2.
:- pred member(T,list(@T)).
member(X,[X|_]).
member(X,[_|L]) :- member(X,L).

% pred member_old(@T1, list(@T2)) -> T1 =< T, T2 =< T.
:- pred member_old(T,list(T)).
member_old(X,[X|_]).
member_old(X,[_|L]) :- member_old(X,L).

%-----

% =/2
:- pred @T = @T.

% =_old/2
:- pred equal_old(T,T).
equal_old(X,Y) :- X = Y.


%-----

:- pred !.

:- pred insert_uniq( T, list(T), list(@T)).  
% insert_uniq(X,L,L) :- member(X,L), !.         % not strongly generic
insert_uniq(X,L,XL) :- member(X,L), !, XL = L.  % logicaly better
insert_uniq(X,L,[X|L]).                         % not member(X,L).


:- pred insert_uniq_old(T, list(T), list(T)).
insert_uniq_old(X,L,L) :- member_old(X,L), !.
insert_uniq_old(X,L,[X|L]).                     % not member_old(X,L).



 
%+++++++++++++++++++++++++++++ tests +++++++++++++++++++++++++++++ 


% tests

:- member(1,[]).     
:- member(1,L).
:- member(1,[1]).
:- member(1,[1,0]).
:- member(1,[-1,2]).   
:- member(1,[-1,-2]).      % ill-typed

:- member_old(1,[-1,-2]).  % ok !!!

%-----

:- 1 = 1.   
:- 1 = 2.
:- 1 = -2.                 % ill-typed

:- equal_old(1,-2).        % ok !!!

%-----

:- insert_uniq(0,X,[1,2]). % ill-typed

:- insert_uniq_old(0,X,[1,2]). % ok !!!

