Functional equivalent

IF/Prolog 5 has the following function:
    dif( +Term1, +Term2)

Eclipse has the following function:
   not_unify(?Term1, ?Term2)

dif/2 says:
   The predicate dif/2 succeeds, if Term1 and Term2 are not unifiable
(Prolog predicate =/2).
not_unify/2 says:
   Succeeds if Term1 and Term2 are not unifiable.

However they produced different results, apparently because not_unify does
not suspend:

[user] ?- dif(A, B), A = a(1), B = a(2).
A = a(1)
B = a(2)
yes

?- not_unify(A, B), A = a(1), B = a(2).
No (0.00s cpu)

--

[user] ?- dif(A, B), A = t(A1), B = t(B1), A1 = a, B1 = b.
A = t(a)
B = t(b)
A1 = a
B1 = b
yes

?- not_unify(A, B), A = t(A1), B = t(B1), A1=a, B1=b.
No (0.00s cpu)

-----
How can this function be emulated in Eclipse?

Doug Edmunds
26 Feb 2000
edmunds@pacifier.com

--------
dif( +Term1, +Term2)

The predicate dif/2 succeeds, if Term1 and Term2 are not unifiable (Prolog
predicate =/2).
The predicate fails, if the terms are equal (Prolog predicate ==/2).
Otherwise, the terms are
unifiable but not equal. Since it cannot be immediately determined, if the
terms will always
be unequal, the predicate is suspended. The test is resumed as soon as one
variable in
either of the terms is instantiated.
If the terms are not unifiable after the instantiation, the predicate that
caused the instan-tiation
succeeds. If the terms are equal after the instantiation, the predicate that
caused
the instantiation fails. Otherwise, the terms are still unifiable but not
equal, and the test is
suspended again.

Arguments
Term1 Term
Term2 Term

Example
[user] ?- dif(A, B), A = a(1), B = a(2).
A = a(1)
B = a(2)
yes

[user] ?- A = B, dif(a(A), a(B)).
no

[user] ?- dif(A, B), A = t(A1), B = t(B1), A1 = a, B1 = b.
A = t(a)
B = t(b)
A1 = a
B1 = b
yes

----------
not_unify(?Term1, ?Term2)
Succeeds if Term1 and Term2 are not unifiable.

?Term1
Prolog term.
?Term2
Prolog term.
Description
Succeeds if Term1 and Term2 are not unifiable. This predicate differs from
\=/2 only if metaterms are involved (e.g. with delayed goals or
constraints). While \=/2 does unification, waking of delayed goals and full
constraint propagation to determine unifiability, not_unify/2 uses the
test_unify-handler for this purpose. not_unify/2 is therefore likely to be
cheaper, but possibly less precise (depending on the test_unify-handler)
than \=/2.

Fail Conditions
Fails if Term1 and Term2 can be unified.

Resatisfiable
No.
Exceptions
Examples

Success:
   not_unify(atom, neutron).
   not_unify(1.0, 1).
Fail:
   not_unify(X, Y).
   not_unify(X, 1).
Note the difference:
   coroutine, X > 1, X \= 1.
       % succeeds because the delayed goal X>1 is
       % taken into account
   coroutine, X > 1, not_unify(X, 1).
       % fails because the delayed goal X>1 is
       % ignored by the test_unify handler