% File : NOT.PL
% Author : R.A.O'Keefe
% Updated: 17 November 1983
% Purpose: "suspicious" 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 have clauses that don't happen to match).
The predicate free_variables/4 defined in this files is also used
by the set_of/bag_of code.
Note: in Dec-10 Prolog you should normally use "\+ Goal" instead
of "not(Goal)". In C-Prolog you can use either, and would have to
do some surgery on pl/init to install this version of "not". The
reason that I have called this predicate "not" is so that people
can choose whether to use the library predicate not/1 (in Invoca.Pl)
or this debugging one, not because I like the name.
*/
:- public
(not)/1. % new checking denial
:- mode
explicit_binding(+,+,-,-),
free_variables(+,+,+,-),
free_variables(+,+,+,+,-),
list_is_free_of(+,+),
not(+),
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, 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 Generator. All variables
% as yet unbound are universally quantified, unless
% a) they occur in the template
% b) they are bound by X^P, setof, or bagof
% free_variables(Generator, Template, OldList, NewList)
% finds this set, using OldList as an accumulator.
free_variables(Term, Bound, VarList, [Term|VarList]) :-
var(Term),
term_is_free_of(Bound, Term),
list_is_free_of(VarList, Term),
!.
free_variables(Term, Bound, VarList, VarList) :-
var(Term),
!.
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, VarList, VarList) :- !.
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(\+ Goal, Bound, fail, Bound ) :- !.
explicit_binding(not(Goal), Bound, fail, Bound ) :- !.
explicit_binding(Var^Goal, Bound, Goal, Bound+Var) :- !.
explicit_binding(setof(Var,Goal,Set), Bound, Goal-Set, Bound+Var) :- !.
explicit_binding(bagof(Var,Goal,Bag), Bound, Goal-Bag, Bound+Var) :- !.
explicit_binding(set_of(Var,Goal,Set), Bound, Goal-Set, Bound+Var) :- !.
explicit_binding(bag_of(Var,Goal,Bag), Bound, Goal-Bag, Bound+Var) :- !.
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([], _).