type texp = node ref and node = Desc of desc | Link of texp and desc = Tvar of int (* l'argument est utilisé seulement pour la mise au point *) | Tint | Tarrow of texp * texp ;; let count = ref 0;; let tvar() = incr count; ref (Desc (Tvar !count));; let tint = ref (Desc Tint);; let tarrow t1 t2 = ref (Desc (Tarrow (t1, t2)));; let rec repr t = match !t with Link u -> let v = repr u in t := Link v; v | Desc _ -> t ;; let desc t = match !(repr t) with Link u -> assert false | Desc d -> d ;; let rec libre x t = let x = repr x and t = repr t in if x == t then true else match desc t with Tint -> false | Tvar _ -> false | Tarrow (t1, t2) -> libre x t1 || libre x t2;; let subst t1 t2 = (repr t1) := Link t2;; exception Unify of texp * texp;; let rec unify t1 t2 = let t1 = repr t1 and t2 = repr t2 in if t1 == t2 then () else match desc t1, desc t2 with | Tvar _, Tvar _ -> () | Tvar _, _ -> if libre t1 t2 then raise (Unify (t1, t2)) else subst t1 t2 | _, Tvar _ -> if libre t2 t1 then raise (Unify (t1, t2)) else subst t2 t1 | Tint, Tint -> () | Tarrow (t11, t12), Tarrow (t21, t22) -> unify t11 t21; unify t12 t22 | _, _ -> raise (Unify (t1,t2)) ;;