```    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)
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.
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)```