/* UNIFY.

Unification procedure for first order logic (with occurs check)
See p80 of Artificial Mathematicians.

Alan Bundy 10.7.81 */


/* Top Level */

unify(Exp1, Exp2, Subst) :-             % To unify two expressions
        unify(Exp1, Exp2, true, Subst). % Start with empty substitution


/* Unify with output and input substitutions */

unify(Exp, Exp, Subst, Subst).          % If expressions are identical, succeedd

unify(Exp1, Exp2, OldSubst, AnsSubst) :-        % otherwise
        disagree(Exp1,Exp2,T1,T2),      % find first disagreement pair
        make_pair(T1,T2,Pair),          % make a substitution out of them, if pos
        combine(Pair,OldSubst,NewSubst),        % combine this with input subst
        subst(Pair,Exp1,NewExp1),       % apply it to expressions
        subst(Pair,Exp2,NewExp2),
        unify(NewExp1,NewExp2,NewSubst,AnsSubst).       % and recurse



/* Find Disagreement Pair */

disagree(Exp1,Exp2,Exp1,Exp2) :-
        Exp1 =.. [Sym1|_], Exp2 =.. [Sym2|_],   % If exps have different
        Sym1 \== Sym2, !.               % function symbol, then succeed

disagree(Exp1,Exp2,T1,T2) :-                            % otherwise
        Exp1 =.. [Sym|Args1], Exp2 =.. [Sym|Args2],     % find their arguments
        find_one(Args1,Args2,T1,T2).                    % and recurse

/* Find first disagreement pair in argument list */

find_one( [Hd | Tl1], [Hd | Tl2],T1,T2) :- !,   % If heads are identical then
        find_one(Tl1,Tl2,T1,T2).                % find disagreement in rest of list

find_one( [Hd1 | Tl1], [Hd2 | Tl2],T1,T2) :-
        disagree(Hd1,Hd2,T1,T2), !.             % else find it in heads.


/* Try to make substitution out of pair of terms */

make_pair(T1,T2,T1=T2) :-       % T1=T2 is a suitable substitution
        is_variable(T1),        % if T1 is a variable and
        free_of(T1,T2).         % T2 is free of T1

make_pair(T1,T2,T2=T1) :-
        is_variable(T2),        % or if T2 is a variable and
        free_of(T2,T1).         % T1 is free of T2

/* By convention: x,y,z,u,v and w are the only variables */
is_variable(u).         is_variable(v).         is_variable(w).
is_variable(x).         is_variable(y).         is_variable(z).


/* T is free of X */
free_of(X,T) :- occ(X,T,0).     % if X occurs 0 times in T


/* Combine new substitution pair with old substitution */

combine(Pair, OldSubst, NewSubst) :-
        mapand(update(Pair),OldSubst,Subst1),   % apply new pair to old subst
        check_overlap(Pair,Subst1,NewSubst).    % and delete ambiguous assigments

/* Apply new pair to old substitution */
update(Pair, Y=S, Y=S1) :-              % apply new pair to rhs of old subst
        subst(Pair,S,S1).

/* If X is bound to something already then ignore it */
check_overlap(X=T,Subst,Subst) :-       % Ignore X=T
        memberchk(X=S,Subst), !.        % if there already is an X=S

check_overlap(Pair,Subst,Pair & Subst). % otherwise don't


/* MINI-PROJECTS

1.  Simplify unify to a one way matcher, as per p76 of 'Artificial
Mathematicians'.

2.  Generalize Unify to a simultaneous unifier of a set of expressions,
(gen_unify) as per p80 of 'Artificial Mathematicians'.

3.  Build the associativity axiom into unify (assoc_unify), as per p82
of 'Artificial Mathematicians'.

*/