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:

For each relevant module M, M:verify_attributes/3 is called, collecting a list of returned Goals.

The variable binding is redone.

Any Goals are called.

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!

I don't have SICStus Prolog, would a meta-interpreter qualifies as an answer (the interface is almost equivalent to `atts`, only `get_atts/2` and `put_atts/2`, may be wrong)? Are you implementing an engine? — notoria, Dec 07 '22 at 18:19
@notoria. With the SICStus interface, solvers are invoked **pre**-unify, that is before any bindings have been performed; Of course a meta-interpreter would be ok, but I guess it's hard to get the *exact* semantics right. — repeat, Dec 07 '22 at 19:48
@notoria. I am implementing a Prolog system with SICStus style extensible unification. — repeat, Dec 07 '22 at 19:50
@notoria. FYI you can get a free one-month test license at https://sicstus.sics.se/eval.html . — repeat, Dec 08 '22 at 09:45
Indeed, I'm trying the [beta](https://sicstus.sics.se/download_beta.html). — notoria, Dec 08 '22 at 09:59
@notoria. Ok, but how? "There are currently no beta releases, see the main Download Page for downloads." :) — repeat, Dec 08 '22 at 10:01
There was one but now it's gone (and I didn't record the page with important information so it can't break before it expires). — notoria, Dec 08 '22 at 10:05
@notoria. No need to get a beta version. Why not a free one-month trial of the latest official release? — repeat, Dec 08 '22 at 10:20

score 8 · Accepted Answer · answered Nov 12 '20 at 08:56

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.

Thanks a lot! The way I see it now the "undo then redo" part is not necessary in my implementation (which only deals with finite trees). Does that sound plausible to you? — repeat, Nov 17 '20 at 16:20

score 1 · Answer 2 · answered Dec 07 '22 at 21:58

This is the meta-interpreter:

:- use_module(library(lists), [append/2,append/3,maplist/2,maplist/3,member/2,select/3]).

% Source: https://sicstus.sics.se/sicstus/docs/3.7.1/html/sicstus_17.html
% Source: https://sicstus.sics.se/sicstus/docs/latest4/html/sicstus.html/lib_002datts.html#lib_002datts

element(Es, E) :-
    member(E, Es).

get_atts(S, _, _, _, _, _) :-
    var(S),
    throw(error(instantiation_error,get_atts/3)).
get_atts(_, V, _, _, _, _) :-
    nonvar(V),
    throw(error(uninstantiation_error,get_atts/3)).
get_atts(+, V, D, G_3, As0, As) :-
    element(As0, s(V0,D0,G0_3)),
    V == V0,
    \+ \+ s(V,D,G_3) = s(V0,D0,G0_3), !,
    mi([s(V0,D0,G0_3) = s(V,D,G_3)], As0, As).
get_atts(-, V, D, G_3, As0, _) :-
    element(As0, s(V0,D0,G0_3)),
    V == V0,
    \+ \+ s(V,D,G_3) = s(V0,D0,G0_3),
    mi([s(V0,D0,G0_3) = s(V,D,G_3)], As0, _), !,
    false.
get_atts(-, _, _, _, As, As).

put_atts(S, _, _, _, _, _) :-
    var(S),
    throw(error(instantiation_error,put_atts/3)).
put_atts(_, V, _, _, _, _) :-
    nonvar(V),
    throw(error(uninstantiation_error,put_atts/3)).
put_atts(_, _, D, _, _, _) :-
    var(D),
    throw(error(instantiation_error,put_atts/3)).
put_atts(+, V, D, G_3, As0, [s(V,D,G_3)|As]) :-
    functor(D, A, N),
    functor(D0, A, N),
    select(s(V0,D0,_), As0, As),
    V == V0, !.
put_atts(+, V, D, G_3, As, [s(V,D,G_3)|As]).
put_atts(-, V, D, G_3, As0, As) :-
    select(s(V0,D0,G0_3), As0, As1),
    V == V0,
    \+ \+ s(V,D,G_3) = s(V0,D0,G0_3),
    mi([s(V0,D0,G0_3) = s(V,D,G_3)], As1, As), !.
put_atts(-, _, _, _, As, As).




mi(G, As) :-
    mi([G], [], As).

mi([], As, As).
mi([G|_], _, _) :-
    var(G),
    throw(error(instantiation_error,mi/3)).
mi([G|_], As, _) :-
    false,
    writeq([G,As]), nl,
    false.
mi([false|_], _, _) :-
    !,
    false.
