% Purpose: find a definiton for subsumes_term/2 with minimal
% errors

subsumes_term_V1(General, Specific) :-
	(	term_attvars(General+Specific, [_|_])
	->	throw(error(subsumption_error,_))
	;	subsumes_chk(General, Specific)
	).

% Problematic error:
% ?- dif(X,_), subsumes_term_V1(c,g(X)).
% ?- dif(X,_), subsumes_term_V1(X,X).

subsumes_term_syntactically(General, Specific) :-
	copy_term_nat(General+Specific,GeneralC+SpecificC),
	subsumes_chk(GeneralC,SpecificC). % the old subsumes_chk

subsumes_term_V2(General, Specific) :-
	(	?=(General, Specific)
	->	General == Specific
	;	term_attvars(General+Specific, [_|_])
	->	throw(error(subsumption_error,_))
	;	subsumes_term_syntactically(General, Specific)
	).

% Problematic error:
% ?- dif(X,_), subsumes_term_V2(f(X,a), f(X,_)).

subsumes_term_V3(General, Specific) :-
	unifiable(General, Specific, Equations),
	(	term_attvars(Equations, [_|_])
	->	throw(error(subsumption_error,_))
	;	subsumes_term_syntactically(General, Specific)
	).

% Problematic error:
% ?- dif(X,a), subsumes_term_V3(f(X),_).

eqsvars([]) -->
	[].
eqsvars([A=B|Eqs]) -->
	( {var(A)} -> [A] ; [] ),
	( {var(B)} -> [B] ; [] ),
	eqsvars(Eqs).

syntacticterms([]) -->
	[].
syntacticterms([T|Ts]) -->
	( {term_attvars(T,[])} -> [T] ; [] ),
	syntacticterms(Ts).

subsumes_term_V4(General, Specific) :-
	unifiable(General, Specific, Equations),
	(	phrase(eqsvars(Equations),Vars),
		term_attvars(Vars, [_|_])
	->	throw(error(subsumption_error,_))
	;	subsumes_term_syntactically(General, Specific)
	).

% Problematic error:
% ?- dif(X,a), subsumes_term_V4(f(X,f(_)),f(a,_)).

subsumes_term_V5(General, Specific) :-
	unifiable(General, Specific, Equations),
	(	Equations = [_|_],
		phrase(eqsvars(Equations),Vars), % Subterms are not considered
		term_attvars(Vars, [_|_]),       % There are constraints involved somehow
		term_variables(Specific, SpecificVars),
		% Unrelated, unconstrained terms that that would cause for themselves
		% failure of subsumes_term
		\+ (	member(A=B,Equations),
			term_attvars(A,[]), % var(A) implicit
		   	nonvar(B),
			member(SVar, SpecificVars),
			A == SVar
		),
		\+ (	phrase(syntacticterms(Equations), SyntacticEquations),
		   	maplist(call,SyntacticEquations),
			term_variables(SpecificVars, SpecificVars2),
			SpecificVars \== SpecificVars2
		)
		\+ (
		   % Only constraints in Specific
		        term_attvars(Specific,[_|_]), % redundant
		    	term_attvars(General,[]),
			
		)
	->	throw(error(subsumption_error,_))
	;	subsumes_term_syntactically(General, Specific)
	).

% Is this the optimum?

% 2009-11-22
% ?- dif(Y,a),subsumes_term_V5(X,Y).
% would work for dif/2.  But in general?