1:- module(subsumes, [
    2	      subsumes/2,
    3	      op(700, xfx, subsumes),
    4	      subsumes_chk/2,
    5	      compact_lbs/1,
    6	      is_permavar/1
    7	  ]).    8
    9:- 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.

   17subsumes(General, Specific) :-
   18    guardedmap(
   19        guard,
   20        subsumes_,
   21        [General, Specific]).
   22
   23subsumes_(General, Specific) :-
   24    var(General)
   25    ->  add_lb(General, Specific)
   26    ;   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.

   36subsumes_chk(General, Specific) :-
   37    guardedmap(
   38	guard,
   39	subsumes_chk_,
   40	[General, Specific]).
   41
   42subsumes_chk_(General, Specific) :- General == Specific, !.
   43subsumes_chk_(General, _) :- is_permavar(General), !.
   44subsumes_chk_(General, Specific) :-
   45    get_lbs(General, LBs),
   46    member(LB, LBs),
   47    subsumes_chk(LB, Specific).
   48
   49guard(General, Specific) :- var(General) ; var(Specific).
   50
   51subsumes_var(G, S) :-
   52    term_variables(G, GVars),
   53    (any(subsumes_chk(S), GVars)
   54    ->  % S already subsumes some var in G, so G subsumes S implies S = G.
   55        % This avoids nontermination when subsumption would induce cyclic
   56        % data, e.g. `f(X) subsumes Y, Y subsumes X`.
   57        S = G
   58    ;   copy_term_nat(G, S),
   59        term_variables(S, SVars),
   60        GVars subsumes SVars).
   61
   62% Add a lower bound to G.
   63add_lb(G, LB) :-
   64    collapse_cycle(G, LB)
   65    ->  true
   66    ;   get_lbs(G, LBs),
   67        set_lbs(G, [LB|LBs]),
   68        dedup_lbs(G).
   69
   70% Collapse all paths from Cur to End, or fail if no path exists.
   71collapse_cycle(End, Cur) :-
   72    End == Cur
   73    ->  true
   74    ;   get_lbs(Cur, CurLBs),
   75        set_lbs(Cur, []),
   76        % If collapse_cycle(End, LB) doesn't succeed on any LBs, then fail
   77        % because there are no cycles. Otherwise, replace its current LBs
   78        % with just the LBs which didn't cycle.
   79        partition(collapse_cycle(End), CurLBs, [_|_], RemainingLBs),
   80        Cur = End, % Cur has no LBs so this doesn't risk repeating work via attr_unify_hook.
   81        call_dcg((get_lbs, append(RemainingLBs)), End, LBs),
   82        set_lbs(Cur, LBs),
   83        dedup_lbs(Cur).
   84
   85% WARNING: This only works assuming G is var, while the expected behavior
   86% might be that `get_lbs(G, LBs)` is equivalent to `get_lbs(G, LBs), maplist(subsumes(G), LBs)`.
   87get_lbs(G, LBs) :- get_attr(G, subsumes, LBs), !.
   88get_lbs(_, []).
   89
   90% WARNING: This only works assuming G is var, while the expected behavior
   91% might be that `set_lbs(G, LBs)` is equivalent to `set_lbs(G, LBs), maplist(subsumes(G), LBs)`.
   92set_lbs(G, []) :- !, del_attr(G, subsumes).
   93set_lbs(G, LBs) :- put_attr(G, subsumes, LBs).

 compact_lbs(+V) is det

Compact V's lower bounds. Safe, functionally invisible, and completely unnecessary for most use cases. It does forget the original LBs, so it is unsuitable if you need them, which is why it's not automatically applied.

  100compact_lbs(G) :-
  101    is_permavar(G)
  102    ->  set_lbs(G, [every, thing])
  103    ;   dedup_lbs(G).
  104
  105dedup_lbs(G) :-
  106    dedup_lbs_(G, LBs),
  107    set_lbs(G, LBs).
  108
  109dcg_peek_state(X, X, X).
  110
  111dedup_lbs_ -->
  112    dcg_peek_state(G),
  113    % Consider merging mergeable LBs, and maybe mark dummy variables in their attributes.
  114    get_lbs,
  115    sort, % dedup
  116    ignore(selectchk_eq(G)). % remove G from its own LBs, if present.

 is_permavar(+V) is semidet

Succeeds if V's nonvar LBs antiunify to a var. This is equivalent to e.g. subsumes_chk(G, apple), subsumes_chk(G, orange).

  122is_permavar(V) :-
  123    call_dcg((get_lbs, include(nonvar), foldl1(term_subsumer)), V, LGG),
  124    var(LGG).
  125
  126attr_unify_hook(LBs, Y) :- maplist(subsumes(Y), LBs).
  127
  128attribute_goals(G) -->
  129    { dedup_lbs(G),
  130      get_lbs(G, LBs),
  131      attribute_goals_(LBs, G, Goals) },
  132    Goals.
  133
  134attribute_goals_([],  _, []) :- !.
  135attribute_goals_([S], G, [subsumes:subsumes(G, S)]) :- !.
  136attribute_goals_(LBs, G, [maplist(subsumes:subsumes(G), LBs)]).
  137
  138%%% UTILS %%%
  139
  140foldl1(Goal, [V0|List], V) :-
  141    foldl(Goal, List, V0, V).
  142
  143member_eq(A, Bs) :-
  144    member(B, Bs),
  145    A == B,
  146    !.
  147
  148ignore(G) --> G, !.
  149ignore(_) --> [].

 selectchk_eq(+Elem)// is semidet

Removes the first occurrence of Elem. Equality is tested with ==.

  154selectchk_eq(X) --> [Y], { X == Y }, !.
  155selectchk_eq(X), [Y] --> [Y], selectchk_eq(X).
  156
  157any(G, Xs) :-
  158    member(X, Xs),
  159    call(G, X)