Extending unification, SICStus-style

Question

I want to understand SICStus-style extensible unification. The User's Manual on library(atts) states that:

Module:verify_attributes(-Var, +Value, -Goals) hook

...
verify_attributes/3 may invoke arbitrary Prolog goals, but Var should not be bound by it. Binding Var will result in undefined behavior.
...
In the case when a single unification binds multiple attributed variables, first all such bindings are undone, then the following actions are carried out for each relevant variable:

1. For each relevant module M, M:verify_attributes/3 is called, collecting a list of returned Goals.
2. The variable binding is redone.
3. Any Goals are called.
4. Any goals blocked on the variable, that has now become unblocked, are called.

So far, I came up with the following interpretation of the above:

• Different verify_attribute/3 handlers hooked on Var, see the same state of Var: All see it "pre_unify".

• verify_attribute/3 must not bind Var, but it may bind other attributed variables.

• These bindings are to be delayed, too, so that the handlers not only see the same state of Var, but of all attributed variables involved.

  Above list of actions entails "5. Force any delayed bindings of attributed variables."

Am I moving in the right direction—is this what "done, then undone, then redone" is all about?  Please help!

Answer 1

That mechanism was originally designed by Christian Holzbaur and implemented by yours truly. Re. your interpretation:

Different verify_attribute/3 handlers hooked on Var, see the same state of Var: All see it "pre_unify".

Right.

verify_attribute/3 must not bind Var, but it may bind other attributed variables.

Right.

These bindings are to be delayed, too, so that the handlers not only see the same state of Var, but of all attributed variables involved.

Wrong. If it binds other attributed variables, the whole extended unification mechanism gets invoked recursively on those variables.

Above list of actions entails "5. Force any delayed bindings of attributed variables."

Wrong.