1:- module(subsumes, [
    2	      subsumes/2,
    3	      op(700, xfx, subsumes),
    4	      subsumes_chk/2
    5	  ]).    6
    7:- consult(guardedmap).
 subsumes(?General, ?Specific) is semidet
subsumes/2 maintains the relation that one term subsumes another, according to standard unification of terms.

See the unit tests for examples.

   15subsumes(General, Specific) :-
   16    guardedmap(
   17        guard,
   18        subsumes_,
   19        [General, Specific]).
   20
   21subsumes_(General, Specific) :-
   22    var(General)
   23    ->  add_lb(General, Specific)
   24    ;   subsumes_var(General, Specific).
 subsumes_chk(+General, +Specific) is semidet
Holds if General necessarily subsumes Specific. This predicate fails to be relational when subsumption is induced after it fails:
?- \+ subsumes_chk(G, S), G subsumes S, subsumes_chk(G, S).
G subsumes S.
   34subsumes_chk(General, Specific) :-
   35    guardedmap(
   36	guard,
   37	subsumes_chk_,
   38	[General, Specific]).
   39
   40subsumes_chk_(General, Specific) :- General == Specific, !.
   41subsumes_chk_(General, _) :- permavar(General), !.
   42subsumes_chk_(General, Specific) :-
   43    get_lbs(General, LBs),
   44    member(LB, LBs),
   45    subsumes_chk(LB, Specific).
   46
   47guard(General, Specific) :- var(General) ; var(Specific).
   48
   49subsumes_var(G, S) :-
   50    term_variables(G, GVars),
   51    (any(subsumes_chk(S), GVars)
   52    ->  % S already subsumes some var in G, so G subsumes S implies S = G.
   53        % This avoids nontermination when subsumption would induce cyclic
   54        % data, e.g. `f(X) subsumes Y, Y subsumes X`.
   55        S = G
   56    ;   copy_term_nat(G, S),
   57        term_variables(S, SVars),
   58        GVars subsumes SVars).
   59
   60% Add a lower bound to G.
   61add_lb(G, LB) :-
   62    collapse_cycle(G, LB)
   63    ->  true
   64    ;   get_lbs(G, LBs),
   65        set_lbs(G, [LB|LBs]),
   66        compact_lbs(G).
   67
   68% Collapse all paths from Cur to End, or fail if no path exists.
   69collapse_cycle(End, Cur) :-
   70    End == Cur
   71    ->  true
   72    ;   get_lbs(Cur, CurLBs),
   73        set_lbs(Cur, []),
   74        % If collapse_cycle(End, LB) doesn't succeed on any LBs, then fail
   75        % because there are no cycles. Otherwise, replace its current LBs
   76        % with just the LBs which didn't cycle.
   77        partition(collapse_cycle(End), CurLBs, [_|_], RemainingLBs),
   78        Cur = End, % Cur has no LBs so this doesn't risk repeating work via attr_unify_hook.
   79        call_dcg((get_lbs, append(RemainingLBs)), End, LBs),
   80        set_lbs(Cur, LBs),
   81        compact_lbs(Cur).
   82
   83% WARNING: This only works assuming G is var, while the expected behavior
   84% might be that `get_lbs(G, LBs)` is equivalent to `get_lbs(G, LBs), maplist(subsumes(G), LBs)`.
   85get_lbs(G, LBs) :- get_attr(G, subsumes, LBs), !.
   86get_lbs(_, []).
   87
   88% WARNING: This only works assuming G is var, while the expected behavior
   89% might be that `set_lbs(G, LBs)` is equivalent to `set_lbs(G, LBs), maplist(subsumes(G), LBs)`.
   90set_lbs(G, []) :- !, del_attr(G, subsumes).
   91set_lbs(G, LBs) :- put_attr(G, subsumes, LBs).
   92
   93% compact_lbs(G) just de-dupes G's lower bounds, and removes any self-subsumption. It doesn't merge LBs or remove redundant transitive subsumptions.
   94compact_lbs(G) :-
   95    permavar(G)
   96    ->  true
   97    ;   % Consider merging mergeable LBs, and maybe mark dummy variables in their attributes.
   98        call_dcg((get_lbs, sort, ignore(selectchk_eq(G))), G, LBs),
   99        set_lbs(G, LBs).
 permavar(+V) is semidet
Succeeds if the set of terms subsumed by V contains a pair of nonvars with a var LGG. If so, var(V) must always hold. This is equivalent to e.g. subsumes_chk(G, apple), subsumes_chk(G, orange).
  106permavar(V) :-
  107    call_dcg((get_lbs, include(nonvar), foldl1(term_subsumer)), V, LGG),
  108    var(LGG),
  109    % The following is just an optimization in case LBs is large.
  110    set_lbs(V, [every, thing]).
  111
  112attr_unify_hook(LBs, Y) :- maplist(subsumes(Y), LBs).
  113
  114attribute_goals(G) -->
  115    { compact_lbs(G),
  116      get_lbs(G, LBs),
  117      attribute_goals_(LBs, G, Goals) },
  118    Goals.
  119
  120attribute_goals_([],  _, []) :- !.
  121attribute_goals_([S], G, [G subsumes S]) :- !.
  122attribute_goals_(LBs, G, [maplist(subsumes(G), LBs)]).
  123
  124%%% UTILS %%%
  125
  126foldl1(Goal, [V0|List], V) :-
  127    foldl(Goal, List, V0, V).
  128
  129member_eq(A, Bs) :-
  130    member(B, Bs),
  131    A == B,
  132    !.
  133
  134ignore(G) --> G, !.
  135ignore(_) --> [].
 selectchk_eq(+Elem)// is semidet
Removes the first occurrence of Elem. Equality is tested with ==.
  140selectchk_eq(X) --> [Y], { X == Y }, !.
  141selectchk_eq(X), [Y] --> [Y], selectchk_eq(X).
  142
  143any(G, Xs) :-
  144    member(X, Xs),
  145    call(G, X)