/****************************************************************************/
/* Modules                                                                  */
/****************************************************************************/

% Pour maplist().
:- use_module(library(apply)).

/****************************************************************************/
/* Petits utilitaires.                                                      */
/****************************************************************************/

% Opérateur ?=.
:- op(20, xfy, ?=).

% Crée une liste à partir d'un élément.
repeter(X, N, [X|Reste]) :- N > 0, I is N - 1, repeter(X, I, Reste), !.
repeter(_, 0, []).

% Prend deux termes et les met en opérande de ?=.
appairer(T1, T2, R) :- R = T1 ?= T2.

% Ecriture conditionnelle.
ecrire(X) :- write(X).

/****************************************************************************/
/* Remplacement d'une variable par un terme.                                */
/****************************************************************************/

% Remplacement de variable dans un terme.
remplace_variable(Terme, Variable, Entree, Sortie) :-
    Variable == Entree,
    Sortie = Terme,
    !
    .

% Remplacement de variable dans un terme.
remplace_variable(Terme, Variable, Entree, Sortie) :-
    compound(Entree),
    Entree =.. [Foncteur|Args],
    length(Args, Longueur),
    repeter(Terme, Longueur, ListeT),
    repeter(Variable, Longueur, ListeV),
    maplist(remplace_variable, ListeT, ListeV, Args, Resultat),
    append([Foncteur], Resultat, ListeSortie),
    Sortie =.. ListeSortie,
    !
    .

% Dans les autres cas de remplacement, aucune modification.
remplace_variable(_, _, Entree, Sortie) :- Sortie = Entree.

/****************************************************************************/
/* Test d'occurrence.                                                       */
/****************************************************************************/

% Test d'occurrence quand le terme est une variable.
occur_check(V, T) :- var(V), V == T, !.

% Test d'occurrence quand le terme est un prédicat.
occur_check(V, T) :-
    compound(T),
    T =.. [_|Args],
    occur_check_liste(V, Args),
    !
    .

% Test d'occurrence dans une liste de termes.
occur_check_liste(V, [Tete|Reste]) :- occur_check(V, Tete) ; occur_check_liste(V, Reste).
occur_check_liste(_, []) :- fail.

/****************************************************************************/
/* Détermination de la règle de calcul applicable.                          */
/****************************************************************************/

% Test d'application de la règle Rename.
regle(X ?= T, rename) :- var(X), var(T), !.

% Test d'application de la règle Simplify.
regle(X ?= T, simplify) :- var(X), atom(T), !.

% Test d'application de la règle Expand.
regle(X ?= T, expand) :- var(X), compound(T), \+ occur_check(X, T), !.

% Test d'application de la règle Check.
regle(X ?= T, check) :- var(X), X \== T, occur_check(X, T), !.

% Test d'application de la règle Orient.
regle(T ?= X, orient) :- var(X), compound(T), !.

% Test d'application de la règle Decompose.
regle(A ?= B, decompose) :-
    compound(A), compound(B),
    A =.. [F1|Args1],
    B =.. [F1|Args2],
    same_length(Args1, Args2),
    !
    .

% Test d'application de la règle Clash.
regle(A ?= B, clash) :-
    compound(A), compound(B),
    A =.. [F1|Args1],
    B =.. [F2|Args2],
    (
        F1 \== F2 ;
        \+ same_length(Args1, Args2)
    ),
    !
    .

/****************************************************************************/
/* Unification des termes en utilisant les règles de calcul de l'algo.      */
/****************************************************************************/

% Application de la règle Rename.
reduit(rename, X ?= T, P, Q) :- remplace_variable(T, X, P, Q), !.

% Application de la règle Simplify.
reduit(simplify, X ?= T, P, Q) :- remplace_variable(T, X, P, Q), !.

% Application de la règle Expand.
reduit(expand, X ?= T, P, Q) :- remplace_variable(T, X, P, Q), !.

% Application de la règle Check.
reduit(check, _, _, Q) :- Q = echec.

% Application de la règle Orient.
reduit(orient, T ?= X, P, Q) :- append([X ?= T], P, Q), !.

% Application de la règle Decompose.
reduit(decompose, A ?= B, P, Q) :-
    A =.. [_|Args1],
    B =.. [_|Args2],
    maplist(appairer, Args1, Args2, Paires),
    append(Paires, P, Q),
    !
    .

% Application de la règle Clash.
reduit(clash, _, _, Q) :- Q = echec.

/****************************************************************************/
/* Différentes stratégies d'unification.                                    */
/****************************************************************************/

% Stratégie dépendant de l'implémentation de Prolog.
choix_premier([Tete|Reste], Resultat, Equation, Regle) :-
    regle(Tete, Regle),
    Equation = Tete,
    reduit(Regle, Tete, Reste, Resultat),
    !
    .

% Choix avec la pondération des règles optimale.
choix_pondere_optimal(Termes, Resultat, Equation, Regle) :-
    choix_pondere(
        Termes, Resultat, Equation, Regle,
        [clash, check, rename, simplify, orient, decompose, expand]
    ).

% Choix avec pondération des règles. Il y a toujours forcément une règle qui s'applique.
choix_pondere(_, _, _, _, []) :- fail.
choix_pondere(Termes, Resultat, Equation, RegleChoisie, [Regle|Regles]) :-
    (
        choix_premier(Termes, Resultat, Equation, Regle),
        RegleChoisie = Regle
    );
    choix_pondere(Termes, Resultat, Equation, RegleChoisie, Regles)
    .

/****************************************************************************/
/* Prédicat exécutant l'algorithme de Martelli-Montanari.                   */
/****************************************************************************/

% Stratégie par défaut.
unifie(Termes) :- unifie(Termes, choix_premier).

% Une liste vide est unifiée.
unifie([], _) :- nl.

% Unification d'un terme.
unifie(Termes, Strategie) :-
    ecrire('system : '), ecrire(Termes), nl,
    call(Strategie, Termes, Resultat, Equation, Regle),
    ecrire(Regle), ecrire(' : '), ecrire(Equation), nl,
    Resultat \== echec,
    unifie(Resultat, Strategie),
    !
    .

/****************************************************************************/
/* Tests                                                                    */
/****************************************************************************/

% unifie([Z ?= f(X), f(X,Y) ?= f(g(Z),h(a))], choix_pondere_optimal).

/****************************************************************************/
/* Menu principal.                                                          */
/****************************************************************************/

unification :-
    write('Entrez une liste de termes a unifier : '),
    read_term(A, [variable_names(L)]), !,
    writeln(L),
    write('Choisissez une strategie : '),
    read_term(B, []), !,
    unifie(A, B)
    .