[m-users.] unification of object terms

[Zoltan Somogyi]

On Fri, 4 Mar 2016 11:05:05 +0100, Christophe REY <cjcrey at gmail.com> wrote:
> unify_term(term(T)::in, term(T)::in, substitution(T)::in, substitution(T)::out)
> 
> from the term module.
> 
> Using term_io.read_term, I am able to read object terms, so I have two 
> ground terms for the first two arguments of unify_terms.
> When I call unify_term with the object terms p(X,foo) and p(bar,Y), then 
> it fails. It seems that there cannot be (object) variables inside both 
> terms to unify. When there are variables only inside one term, then it 
> is ok.
> Is it normal ?

It is not normal, but it is exactly what I would expect if you gave
unify_term two terms that you read in separately, and did not do anything
to merge their varsets. That way, p(X, foo) would have X as variable 1,
p(bar, Y) would have Y as variable 1, and the unification would fail
because variable 1 cannot be bound to both bar and foo at the same time.

If you get two terms from two different sources but want to unify them,
(or do any other operation that operates on both terms), you need to
get them to use variables from the same varset first.
The predicate varset.merge_renaming is what you need.
merge_renaming(TermAVarSet, TermBVarSet, BothTermsVarSet,
RenamingFromBToBoth) extends TermAVarSet, adding to it all
the variables in TermBVarSet, and returns the result as BothTermsVarSet.
It also returns the renaming that you apply to TermB; the result will
use the variables in BpthTermsVarSet.
 
Zoltan.