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