Search code examples
prologunification

Detecting whether proving a predicate unified something

I have a predicate that may unify its arguments, for example:

foo(X) :- X = 42.

How can I tell if, while proving foo(X), unification changed X? For example, I would like to know if writeln(X), foo(X), writeln(X) would print the same value for X twice, without actually doing the printing.

My actual implementation of foo/1 is actually much more complex, so please don't suggest specific to the simplified version above. In my program, foo(X) simplifies X using unification, but foo(X) may need to be proven several times until all simplifications have been performed. I would like to be able to write a foohelper(X) predicate that invokes foo(X) until X stops being unified.

Solution

  • Maybe you can use the standard term_variables/2 predicate? You can call it with your goal before and after calling the goal and check if the returned lists of variables are different. Something like:

    ...,
term_variables(foo(X), Vars0),
foo(X),
term_variables(foo(X), Vars),
(  Vars0 == Vars ->
   write(simplified)
;  write(not_simplified)
),
...