% 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?