/*********************************************************/
/*               UNIFICATION ALGORITHM                   */
/*                                                       */
/* Taken from Sterling & Shapiro, with minor changes,    */
/* pages 151-152.                                        */
/*                                                       */
/* Example uses are:                                     */
/* ?- unif(f(a), X).                                    */
/* ?- unif(f(a, g(X)), f(Y, Z))                         */
/* Compare the result of these with the in-built Prolog  */
/* unification, i.e.:                                    */
/* ?- f(a)=X.                                            */
/* ?- f(a, g(X)) = f(Y, Z)                               */
/* In particular, to see the effect of the occurs check, */
/* compare the following:                                */
/* ?- unif(f(X), X).                                    */
/* ?- f(X)=X.                                            */
/*********************************************************/

unif(X, Y) :-
   var(X), var(Y), X=Y.

unif(X, Y) :-
   var(X), nonvar(Y), not_occurs_in(X, Y), X=Y.

unif(X, Y) :-
   var(Y), nonvar(X), not_occurs_in(Y, X), Y=X.

unif(X, Y) :-
   nonvar(X), nonvar(Y), constant(X), constant(Y), X=Y.

unif(X, Y) :-
   nonvar(X), nonvar(Y), compound(X), compound(Y), term_unif(X, Y).

not_occurs_in(X, Y) :-
   var(Y), X \== Y.

not_occurs_in(X, Y) :-
   nonvar(Y), constant(Y).

not_occurs_in(X, Y) :-
   nonvar(Y), compound(Y), functor(Y, F, N), not_occurs_in(N, X, Y).

not_occurs_in(N, X, Y) :-
   N > 0, arg(N, Y, Arg), not_occurs_in(X, Arg), N1 is N - 1,
   not_occurs_in(N1, X, Y).

not_occurs_in(0, X, Y).

term_unif(X, Y) :-
   functor(X, F, N), functor(Y, F, N), unif_args(N, X, Y).

unif_args(N, X, Y) :-
   N > 0, unif_arg(N, X, Y), N1 is N - 1, unif_args(N1, X, Y).

unif_args(0, X, Y).

unif_arg(N, X, Y) :-
   arg(N, X, ArgX), arg(N, Y, ArgY), unif(ArgX, ArgY).

constant(X) :- integer(X).

constant(X) :- atom(X).

compound(X) :- not atomic(X).