(* Source !\ahref{hindley2.ml}{hindley2.ml}! *) open S open Ast open T.Type (* Voir la documentation du module !\pcfmodule{Eq}!, qui définit les équations, les substitutions etc. *) exception Error of string (*******************************************************) (* Algorithme de synthèse de type simples (de hindley) *) (* avec résolution immédiate *) (*******************************************************) let rec typeof env t s = match t with | Num n -> Nat,s | Var x -> let ty = try List.assoc x env with Not_found -> raise (Error ("Unbound var: "^x)) in ty,s | Op (_op,t1,t2) -> let ty1,s = typeof env t1 s in let s = Eq.mgu_incr ty1 Nat s in let ty2,s = typeof env t2 s in let s = Eq.mgu_incr ty2 Nat s in Nat,s | Ifz (t1,t2,t3) -> let ty1,s = typeof env t1 s in let s = Eq.mgu_incr ty1 Nat s in let ty2,s = typeof env t2 s in let ty3,s = typeof env t3 s in let s = Eq.mgu_incr ty2 ty3 s in ty3,s | App (t1,t2) -> let ty1,s = typeof env t1 s in let ty2,s = typeof env t2 s in let n = Eq.fresh_var() in let s = Eq.mgu_incr ty1 (Arrow (ty2,Tvar n)) s in Tvar n,s | Fun (x,t) -> let n = Eq.fresh_var () in let ty,s = typeof ((x,Tvar n)::env) t s in Arrow (Tvar n, ty),s | Fix (x,t) -> let n = Eq.fresh_var () in let ty,s = typeof ((x,Tvar n)::env) t s in let s = Eq.mgu_incr (Tvar n) ty s in ty,s | Let (x,t1,t2) -> let ty1,s = typeof env t1 s in typeof ((x,ty1)::env) t2 s let infer env t = (* fabriquer les équations *) let ty,s = typeof env t Eq.id in (* Ne pas oublier d'appliquer le mgu *) Eq.subst_type s ty