exception Libre of var let tvar = let last = ref 0 in fun () -> incr last; Tvar !last;; let find_type_var x env = try List.assoc x env with Not_found -> raise (Libre x) let rec infer env a = match a with | Const n -> Tint, [ ] | Var x -> find_type_var x env, [ ] | App (a1, a2) -> let t1, s1 = infer env a1 in let t2, s2 = infer (subst_tenv s1 env) a2 in let t3 = tvar() in let s3 = unify (subst_texp s2 t1) (Tarrow (t2, t3)) in subst_texp s3 t3, compose s3 (compose s2 s1) | Fonction (x, a) -> let t0 = tvar() in let t1, s1 = infer ((x, t0)::env) a in Tarrow (subst_texp s1 t0, t1), s1 | Liaison (x, a1, a2) -> let t1, s1 = infer env a1 in let t2, s2 = infer ((x, t1):: subst_tenv s1 env) a2 in t2, compose s2 s1 | Prim (f, al) -> let tf : texp = find_type_var f.name env in let t0 = tvar() in let rec targs = function [] -> t0, [ ] | a:: rest -> let tr, sr = targs rest in let tl, sl = infer (subst_tenv sr env) a in Tarrow (tl, tr), compose sl sr in let t, s = targs al in let s1 = unify (subst_texp s tf) t in let s2 = compose s1 s in subst_texp s2 t0, s2 ;;