mi([true|Gs], As0, As) :-
    !,
    mi(Gs, As0, As).
mi([G0|Gs], As0, As) :-
    functor(G0, call, N),
    N @> 0,
    G0 =.. [call,F|Bs0], !,
    F =.. Bs1,
    append(Bs1, Bs0, Bs),
    G =.. Bs,
    mi([G|Gs], As0, As).
mi([(G0, G)|Gs], As0, As) :-
    !,
    mi([G0,G|Gs], As0, As).
mi([(G ; _)|Gs], As0, As) :-
    G \= (_->_),
    mi([G|Gs], As0, As).
mi([(G0 -> G ; _)|Gs], As0, As) :-
    mi([G0], As0, As1), !,
    mi([G|Gs], As1, As).
mi([(_ ; G)|Gs], As0, As) :-
    !,
    mi([G|Gs], As0, As).
mi([(G0 -> G)|Gs], As0, As) :-
    mi([G0], As0, As1), !,
    mi([G|Gs], As1, As).
mi([catch(G0, E, G)|Gs], As0, As) :-
    catch(mi([G0|Gs], As0, As), E, mi([G|Gs], As0, As)).
mi([throw(E)|_], _, _) :-
    throw(E).
mi([A \= B|_], As, _) :-
    mi([A = B], As, _), !,
    false.
mi([_ \= _|Gs], As0, As) :-
    !,
    mi(Gs, As0, As).
mi([get_atts(Mode, V, D, G_3)|Gs], As0, As) :-
    !,
    get_atts(Mode, V, D, G_3, As0, As1),
    mi(Gs, As1, As).
mi([put_atts(Mode, V, D, G_3)|Gs], As0, As) :-
    !,
    put_atts(Mode, V, D, G_3, As0, As1),
    mi(Gs, As1, As).
% mi([G0|_], _, _) :-
%     functor(G0, A, N),
%     \+ pi(A, N), !,
%     throw(error(existence_error(procedure,A/N),mi/3)).
mi([G0|Gs0], As0, As) :-
    copy_term(G0, G),
    head_body(G, Gs, Gs0),
    unify(G0, G, As0, As1),
    mi(Gs, As1, As).

unify(G0, G, As0, As) :-
    maplist(arg(1), As0, Vs0),
    sort(Vs0, Vs),
    unify_(G0, G, Vs, As0, As).

unify_(G, G, Vs, As0, As) :-
    maplist(var, Vs),
    term_variables(Vs, Vs), !,
    As0 = As.
unify_(G0, G, Vs, As0, As) :-
    unifiable(G0, G, Eqs0),
    shrink_equations(Vs, Eqs0, Eqs),
    gather_attributes_goals(Eqs, As0, As1, Gs),
    G0 = G, % maplist(call, Eqs),
    filter_attributes(As1, As2),
    mi(Gs, As2, As).

shrink_equations(_, [], []).
shrink_equations(Vs, [Eq|Eqs0], Eqs) :-
    call(Eq),
    maplist(var, Vs),
    term_variables(Vs, Vs), !,
    shrink_equations(Vs, Eqs0, Eqs).
shrink_equations(Vs, [Eq|Eqs0], [Eq|Eqs]) :-
    shrink_equations(Vs, Eqs0, Eqs).

unifiable(X, Y, Eqs) :-
    \+ \+ X = Y,
    unifiable_([X], [Y], Eqs, Eqs, []).

unifiable_([], [], _, Eqs, Eqs).
unifiable_([X|Xs], [Y|Ys], Eqs0, Eqs1, Eqs) :-
    nonvar(X),
    nonvar(Y), !,
    functor(X, A, N),
    functor(Y, A, N),
    X =.. [A|Xs0],
    Y =.. [A|Ys0],
    unifiable_(Xs0, Ys0, Eqs0, Eqs1, Eqs2),
    unifiable_(Xs, Ys, Eqs0, Eqs2, Eqs).
unifiable_([X|Xs], [Y|Ys], Eqs0, Eqs1, Eqs) :-
    element([X=Y,Y=X], Eq),
    \+ maplist(\==(Eq), Eqs0), !,
    unifiable_(Xs, Ys, Eqs0, Eqs1, Eqs).
unifiable_([X|Xs], [Y|Ys], Eqs0, [X=Y|Eqs1], Eqs) :-
    unifiable_(Xs, Ys, Eqs0, Eqs1, Eqs).

gather_attributes_goals(Eqs, As0, As, Gs) :-
    gather_attributes_goals_(Eqs, As0, As, Gss, []),
    append(Gss, Gs).

