(* Source !\ahref{poly.ml}{poly.ml}! *) open S.Ast (* Termes non-typés *) open T.Type (* Types *) (* Documentation du module !\pcfmodule{Eq}! *) (* Petite abréviation *) module V = Eq.Vars (* Documentation du module !\pcfmodule{Eq.Vars}! *) (***************************************) (* Divers calculs des variables libres *) (***************************************) (* Dans un type *) let rec free t = match t with | Tvar n -> V.singleton n | Nat -> V.empty | Arrow (t1,t2) -> V.union (free t1) (free t2) (* Dans un schéma de type *) let free_scheme (xs,t) = V.diff (free t) (V.of_list xs) (* Dans un environnement de typage *) let free_env env = List.fold_right (fun (_,sc) r -> V.union (free_scheme sc) r) env V.empty (*****************************************) (* Diverses applications de substitution *) (*****************************************) (* À un schéma de type: on suppose que le support de s et vs sont disjoints *) let subst_scheme s (xs,t) = assert (V.disjoint (Eq.dom s) (V.of_list xs)) ; (* Ce qui simplifie beaucoup... *) xs,Eq.subst_type s t (* Application d'une substitution à un environnement *) let subst_env s env = List.map (fun (x,sc) -> x,subst_scheme s sc) env (****************************************) (* !\aname{freshen}{Instance}! fraîche d'un schéma de type *) (****************************************) (* Fabriquer une substitution qui associe des variables fraîches aux variables de la liste xs *) let subst_fresh xs = List.fold_right (fun x r -> Eq.comp (Eq.delta x (Tvar (Eq.fresh_var ()))) r) xs Eq.id let freshen (xs,t) = Eq.subst_type (subst_fresh xs) t (************************************************) (* !\aname{generalize}{Généralisation}! d'un type en un schéma de type *) (************************************************) (* Assez sportif (pas de renommage), mais ils semble que cela fonctionne. 1. La prise d'instance n'est en rien influencée le nom exact des xs (freshen ci-dessus) 2. La substitution dans un schéma (subst_scheme) semble également correcte, car les variables quantifiée sont justement absentes de l'environnement *) let generalize env t = let xs = V.elements (V.diff (free t) (free_env env)) in xs,t (***************************) (* Inféreur proprement dit *) (***************************) exception Error of string let rec typeof s env t = match t with (* Plus que facile *) | Num _ -> Nat,s (* Pour l'application voir !\ahrefloc{apply}{ci-après}! *) | App (t1,t2) -> typeof_app (typeof s env t1) env t2 (* Les deux cas suivants sont des cas particuliers d'application *) | Op (_,t1,t2) -> let t_op = Arrow (Nat, Arrow (Nat,Nat)) in let r = typeof_app (t_op,s) env t1 in typeof_app r env t2 | Ifz (t1,t2,t3) -> let t_if = (* Type d'une occurrence d'une hypothétique fonction ifz : \forall A [Nat -> A -> A] *) let tv = Tvar (Eq.fresh_var ()) in Arrow (Nat,Arrow (tv,Arrow (tv,tv))) in let r = typeof_app (t_if,s) env t1 in let r = typeof_app r env t2 in typeof_app r env t3 (* Pas grand chose à remarquer si ce n'est que env est étendu *) | Fun (x,t1) -> let tyx = Tvar (Eq.fresh_var ()) in let ty1,s = typeof s ((x,([],tyx))::env) t1 in Arrow (tyx,ty1),s (* Par l'opérateur de pt fixe Y: \forall A [(A -> A) -> A] *) | Fix (x,t) -> let t_fix = let tv = Eq.fresh_var () in Arrow (Arrow (Tvar tv,Tvar tv), Tvar tv) in typeof_app (t_fix,s) env (Fun (x,t)) (* Tout le polymorphisme est là, voir aussi !\ahrefloc{freshen}{freshen}! et !\ahrefloc{generalize}{generalize}! *) | Let (x,t1,t2) -> let ty1,s = typeof s env t1 in let sc1 = generalize (subst_env s env) (Eq.subst_type s ty1) in typeof s ((x,sc1)::env) t2 | Var x -> let sc = try List.assoc x env with Not_found -> raise (Error ("Unbound var: "^x)) in freshen sc,s (* !\aname{apply}{Traitement}! de l'application, seul cas de résolution. *) and typeof_app (ty_fun,s) env t = (* t_fun,s est le type de la fonction *) let ty_arg,s = typeof s env t in (* typer l'argument *) let ty_res = Tvar (Eq.fresh_var ()) in let s = (* ajouter l'équation ty_fun = ty_arg -> ty_res *) Eq.mgu_incr ty_fun (Arrow (ty_arg,ty_res)) s in ty_res, s (***********************) (* Fonctions exportées *) (***********************) (* Typer dans un environnement vide *) let infer t = let ty,s = typeof Eq.id [] t in Eq.subst_type s ty let verbose = List.mem "-v" (Array.to_list Sys.argv) (* Pour la boucle interactive *) let infer_scheme env t = let ty,s = typeof Eq.id env t in let ty = Eq.subst_type s ty in (* Généralisaton de toutes les variables de t, correct si env ne contient aucune variable libre, ce qui est le cas si les schema de types de env sont ainsi genéralisés. *) let xs = free ty in assert (V.disjoint (free_env env) xs) ; V.elements xs,ty (* Tests... # Élémentaire Let x = 1;; Let y = 1+3;; Let z = x+y;; ;; # fonctions Let id = Fun x -> x;; Let k1 = Fun x -> Fun y -> y;; Let k2 = Fun x -> Fun y -> x;; Let plus = Fun x -> Fun y -> x+y;; # if + fonctions Let if1 = Fun x -> Fun y -> Ifz x Then y Else x;; Let if2 = Fun x -> Fun y -> Ifz x Then x Else y;; Let if3 = Fun x -> Fun y -> Fun z -> Ifz x Then y Else z;; Let f1 = Fun x -> Fun y -> x+0 In Let f2 = Fun x -> Fun y -> y+0 In Fun z -> Ifz z Then f1 Else f2 ;; # fonctions plus méchant Let t = Fun t -> Fun f -> t;; Let f = Fun t -> Fun f -> f;; Let not = Fun b -> Fun kt -> Fun kf -> b kf kt;; Let and = Fun b1 -> Fun b2 -> Fun kt -> Fun kf -> b1 (b2 kt kf) kf;; let or = Fun b1 -> Fun b2 -> not (and (not b1) (not b2)) ;; # Doit avoir le type de f Let b = and f (or t (or f f));; # Généralisation Let test_gen1 = Fun x -> Let y = x in y;; Let test_gen2 = Let id = Fun x -> x In id id id id id # Et encore Let app = Fun f -> Fun x -> f x;; let app1 = fun x -> let g = fun y -> x y in g;; Let app2 = Fun f -> Let g = Fun x -> f x In Let h = Fun x -> g x In h;; Let x = 1 In Fun f -> Fun z -> f x z;; # Quelques pt. fixes Let Rec pow = Fun n -> Ifz n Then 1 Else 2 * pow (n-1);; Let Rec loop = loop;; Let Rec loop2 = Fun x -> loop2 x;; Let Rec loop3 = Fun x -> loop3 (x+x);; Let Rec loop4 = Fun x -> loop4 (loop4 (x+x));; # Ne doit pas typer Let Rec f = Fun x -> Ifz x Then 0 Else f+1;; # Casse tout Let pair = Fun x -> Fun y -> Fun p -> p x y In Let x0 = Fix x -> x In Let x1 = pair x0 x0 In Let x2 = pair x1 x1 In Let x3 = pair x2 x2 In Let x4 = pair x3 x3 In Let x5 = pair x4 x4 In Let x6 = pair x5 x5 In Let x7 = pair x6 x6 In Let x8 = pair x7 x7 In Let x9 = pair x8 x8 In x9 ;; *)