Third attempt. This is mainly a bugfix in a previous answer (which already had many modifications).
Edit: 06/04/2015
When creating a more general term I was leaving both subterms as-is if either of them was a variable. Now I build a more general term for the “other” subterm in this case, by calling term_general/2.
unify_sto(X,Y):-
unify_with_occurs_check(X,Y) -> true ;
(
term_general(X, Y, unify(X,Y), XG, YG),
\+unify_with_occurs_check(XG,YG),
throw(error(type_error(acyclic, unify(X,Y)),_))
).
term_general(X, Y, UnifyTerm, XG, YG):-
(var(X) -> (XG=X, term_general(Y, YG)) ;
(var(Y) -> (YG=Y, term_general(X, XG)) ;
((
functor(X, Functor, Len),
functor(Y, Functor, Len),
X=..[_|XL],
Y=..[_|YL],
term_general1(XL, YL, UnifyTerm, NXL, NYL)
) ->
(
XG=..[Functor|NXL],
YG=..[Functor|NYL]
) ;
( XG=_, YG=_ )
))).
term_general1([X|XTail], [Y|YTail], UnifyTerm, [XG|XGTail], [YG|YGTail]):-
term_general(X, Y, UnifyTerm, XG, YG),
(
\+(unify_with_occurs_check(XG,YG)) ->
throw(error(type_error(acyclic,UnifyTerm),_)) ;
term_general1(XTail, YTail, UnifyTerm, XGTail, YGTail)
).
term_general1([], [], _, [], []).
term_general(X, XG):-
(var(X) -> XG=X ;
(atomic(X) -> XG=_ ;
(
X=..[_|XL],
term_general1(XL, XG)
))).
term_general1([X|XTail], [XG|XGTail]):-
term_general(X, XG),
term_general1(XTail, XGTail).
term_general1([], _).
And here the unit tests so far mentioned in this question:
unit_tests:-
member([TermA,TermB], [[_A+_B,_C+_D], [_E+_F, 1+2],
[a(_G+1),a(1+_H)], [a(1), b(_I)],
[A+A,a(B)+b(B)], [A+A,a(B,1)+b(B)]]),
(unify_sto(TermA, TermB)->Unifies=unifies ; Unifies=does_not_unify),
writeln(test(TermA, TermB, Unifies)),
fail.
unit_tests:-
member([TermA,TermB], [[A+A,B+a(B)], [A+A,A+b(A)],
[A+A,a(_)+b(A)], [1+A,2+s(A)],
[a(1)+X,b(1)+s(X)]]),
catch(
(
(unify_sto(TermA, TermB)->true;true),
writeln(test_failed(TermA, TermB))
), E, writeln(test_ok(E))),
fail.
unit_tests.