gather_attributes_goals_([], As, As, Gss, Gss).
gather_attributes_goals_([X=Y|Eqs], As0, As, Gss0, Gss) :-
    % TODO: Investigate `==(X)` and `==(Y)`, since goals are executed.
    filter(ar(1, ==(X)), As0, SubAs0),
    maplist(arg(3), SubAs0, Gs0),
    execute_attributes(Gs0, X, Y, As0, As1, Gss0, Gss1),

    filter(ar(1, ==(Y)), As1, SubAs1),
    maplist(arg(3), SubAs1, Gs1),
    execute_attributes(Gs1, Y, X, As1, As2, Gss1, Gss2),

    gather_attributes_goals_(Eqs, As2, As, Gss2, Gss).

execute_attributes([], _, _, As, As, Gss, Gss).
execute_attributes([G_3|Gs], X, Y, As0, As, [Gs0|Gss0], Gss) :-
    mi([call(G_3, X, Y, Gs0)], As0, As1),
    execute_attributes(Gs, X, Y, As1, As, Gss0, Gss).

filter_attributes([], []).
filter_attributes([s(V,_,_)|As0], As) :-
    nonvar(V), !,
    filter_attributes(As0, As).
filter_attributes([s(V,D,_)|As0], As) :-
    var(V),
    functor(D, A, N),
    functor(D0, A, N),
    element(As0, s(V0,D0,_)),
    V == V0, !,
    filter_attributes(As0, As).
filter_attributes([A|As0], [A|As]) :-
    filter_attributes(As0, As).

ar(N, G_1, A0) :-
    arg(N, A0, A),
    call(G_1, A).

filter(_, [], []).
filter(G_1, [L|Ls0], Ms) :-
    call(G_1, L), !,
    Ms = [L|Ls],
    filter(G_1, Ls0, Ls).
filter(G_1, [_|Ls0], Ls) :-
    filter(G_1, Ls0, Ls).


head_body(true, Rs, Rs).
head_body(A=A, Rs, Rs).
head_body(element([A|_], A), Rs, Rs).
head_body(element([_|As], A), [element(As, A)|Rs], Rs).
head_body(select(A0, [A0|As], As), Rs, Rs).
head_body(select(A0, [A|As0], [A|As]), [select(A0, As0, As)|Rs], Rs).
head_body(maplist(_, []), Rs, Rs).
head_body(maplist(G_1, [A|As]), [call(G_1, A), maplist(G_1, As)|Rs], Rs).
head_body(p(_), Rs, Rs).
head_body(p(a), Rs, Rs).

head_body(var(T), Rs, Rs) :-
    var(T).
head_body(nonvar(T), Rs, Rs) :-
    nonvar(T).
head_body(T0==T, Rs, Rs) :-
    T0 == T.
head_body(T0\==T, Rs, Rs) :-
    T0 \== T.
head_body(sort(As0,As), Rs, Rs) :-
    sort(As0, As).

head_body(freeze(V, G_0), [(
    (   var(V) ->
        put_atts(+, W, frozen(G_0), freezer),
        W = V
    ;   nonvar(V), call(G_0)
    )
)|Rs], Rs).
head_body(freezer(V, W, Gs), [(
    get_atts(+, V, frozen(G0), _),
    (   var(W) ->
        (   get_atts(+, W, frozen(G1), _) ->
            put_atts(+, V, frozen((G0, G1)), freezer)
        ;   true
        ),
        Gs = []
    ;   Gs = [G0]
    )
)|Rs], Rs).

head_body(domain(V, Dom0), [(
    (   var(Dom0) ->
        get_atts(+, V, dom(Dom0), _)
    ;   maplist(nonvar, Dom0),
        sort(Dom0, Dom),
        Dom = [E|Es],
        (   Es = [] ->
            V = E
        ;   put_atts(+, W, dom(Dom), contraction),
            V = W
        )
    )
)|Rs], Rs).
head_body(contraction(V, W, Gs), [(
    get_atts(+, V, dom(Dom0), _),
    (   var(W) ->
        (   get_atts(+, W, dom(Dom1), _) ->
            intersection(Dom0, Dom1, Dom),
            Dom = [E|Es],
            (   Es = [] ->
                Gs = [W=E]
            ;   put_atts(+, V, dom(Dom), contraction),
                % put_atts(+, W, dom(Dom), contraction),
                Gs = []
            )
        ;   Gs = []
        )
    ;   (   element(Dom0, W) ->
            true
        ;   false
        ),
        Gs = []
    )
)|Rs], Rs).
head_body(intersection(Us, Vs, Ws), [(
    (   (Us = [] ; Vs = []) ->
        Ws = []
    ;   [U|Us0] = Us,
        (   select(V, Vs, Vs0), U == V ->
            [U|Ws0] = Ws
        ;   Vs0 = Vs,
            Ws0 = Ws
        ),
        intersection(Us0, Vs0, Ws0)
    )
)|Rs], Rs).

