pereira@sri-unix.UUCP (08/15/83)
% File : NOT.PL
% Author : R.A.O'Keefe
% Updated: 21 May 1983
% Purpose: "suspicious" negation and double negation
/* This file defines a version of 'not' which checks that there are
no free variables in the goal it is given to "disprove". Bound
variables introduced by the existential quantifier ^ or set/bag
dummy variables are accepted. If any free variables are found,
a message is printed on the terminal and a break level entered.
It is intended purely as a debugging aid, though it shouldn't slow
interpreted code down much. There are several other debugging
aids that you might want to use as well, particularly
unknown(_, trace)
which will detect calls to undefined predicates (as opposed to
predicates which ahve clauses that don't happen to match).
*/
:- public
not/1. % new checking denial
:- mode
explicit_binding(+,+,-,-),
free_variables(+,+,+,-),
free_variables(+,+,+,+,-),
list_is_free_of(+,+),
not(+),
note_free_variable(+,+,+,-),
term_is_free_of(+,+),
term_is_free_of(+,+,+).
not(Goal) :-
free_variables(Goal, [], [], Vars),
Vars \== [], !,
telling(Old), tell(user),
nl, write('** '), write(not(Goal)),
nl, write('-- free variables '), write(Vars),
nl, trace, break,
tell(Old), !,
call(Goal),
!, fail.
not(Goal) :-
call(Goal),
!, fail.
not(_).
% In order to handle variables properly, we have to find all the
% universally quantified variables in the Filter. Any variables
% that are left are universally quantified, unless
% a) they occur in the template
% b) they are bound by X^P, setof, or bagof
% free_variables(Filter, Template, OldList, NewList)
% finds this set, using OldList as an accumulator.
free_variables(Term, Bound, OldList, NewList) :-
var(Term), !,
note_free_variable(Term, Bound, OldList, NewList).
free_variables(Term, Bound, OldList, NewList) :-
explicit_binding(Term, Bound, NewTerm, NewBound), !,
free_variables(NewTerm, NewBound, OldList, NewList).
free_variables(Term, Bound, OldList, NewList) :-
functor(Term, _, N),
free_variables(N, Term, Bound, OldList, NewList).
free_variables(0, Term, Bound, AnsList, AnsList) :- !.
free_variables(N, Term, Bound, OldList, NewList) :-
arg(N, Term, Argument),
free_variables(Argument, Bound, OldList, MidList),
M is N-1, !,
free_variables(M, Term, Bound, MidList, NewList).
% explicit_binding checks for goals known to existentially quantify
% one or more variables. In particular \+ is quite common.
explicit_binding(\+ Test, Bound, fail, Bound ) :- !.
explicit_binding(not(Test), Bound, fail, Bound ) :- !.
explicit_binding(Var^Test, Bound, Test, [Var|Bound]) :- !.
explicit_binding(setof(Var,Test,Set), Bound, (Test,Set), [Var|Bound]) :- !.
explicit_binding(bagof(Var,Test,Set), Bound, (Test,Set), [Var|Bound]) :- !.
% note_free_variable(Var, Bound, OldList, NewList)
% checks a variable Var. If the variable is existentially bound (i.e.
% it occurs in Bound) or already known, no change is made, otherwise
% it is added to the NewList.
note_free_variable(Var, Bound, List, [Var|List]) :-
term_is_free_of(Bound, Var),
list_is_free_of(List, Var), !.
note_free_variable(_, _, List, List).
term_is_free_of(Term, Var) :-
var(Term), !,
Term \== Var.
term_is_free_of(Term, Var) :-
functor(Term, _, N),
term_is_free_of(N, Term, Var).
term_is_free_of(0, Term, Var) :- !.
term_is_free_of(N, Term, Var) :-
arg(N, Term, Argument),
term_is_free_of(Argument, Var),
M is N-1, !,
term_is_free_of(M, Term, Var).
list_is_free_of([Head|Tail], Var) :- !,
Head \== Var, !,
list_is_free_of(Tail, Var).
list_is_free_of([], _).