/* File:      flrnegation.P
**
** Author(s): Michael Kifer
**
** Contact:   flora-users@lists.sourceforge.net
**
** Copyright (C) The Research Foundation of SUNY, 2003
**
** FLORA-2 is free software; you can redistribute it and/or modify it under the
** terms of the GNU Library General Public License as published by the Free
** Software Foundation; either version 2 of the License, or (at your option)
** any later version.
** 
** FLORA-2 is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
** FOR A PARTICULAR PURPOSE.  See the GNU Library General Public License for
** more details.
** 
** You should have received a copy of the GNU Library General Public License
** along with FLORA-2; if not, write to the Free Software Foundation,
** Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
** 
** 
*/

:- compiler_options([xpp_on]).
#include "flora_porting.flh"
#include "flora_prefix.flh"

#define MAX_NEGATION_NESTING_DEPTH 10000


%% Identical to XSB's sk_not, but allows us to clean up the intermediate
%% tables created while computing the negation

%% Variables temporarily changed to ground and tnot 
%% call is made.  Should give existential semantics to nonground negative
%% calls.  That is
%%	...:- FLORA_TNOT(p(X)),...
%% is like
%%	... :- tnot(pp),...
%%	pp :- p(X).
%% where pp is a new proposition.

:- import numbervars/3, unnumbervars/2 from num_vars.
:- import copy_term/2 from basics.
:- import 't not'/1 from tables.
:- import
	flora_abolish_table_predicate/1,
	flora_abolish_table_call/1
   from flrtables.

:- export
	flora_cleanup_negation/0,
	flora_cleanup_negation/1,
	FLORA_TNOT_PREDICATE/1.

:- table tabled_unnumber_call/1.
:- use_variant_tabling tabled_unnumber_call(_).

FLORA_TNOT_PREDICATE(Goal) :-
	copy_term(Goal,Goal1),
	numbervars(Goal1,0,_),  % is now ground, so no check necessary
	't not'(tabled_unnumber_call(Goal1)).

tabled_unnumber_call(GGoal) :-
	unnumbervars(GGoal,VGoal),
	call(VGoal).

%% Clean up tables introduced for the intermediate resuts in computing negation
flora_cleanup_negation :-
	flora_abolish_table_predicate(tabled_unnumber_call(_)).
flora_cleanup_negation(Call) :-
	flora_abolish_table_call(tabled_unnumber_call(Call)).