Salut Vincent,

Pour l'unification, il faudrait donc implémenter une fonction dont la signature devrait ressembler à qqch comme:

unify: lexp -> lexp -> subst -> ((subst * constraints) option)

où `constraints` serait qqch du genre:

type contraints = (lexp * lexp) list

et représente une lite de contraintes d'égalités qu'on a pas su résoudre, c'est à dire pour lesquelles on ne peut pas dire que l'égalité est nécessairement fausse, mais on ne sait pas non plus quelle substitution pourrait la résoudre.

Pour `subst` c'est simplement une table qui associe une lexp à certaines méta-variables, donc du genre:

module VMap = Map.Make (struct type t = int let compare = compare end) type subst = lexp VMap.t

si les méta-variables sont représentée par des entiers rajoutés dans le type `lexp` avec un contructeur:

| Metavar of int (* string * location)

Tu peux t'inspirer de la fonction conv_p dans typecheck.ml.

Stefan