1:- module(anti_unify, [anti_unify/3]).    2
    3:- use_module(library(subsumes)).    4:- use_module(library(apply), [maplist/2, maplist/3, include/3]).    5
    6:- use_module(guardedmap).    7
    8%!  anti_unify(?A, ?B, ?LGG) is semidet.
    9%
   10%   anti_unify/3 maintains the relation that `LGG` is the least general
   11%   generalization of `A` and `B`.
   12%
   13%   See the unit tests for examples.
   14anti_unify(A, B, LGG) :-
   15    % It's cleaner to assert subsumption up front,
   16    % even though it traverses LGG more than necessary.
   17    LGG subsumes A,
   18    LGG subsumes B,
   19    myguardedmap(A, B, LGG).
   20
   21% anti_unify(A, B, LGG) assumes that guard(A, B, LGG) has just succeeded.
   22anti_unify_(A, B, LGG), A == B =>
   23    % If A == B then it is its own LGG.
   24    LGG = A.
   25
   26anti_unify_(A, B, LGG), (LGG == A ; LGG == B) =>
   27    % anti_unify(A, LGG, LGG) iff LGG subsumes A, which is already
   28    % enforced, so the "when" clause is superfluous.
   29    true.
   30anti_unify_(A, B, _LGG), nonvar(A), nonvar(B) =>
   31    % If A and B are both nonvar then guard(A, B, LGG) implies that they
   32    % have different functors, so LGG is permavar (can never be nonvar),
   33    % which characterizes its observable behavior and is already enforced
   34    % by its existing subsumption of A and B.
   35    true.
   36anti_unify_(A, B, LGG) =>
   37    Callback = myguardedmap(A, B, LGG),
   38    (var(A)  ->  add_callback(A, Callback) ; true),
   39    (var(B)  ->  add_callback(B, Callback) ; true).
   40
   41guard(A, B, _LGG) :-
   42    once(A == B ;
   43         var(A) ;
   44         var(B) ;
   45         \+ same_functor(A, B)).
   46
   47myguardedmap(A, B, LGG) :- guardedmap(guard, anti_unify_, A, B, LGG).
   48
   49get_callbacks(Var, Cs) :-
   50    get_attr(Var, anti_unify, Cs0)
   51    ->  Cs = Cs0
   52    ;   Cs = [].
   53
   54set_callbacks(Var, [])        => del_attr(Var, anti_unify).
   55set_callbacks(Var, Callbacks) => put_attr(Var, anti_unify, Callbacks).
   56
   57add_callback(Var, Callback) :-
   58    get_callbacks(Var, Callbacks),
   59    maplist(\==(Callback), Callbacks)
   60    ->  set_callbacks(Var, [Callback|Callbacks])
   61    ;   true.
   62
   63attr_unify_hook(XCallbacks, Y) :-
   64    % Call it all!
   65    maplist(call, XCallbacks),
   66    (var(Y)
   67    ->  get_callbacks(Y, YCallbacks),
   68	set_callbacks(Y, []),
   69	maplist(call, YCallbacks)
   70    ;   true).
   71
   72id3(X, X, X).
   73
   74attribute_goals_ -->
   75    id3(V),
   76    get_callbacks,
   77    maplist(private_public),
   78    include(is_representative_antiunificand(V)).
   79
   80attribute_goals(V) -->
   81    { attribute_goals_(V, Goals) },
   82    Goals.
   83
   84% The callbacks use the non-exported myguardedmap/3 as a slight optimization,
   85% but for attribute_goals//1 we replace it with the exported anti_unify/3.
   86private_public(myguardedmap(A, B, LGG), anti_unify(A, B, LGG)).
   87
   88% Each antiunificand has a copy of the same callback, so we only need to
   89% retain one (in this case, the first nonvar's) as a representative.
   90is_representative_antiunificand(V, anti_unify(A, B, _)) =>
   91    var(A) -> V == A ; V == B.
   92
   93same_functor(A, B), nonvar(A), nonvar(B) =>
   94    functor(A, Name, Arity),
   95    functor(B, Name, Arity)