% Unification by transformation

remove(X,[X|XS],XS).
remove(X,[Y|XS],[Y|ZS]) :- remove(X,XS,ZS).

occurs(X,var(X)).
occurs(X,app(F,TS)) :- occursl(X,TS).
occursl(X, [T|TS]) :- occurs(X, T).
occursl(X, [T|TS]) :- occursl(X, TS).

occurseqs(X, [(T1,T2)|TS]) :- occurs(X, T1).
occurseqs(X, [(T1,T2)|TS]) :- occurs(X, T2).
occurseqs(X, [T|TS]) :- occurseqs(X, TS).

subst(X,T,var(X),T).
subst(X,T,var(Y),var(Y)) :- X \= Y.
subst(X,T,app(F,TS),app(F,US)) :- substl(X,T,TS,US).
substl(X,T,[],[]).
substl(X,T,[R|RS],[U|US]) :- subst(X,T,R,U), substl(X,T,RS,US).

substeqs(X,T,[],[]).
substeqs(X,T,[(R1,R2)|RS],[(U1,U2)|US]) :- subst(X,T,R1,U1), subst(X,T,R2,U2), substeqs(X,T,RS,US).

isvar(var(X)).

solved(QS,[]).
solved(QS,[(var(X),T)|PS]) :-
  not(occurs(X,T)), not(occurseqs(X,PS)), not(occurseqs(X,QS)), solved([(var(X),T)|QS],PS).

zip([],[],[]).
zip([X|XS],[Y|YS],[(X,Y)|ZS]) :- zip(XS,YS,ZS).

transform(PS, QS) :- remove((T, T), PS, QS).
transform(PS, ZS) :- remove((app(F,TS),app(F,US)), PS, RS), zip(TS,US,QS), append(QS,RS,ZS).
transform(PS, [(var(X),T)|QS]) :- remove((T,var(X)), PS, QS), not(isvar(T)).
transform(PS, [(var(X),T)|RS]) :-
  remove((var(X),T), PS, QS), occurseqs(X,QS), not(occurs(X,T)), substeqs(X,T,QS,RS).

solve(PS, PS) :- solved([], PS).
solve(PS, RS) :- not(solved([], PS)), transform(PS, QS), !, solve(QS, RS).

% Test:
%
% solve([(var(x),app(f,[var(a)])),(app(g,[var(x),var(x)]),app(g,[var(x),var(y)]))], PS).
%
% yields
%
% PS = [(var(y), app(f, [var(a)])), (var(x), app(f, [var(a)]))]
%
% solve([(app(f,[var(x),var(x)]),app(f,[var(y),app(g,[var(y)])]))], PS).
%
% fails (because of occurs check).
