/****************************************************************
**
**      File            : negation.clpr
**      Module          : negation
**      Language        : clpr version 1.2
**      Purpose         : System predicate extension for CLP(R)
**      Revision        : 2.0a 07/07/93
**      Copyright       : (C) 1991-1993 K J Dryllerakis
**                         Permission is granted to copy, use and
**                         modify this file as long as the header
**                         and copyright notice remains in place
**	Information	: Work on Constructive negation on real 
**			  numbers.
**
******************************************************************/

?-printf("\nCLP(R) System Extension (Module negation):\n ",[]).

/****************************************************************
**
**      Check if the System module is loaded and give warning
**
******************************************************************/

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

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

/****************************************************************
**
**     \+ definition 
**
******************************************************************/
?-writeseq("\\+/1",[]).

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

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

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

/****************************************************************
**
**      do_not
**
******************************************************************/

::-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).

/****************************************************************
**
**     constraint_vars
**
******************************************************************/

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

constraint_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).

/****************************************************************
**
**      complement_of
**
******************************************************************/

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

complement_of(_,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(_,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).

complement_of(X,_):-
	asserta('   ##INV'(X)),   % Dump Constraints on X
	retract('   ##INV'(_)),   % 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)).

find_nonvar_in([X|_],X,[Y|_],Y):-
	nonvar(X), arithmetic(X).
find_nonvar_in([_|Xs],X1,[_|Ys],Y1):-
	find_nonvar_in(Xs,X1,Ys,Y1).

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(_),_):-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([_|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",[]).