/*  NUMBERVARS.PL  */
 
 
:- module numbervars.
 
 
:- public numbervars/3.                    
 
 
/*
SPECIFICATION
-------------
 
PUBLIC numbervars( Term+, I1+, I2- ):
       numbervars( Term+, I1+, I2+ ):
 
I've provided this for compatibility with systems that lack it: in
Poplog, C-Prolog, Quintus, and many others, it exists already.
 
'numbervars' causes all the variables in Term to be instantiated to
terms of the form '$VAR'(N), where N is an integer. Non-sharing
variables are allocated different integers. The variable numbers go from
I1 to I2 - 1. I1 must initially be instantiated, but I2 need not.
 
Example:
 
    ?- numbervars( a(A,B)+b(B,C), 10, I2 ).
    A = '$var'(10)
    B = '$var'(11)
    C = '$var'(12)
    I2 = 13
 
I don't know whether other Prologs guarantee that the variables are
numbered in a given order. Probably best not to rely on it.
 
Note: in Poplog, some versions of ESL Prolog, and possibly other
systems, terms of the form '$VAR'(X) are treated specially by write,
writeq and display. These predicates just output X.
 
 
The Tutor calls "numbervars" when it needs to treat clauses not as code
to be executed, but as terms in their own right. To do so soundly, all
the atomic components of such terms have to be logical constants: i.e.
on the same footing as numbers or atoms. This can be illustrated by
considering the "delete Fact" variant of the "delete" command, as in
    delete X loves Y.
 
Suppose we have in the textbase the facts
    adrian loves robin.
    edmund loves X.
    Z loves Z.
    A loves B.
 
Now, the specification of "delete Fact" is that it should delete the
first fact which is textually identical to "Fact". As explained in
comments to the editor, this criterion is satisfactorarily approximated
by requiring that it delete the first fact that strictly matches Fact.
 
    F1 strictly matches F2
means we take the first variable in F1 and replace all occurrences of it
by some unique term --- say var_(1) --- that doesn't occur elsewhere in
F1 or F2. We then replace the next variable by another unique term ---
var_(2) --- ; and we continue for as long as there remain unbound
variables in F1. We then do the same to F2. If after this the facts
match, they strictly match one another.
 
Carrying out this procedure, "A loves A" and "B loves B" both become
    var_(1) loves _var(1)_,
and hence strictly match one another. However, they would not strictly
match "A loves B" or "X loves Y",
which would both become
    var_(1) loves _var(2)_.
What this is saying is that we want a way of re-representing a term such
that the variables in it behave like constants under equality: A must =
A, but we do not want it to = B (unless A and B are sharing). You can
hack this with "==", but I prefer "numbervars", which (in my version)
carries out the replacement outlined above, except that the terms are
generally '$var'(N) and not var_(N).
 
"numbervars" is also used inside the AND-OR tree interpreter, and for
the same reason.      
*/
 
 
/*
IMPLEMENTATION
--------------
 
This is a straightforward term-crunching predicate. numbervars/3 calls
numbervars/5: the latter has two accumulator arguments, one for the
greatest number so far, and one for the list of variables.
 
numbervarsl deals with argument lists.
 
membervar checks whether a list contains a given variable: it has to use
== rather than unification.
*/
 
 
numbervars( X, I1, I2 ) :-
    numbervars( X, I1, I2, [], _ ).
 
 
numbervars( X, N0, N0, Vars0, Vars0 ) :-
    atomic(X),
    !.
 
numbervars( V, N0, N0, Vars0, Vars0 ) :-
    var(V),
    membervar( V, Vars0 ),
    !.
 
numbervars( V, N0, N, Vars0, [V|Vars0] ) :-
    var( V ),
    !,
    V = '$var'(N0),
    N is N0 + 1.
 
numbervars( X, N0, N, Vars0, Vars ) :-
    X =.. [ _ | Args ],
    numbervarsl( Args, N0, N, Vars0, Vars ).
 
 
numbervarsl( [], N0, N0, Vars0, Vars0 ).
 
numbervarsl( [H|T], N0, N, Vars0, Vars ) :-
    numbervars( H, N0, N1, Vars0, Vars1 ),
    numbervarsl( T, N1, N, Vars1, Vars ).
 
 
membervar( V, [V_|_] ) :-
    V == V_,
    !.
 
membervar( V, [_|T] ) :-
    membervar( V, T ).
 
 
:- endmodule.
