% unify(+Term1, +Term2, -List)
%   Returns an mgu of Term1 and Term2 in List
%       if they are unifiable.
%   Fails otherwise.
%
% Variables in the unification problems are represented as Prolog
% constants that end with the underscore.
% Example: unify(f(x_,g(a)), f(b,g(y_)), Mgu).

unify(Term1, Term2, Unifier):-
    unify_list([[Term1,Term2]], [], Unifier),
    !.

% Nothing to be done

unify_list([], Acc, Acc).


% Trivial

unify_list([[X,X]|Rest], Acc, Unifier):-
   !,
   unify_list(Rest, Acc, Unifier).

% Variable Elimination

unify_list([[T1,T2]|Rest], Acc, Unifier):-
     variable(T1),
     !,
     \+(occurs(T1, T2)),
     apply_substitution(Rest, [T1 -> T2], Instance_of_Rest),
     compose_substitutions(Acc, [T1 -> T2], Acc1),
     unify_list(Instance_of_Rest, Acc1, Unifier).


% Orient

unify_list([[T1,T2]|Rest], Acc, Unifier):-
     variable(T2),
     !,
     unify_list([[T2,T1]|Rest], Acc, Unifier).


% Decomposition

unify_list([[T1,T2]|Rest], Acc, Unifier):-
     functor(T1, Functor, Arity),
     functor(T2, Functor, Arity),
     argument_pairs(T1, T2, Arity, Rest, Pairs),
     unify_list(Pairs, Acc, Unifier).

% Forming argument pairs componentwise

argument_pairs(_, _, 0, Acc, Acc).
argument_pairs(T1, T2, Argument_number, Acc, Pairs):-
    arg(Argument_number, T1, Argument1),
    arg(Argument_number, T2, Argument2),
    Argument_number1 is Argument_number-1,
    argument_pairs(T1, T2, Argument_number1, [[Argument1,Argument2]|Acc], Pairs).

% Occurrence check

occurs(X, X):-
    !.
occurs(X, Y):-
    compound(Y),
    Y=..[_|YL],
    occurs_list(X, YL).

occurs_list(X, [Y|_]):-
    occurs(X, Y),
    !.
occurs_list(X, [_|T]):-
    occurs_list(X, T).


% Variable test, Variable are identifiers that end with _.

variable(X):-
    atom(X),
    name(X, List),
    append(_, [95], List).


% Application of a substitution on a list of expressions.
% Expression is any Prolog structure.

apply_substitution([], _, []).

apply_substitution([Expr|Rest], [Var -> Term], [Expr_Instance|Rest_Instance]):-
     apply_on_expr(Expr, [Var -> Term], Expr_Instance),
     apply_substitution(Rest, [Var -> Term], Rest_Instance).


% Application of a substitution on an expression

apply_on_expr(Var, [Var -> Term], Term):-!.

apply_on_expr(Expr, Subst, Expr_Instance):-
     compound(Expr),
     !,
     Expr =..[Functor|Arguments],
     apply_substitution(Arguments, Subst, Argument_Instance),
     Expr_Instance=..[Functor|Argument_Instance].

apply_on_expr(Expr, _, Expr).




% Compose substitutions

compose_substitutions(Subst1, Subst2, Subst3):-
    apply_substitution(Subst1, Subst2, S),
    add_and_clean(S, Subst2, [], Subst3).

add_and_clean([],[V -> T], Acc, [V ->T |Acc]).
add_and_clean([V -> T|Rest], Subst, Acc, Answer):-
    remove_if_the_same_variable(Subst, V, NewSubst),
    add_if_not_identity([V -> T], Acc, NewAcc),
    add_and_clean(Rest, NewSubst, NewAcc, Answer).


remove_if_the_same_variable([V -> _], V, []):-
    !.
remove_if_the_same_variable([V -> T], _, [V -> T]).

add_if_not_identity([V->V], Answer, Answer):-
    !.
add_if_not_identity([V->T], Answer, [V->T|Answer]).