/*
head_body(dif(X, Y), [(
    X \== Y,
    (   X \= Y ->
        true
    ;   put
    )
)|Rs], Rs).
head_body(differentiator(V, W, Gs), [(
    get_atts(+, V, dif(Vs), _),
    (   var(W) ->
        (   get_atts(+, W, dif(Ws), _) ->
            intersection(Vs, Ws, Xs),
            maplist(differentiate(V, W), Xs, Gs)
        ;   Gs = []
        )
    ;   Gs = []
    )
)|Rs], Rs).
% */

test :-
    writeq(freeze), nl,
    mi(freeze(A,false), As),
    writeq([A,As]), nl,
    false.
test :-
    writeq(freeze), nl,
    mi((freeze(A,false),freeze(A,true)), As),
    writeq([A,As]), nl,
    false.
test :-
    writeq(domain), nl,
    mi((domain(X,[5,6,7,1]),domain(Y,[3,4,5,6]),domain(Z,[1,6,7,8])), As),
    writeq([X,Y,Z,As]), nl,
    false.
test :-
    writeq(domain), nl,
    mi((domain(X,[5,6,7,1]),domain(Y,[3,4,5,6]),domain(Z,[1,6,7,8]),X=Y), As),
    writeq([X,Y,Z,As]), nl,
    false.
test :-
    writeq(domain), nl,
    mi((domain(X,[5,6,7,1]),domain(Y,[3,4,5,6]),domain(Z,[1,6,7,8]),X=Y,Y=Z), As),
    writeq([X,Y,Z,As]), nl,
    false.
test :-
    halt.

For a quick test run test/0.

The predicates of interest are get_atts/6 and put_atts/6. This meta-interpreter doesn't handle module so the interface has been generalized (thus creating new unknown issue).

This hasn't been tested extensively, the predicate gather_attributes_goals/4 may need a deeper inspection. Only freeze/2 and domain/2 has been implemented (but need more testing). Implementing dif/2 could help in testing it. Implementing cut could also help load a library like clpz for testing.

Unification is done with unify/4 where handling the attributed variables begins.

This is the first implementation polished, it's more something to learn how does it work, I still need to work on something better.

`freezer` is a bit broken: `( get_atts(+, W, frozen(G1), _) -> put_atts(+, V, frozen((G0, G1)), freezer) ; true )` should better be `( get_atts(+,W,frozen(G1),_) -> put_atts(+,W,frozen((G0,G1)),freezer) ; put_atts(+,W,frozen(G0),freezer) )` (if you are using the same argument order as SICStus' `verify_attributes/3`). — repeat, Dec 08 '22 at 13:21
Yes, but that unification is *asymmetric*: the attvar `V` will cease to exist. If `W` is an attvar, `V` is demoted to a plain var (pointing to `W`). Thus, all relevant attributes need to be copied from `V` to `W`. — repeat, Dec 08 '22 at 14:10
In this implementation `freezer` doesn't demote variable and which variables remain is decided in `filter_attributes/2`. — notoria, Dec 08 '22 at 14:42
How does `freezer` know which way to copy atts when unifying two vars? — repeat, Dec 08 '22 at 16:05
It doesn't know, in `gather_attributes_goals_/5` `X=Y` and `Y=X` trigger the goals but it seems that without demotion it would be wrong (try `?- freeze(A, false), freeze(A, true)` and print before `filter_attributes/2`). — notoria, Dec 08 '22 at 16:19
First things first. I value your effort and interesting work. But I already *have* an implementation of said extended unification mechanism and so I set the bounty to reward an existing answer. — repeat, Dec 08 '22 at 16:33
I think that's a good way to get to know the quirks of the interface. The devil's in the details. Anyway, solvers using this interface will run (at least) on SICStus Prolog, Scryer Prolog, and MI-Prolog. — repeat, Dec 08 '22 at 16:43

Extending unification, SICStus-style

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

2 Answers2

Extending unification, SICStus-style

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

2 Answers2

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