%
%	This is the System Extension for CLP(R)
%	Current Module: Negation.
%	Work on Constructive negation on real numbers.
%	For a complete analysis see technical report:
%		Constructive Negation in CLP languages
%	All work copyright 1991-1992 by K J Dryllerakis
%	Permission is granted to freely modify and distribute the
%	code if it is accompanied by this header.
%
?-printf("\n CLP(R) System Extension (MODULE: negation):\n ",[]).

::-not('  ##system loaded'),
	printf("\n ************** Warning: System module is not loaded **********\n",[]),
	printf("************** Negation will not work. Load System ***********\n",[]).

::-dynamic('   ##INV',1).
::-op(60,fx,do_not).

::-writeseq("\\+/1",[]).

::-op(60,fx,\+).
\+ X :- do_not X.
::-prot(\+,1).

::-writeseq("do_nbf/1",[]).

do_nbf(Goal):-
	call(Goal),
	!,
	fail.
do_nbf(Goal).
::-prot(do_nbf,1).

::-writeseq("do_not/1",[]).

do_not(Goal):-
	ground(Goal),
	!,
	do_nbf(Goal).
do_not(Goal):-
	varsin(quote(Goal),Vars),
	!,
	(arithmetics(Vars) ->
		find_all(Vars,Goal,SolutionList),
		inverse_constraint_list(SolutionList,InvertedList),
		constraint_vars(Vars,InvertedList)
	;
		write("Your free variables are not of arithmetic type"),nl,
		write("If you think it should be include a real(Var) predicate"),nl,
		write("I will try unsafe negation"),nl,
		do_nbf(Goal)
	).
::-prot(do_not,1).

::-writeseq("constraint_vars/2",[]).

constraint_vars(Vars,[]).
constraint_vars(Vars,[LVars|MoreVars]):-
	constraint_all_vars(Vars,LVars),
	constraint_vars(Vars,MoreVars).
constraint_all_vars([],[]).
constraint_all_vars([X|Xs],[CX|CXs]):-
	X=CX,
	constraint_all_vars(Xs,CXs).
inverse_constraint_list([],[]).
inverse_constraint_list([X|Xs],[XX|XXs]):-
	complement_of(X,XX),
	inverse_constraint_list(Xs,XXs).

::-writeseq("complement_of/2",[]).

complement_of(X,Y):-
	nonvars(Y),	% Y is not a list of vars!
	write("Wrong Usage of complement_of/2 second arg is not a list of vars"),nl,
	!,
	fail.
complement_of(X,Y):-
	arithmetics(Y),% Y is a list that contains arithmetic terms
	write("Wrong Usage of complement_of/2 second arg is arithmetic"),nl,
	!,
	fail.
complement_of(X,Y):-
	find_nonvar_in(X,Num,Y,Rnum),
       (Rnum<Num ; Rnum>Num).

find_nonvar_in([X|Xs],X,[Y|Ys],Y):-
	nonvar(X), arithmetic(X).
find_nonvar_in([X|Xs],X1,[Y|Ys],Y1):-
	find_nonvar_in(Xs,X1,Ys,Y1).
complement_of(X,Y):-
	asserta('   ##INV'(X)),   % Dump Constraints on X
	retract('   ##INV'(M)),   % If this succeeds no constraints on X!
	!,
	fail.
complement_of(X,Y):-
	arithmetics(X), % test already performed
	list_of_reals(X,Y),
	retract('   ##INV'(X):- CX),      % CX are the quoted constraints on X
	r_c_on(X,CX,Y,CY),
	call(eval(CY)).
r_c_on(X,(A,B),Y,(C;D)):-
	arithmetics(Y), % test already performed
	!,
	r_c_on(X,A,Y,C),
	r_c_on(X,B,Y,D).

r_c_on(X,A,Y,C):-
	copy_replace(X,quote(A),Y,C1),
	inv_co(eval(C1),quote(C)).

inv_co(abs(X-Y)>0,X=Y).
inv_co(X=Y,X<>Y).
inv_co(X>Y,X<=Y).
inv_co(X<Y,X>=Y).
inv_co(X<=Y,X>Y).
inv_co(X>=Y,X<Y).
inv_co(real(X),_):-fail.

arithmetics([X]):-arithmetic(X).
arithmetics([X|Xs]):-
	arithmetic(X),
	arithmetics(Xs).
nonvars([X]):- nonvar(X).
nonvars([X|Z]):- nonvar(X),nonvars(Z).
list_of_reals([],[]).
list_of_reals([X|Xs],[Y|Ys]):-
	real(Y),
	list_of_reals(Xs,Ys).
::-prot(constraint_vars,2),prot(constraint_all_vars,2),
	prot(inverse_constraint_list,2),prot(complement_of,2),
	prot(find_nonvar_in,4),prot(r_c_on,4),prot(inv_co,2),
	prot(arithmetics,1),prot(nonvars,1),prot(list_of_reals,2).

'  ##negation loaded'.
::-prot('  ##negation loaded',0).
::-writeseq("done\n",[]).