Algorithme d'unification

Pour des détails sur l'algorithme et afin de pouvoir suivre plus facilement, on se reportera aux source en annexe.
Pour l'unification, une procédure et une fonction particulières sont utilisées : Variable_Liee et Environnement_Empiler. La première prend en arguments une instance de variable (la variable et son niveau) ainsi qu'un environnement et retourne un lien (sous forme d'instance d'arbre). Elle recherche dans l'environnement si l'instance de variabe est liée et si oui, elle renvoie dans son paramètre de sortie vers le lien en question. Sinon, elle renvoie NULL. Il faut faire attention à cette fonction, car elle construit un nouvel environnement (donc elle alloue de la mémoire) pour le rajouter au sommet de la pile d'environnements courante. Il faudra donc penser à la désallocation plus tard (voir la section 2.3). La seconde prend deux instances d'arbre qui sont liées en argument ainsi qu'une pile d'environnements. Elle empile ces deux instances au sommet de la pile d'environnement et retourne la pile résultante. Afin d'éviter les boucles du genre *a1 pointe vers *a2 et *a2 pointe *a1, on convient de toujours faire pointer la variable de niveau supérieur vers la variable de niveau inférieur.
La procédure Unifier prend donc en arguments deux instances d'arbre à unifier instance1 et instance2, une pile d'environnements de départ depart contenant les contraintes initiales sur les variables. Elle a deux paramètres de sortie: un boléen match valant TRUE ou FALSE selon que les deux instances d'arbre étaient unifiables ou non, et l'environnement resultat résultant de l'éventuel unification. Si l'unification n'était pas possible, l'environnement resultat est le même que l'environnement depart.
Pour unifier deux foncteurs, il faut d'abord vérifier qu'ils aient même nom et même nombre d'arguments. En effet deux foncteurs peuvent avoir le même nom mais un nombre différent d'arguments : dans ce cas, ils sont bien sûr considérés comme étant différents et par conséquent non unifiables. Il faut ensuite chercher si leurs arguments sont deux à deux unifiables et en déduire les contraintes correspondantes. Pour cela, il suffit d'appeler récursivement la procédure Unifier sur les instances d'arbre correspondants aux arguments respectifs des deux foncteurs. Le seul problème est que les arguments des foncteurs sont connus sous leur forme d'arbre et non d'instance d'arbre. Il faut donc reconstruire une instance d'arbre à partir des deux arbres avec, comme niveau, le niveau de leur foncteur père respectif, à savoir instance1 et instance2. Si un seul de leurs arguments n'est pas unifiable, alors les deux foncteurs ne sont pas unifiables et il faut alors désallouer l'environnemet que l'on a commencé à construire.
L'unification d'une variable avec un foncteur est plus simple. On regarde si cette variable est liée dans la pile d'environnement de départ. Si c'est le cas, alors on essaye d'unifier le foncteur avec ce vers quoi pointe cette variable (appel récursif à Unifier). Sinon, alors on peut empiler une nouvelle contrainte sur la pile d'environnement grâce à la fonction Environnement_Empiler.
Pour unifier deux variables, on regarde d'abord si la première est liée. Si c'est le cas, alors il suffit de tenter d'unifier (récursivement) la deuxième variable avec ce vers quoi pointe la première. Sinon, on fait la même chose pour la deuxième variable (en inversant les rôles). Finalememt, si aucune des deux n'est liée, alors il faut empiler la nouvelle contrainte sur la pile d'environnement.