:- use_module("../prolog/subsumes").
:- begin_tests(subsumes).
test(direct_unresolvable_subsumption_fails) :-
\+ f subsumes g.
test(indirect_unresolvable_subsumption_fails) :-
X subsumes f,
X subsumes g,
\+ g subsumes X.
test(idempotent) :-
maplist(subsumes(X), [f(g),f(g),A,B,A]),
check_lbs(X, [A,B,f(g)]).
test(multiple_cycles_collapsed) :-
X = [A,B,C,A,D],
Y = [B,C,E,D,E],
maplist([V]>>(V subsumes f(V)), X),
X subsumes Y,
% Now induce cycle with two distinct paths: A-B-C-E and A-D-E.
E subsumes A,
% Make sure both paths were collapsed.
maplist(==(A), [B,C,D,E]),
check_lbs(A, [f(A)]).
test(permavar_lbs_compressed) :-
maplist(subsumes(X), [1, 2, 3, 4, 5, 6]),
check_lbs(X, [every, thing]).
test(subsumption_with_directly_induced_cyclic_data_terminates) :-
f(X, Y) subsumes X,
X == f(X, Y).
test(subsumption_with_1_step_indirectly_induced_cyclic_data_terminates2) :-
f(X) subsumes Y,
Y subsumes X.
test(subsumption_with_2_step_indirectly_induced_cyclic_data_terminates) :-
X subsumes Y,
Y subsumes Z,
X = f(Z).
test(subsumption_with_cyclic_data) :-
X = f(X, Y),
X subsumes f(f(A, B), C),
term_variables(A, [Fresh]),
A == f(A, Fresh),
check_lbs(Y, [C, B, Fresh]).
test(subsume_then_unify_leaves_loop) :-
X subsumes Y,
X = Y,
% This is unfortunate but unavoidable, as attr_unify_hook is not called
% when unifying with an unattributed variable. However, it is unobservable
% because compact_lbs/1 is called by attribute_goals//1.
check_lbs(X, [X]).
%%% UTILS %%%
get_lbs(G, LBs) :- get_attr(G, subsumes, LBs), !.
get_lbs(_, []).
check_lbs(G, Expected) :-
get_lbs(G, Actual),
msort(Expected, X),
msort(Actual, X).
:- end_tests(subsumes).