(***********************************************************************) (* *) (* Objective Caml *) (* *) (* Xavier Leroy and Jerome Vouillon, projet Cristal, INRIA Rocquencourt*) (* *) (* Copyright 1996 Institut National de Recherche en Informatique et *) (* en Automatique. All rights reserved. This file is distributed *) (* under the terms of the Q Public License version 1.0. *) (* *) (***********************************************************************) (* $Id: ctype.ml 9453 2009-12-07 13:04:54Z garrigue $ *) (* Operations on core types *) open Misc open Asttypes open Types open Btype (* Type manipulation after type inference ====================================== If one wants to manipulate a type after type inference (for instance, during code generation or in the debugger), one must first make sure that the type levels are correct, using the function [correct_levels]. Then, this type can be correctely manipulated by [apply], [expand_head] and [moregeneral]. *) (* General notes ============= - As much sharing as possible should be kept : it makes types smaller and better abbreviated. When necessary, some sharing can be lost. Types will still be printed correctly (+++ TO DO...), and abbreviations defined by a class do not depend on sharing thanks to constrained abbreviations. (Of course, even if some sharing is lost, typing will still be correct.) - All nodes of a type have a level : that way, one know whether a node need to be duplicated or not when instantiating a type. - Levels of a type are decreasing (generic level being considered as greatest). - The level of a type constructor is superior to the binding time of its path. - Recursive types without limitation should be handled (even if there is still an occur check). This avoid treating specially the case for objects, for instance. Furthermore, the occur check policy can then be easily changed. *) (* A faire ======= - Revoir affichage des types. - Etendre la portee d'un alias [... as 'a] a tout le type englobant. - #-type implementes comme de vraies abreviations. - Niveaux plus fins pour les identificateurs : Champ [global] renomme en [level]; Niveau -1 : global 0 : module toplevel 1 : module contenu dans module toplevel ... En fait, incrementer le niveau a chaque fois que l'on rentre dans un module. 3 4 6 \ / / 1 2 5 \|/ 0 [Subst] doit ecreter les niveaux (pour qu'un variable non generalisable dans un module de niveau 2 ne se retrouve pas generalisable lorsque l'on l'utilise au niveau 0). - Traitement de la trace de l'unification separe de la fonction [unify]. *) (**** Errors ****) exception Unify of (type_expr * type_expr) list exception Tags of label * label exception Subtype of (type_expr * type_expr) list * (type_expr * type_expr) list exception Cannot_expand exception Cannot_apply exception Recursive_abbrev (**** Type level management ****) let current_level = ref 0 let nongen_level = ref 0 let global_level = ref 1 let saved_level = ref [] let init_def level = current_level := level; nongen_level := level let begin_def () = saved_level := (!current_level, !nongen_level) :: !saved_level; incr current_level; nongen_level := !current_level let begin_class_def () = saved_level := (!current_level, !nongen_level) :: !saved_level; incr current_level let raise_nongen_level () = saved_level := (!current_level, !nongen_level) :: !saved_level; nongen_level := !current_level let end_def () = let (cl, nl) = List.hd !saved_level in saved_level := List.tl !saved_level; current_level := cl; nongen_level := nl let reset_global_level () = global_level := !current_level + 1 let increase_global_level () = let gl = !global_level in global_level := !current_level; gl let restore_global_level gl = global_level := gl (* Abbreviations without parameters *) (* Shall reset after generalizing *) let simple_abbrevs = ref Mnil let proper_abbrevs path tl abbrev = if !Clflags.principal || tl <> [] then abbrev else let name = match path with Path.Pident id -> Ident.name id | Path.Pdot(_, s,_) -> s | Path.Papply _ -> assert false in if name.[0] <> '#' then simple_abbrevs else abbrev (**** Some type creators ****) (* Re-export generic type creators *) let newty2 = Btype.newty2 let newty desc = newty2 !current_level desc let new_global_ty desc = newty2 !global_level desc let newvar () = newty2 !current_level Tvar let newvar2 level = newty2 level Tvar let new_global_var () = newty2 !global_level Tvar let newobj fields = newty (Tobject (fields, ref None)) let newconstr path tyl = newty (Tconstr (path, tyl, ref Mnil)) let none = newty (Ttuple []) (* Clearly ill-formed type *) (**** Representative of a type ****) (* Re-export repr *) let repr = repr (**** Type maps ****) module TypePairs = Hashtbl.Make (struct type t = type_expr * type_expr let equal (t1, t1') (t2, t2') = (t1 == t2) && (t1' == t2') let hash (t, t') = t.id + 93 * t'.id end) (**********************************************) (* Miscellaneous operations on object types *) (**********************************************) (**** Object field manipulation. ****) let dummy_method = "*dummy method*" let object_fields ty = match (repr ty).desc with Tobject (fields, _) -> fields | _ -> assert false let flatten_fields ty = let rec flatten l ty = let ty = repr ty in match ty.desc with Tfield(s, k, ty1, ty2) -> flatten ((s, k, ty1)::l) ty2 | _ -> (l, ty) in let (l, r) = flatten [] ty in (Sort.list (fun (n, _, _) (n', _, _) -> n < n') l, r) let build_fields level = List.fold_right (fun (s, k, ty1) ty2 -> newty2 level (Tfield(s, k, ty1, ty2))) let associate_fields fields1 fields2 = let rec associate p s s' = function (l, []) -> (List.rev p, (List.rev s) @ l, List.rev s') | ([], l') -> (List.rev p, List.rev s, (List.rev s') @ l') | ((n, k, t)::r, (n', k', t')::r') when n = n' -> associate ((n, k, t, k', t')::p) s s' (r, r') | ((n, k, t)::r, ((n', k', t')::_ as l')) when n < n' -> associate p ((n, k, t)::s) s' (r, l') | (((n, k, t)::r as l), (n', k', t')::r') (* when n > n' *) -> associate p s ((n', k', t')::s') (l, r') in associate [] [] [] (fields1, fields2) (**** Check whether an object is open ****) (* +++ Il faudra penser a eventuellement expanser l'abreviation *) let rec object_row ty = let ty = repr ty in match ty.desc with Tobject (t, _) -> object_row t | Tfield(_, _, _, t) -> object_row t | _ -> ty let opened_object ty = match (object_row ty).desc with | Tvar -> true | Tunivar -> true | Tconstr _ -> true | _ -> false (**** Close an object ****) let close_object ty = let rec close ty = let ty = repr ty in match ty.desc with Tvar -> link_type ty (newty2 ty.level Tnil) | Tfield(_, _, _, ty') -> close ty' | _ -> assert false in match (repr ty).desc with Tobject (ty, _) -> close ty | _ -> assert false (**** Row variable of an object type ****) let row_variable ty = let rec find ty = let ty = repr ty in match ty.desc with Tfield (_, _, _, ty) -> find ty | Tvar -> ty | _ -> assert false in match (repr ty).desc with Tobject (fi, _) -> find fi | _ -> assert false (**** Object name manipulation ****) (* +++ Bientot obsolete *) let set_object_name id rv params ty = match (repr ty).desc with Tobject (fi, nm) -> set_name nm (Some (Path.Pident id, rv::params)) | _ -> assert false let remove_object_name ty = match (repr ty).desc with Tobject (_, nm) -> set_name nm None | Tconstr (_, _, _) -> () | _ -> fatal_error "Ctype.remove_object_name" (**** Hiding of private methods ****) let hide_private_methods ty = match (repr ty).desc with Tobject (fi, nm) -> nm := None; let (fl, _) = flatten_fields fi in List.iter (function (_, k, _) -> match field_kind_repr k with Fvar r -> set_kind r Fabsent | _ -> ()) fl | _ -> assert false (*******************************) (* Operations on class types *) (*******************************) let rec signature_of_class_type = function Tcty_constr (_, _, cty) -> signature_of_class_type cty | Tcty_signature sign -> sign | Tcty_fun (_, ty, cty) -> signature_of_class_type cty let self_type cty = repr (signature_of_class_type cty).cty_self let rec class_type_arity = function Tcty_constr (_, _, cty) -> class_type_arity cty | Tcty_signature _ -> 0 | Tcty_fun (_, _, cty) -> 1 + class_type_arity cty (*******************************************) (* Miscellaneous operations on row types *) (*******************************************) let sort_row_fields = Sort.list (fun (p,_) (q,_) -> p < q) let rec merge_rf r1 r2 pairs fi1 fi2 = match fi1, fi2 with (l1,f1 as p1)::fi1', (l2,f2 as p2)::fi2' -> if l1 = l2 then merge_rf r1 r2 ((l1,f1,f2)::pairs) fi1' fi2' else if l1 < l2 then merge_rf (p1::r1) r2 pairs fi1' fi2 else merge_rf r1 (p2::r2) pairs fi1 fi2' | [], _ -> (List.rev r1, List.rev_append r2 fi2, pairs) | _, [] -> (List.rev_append r1 fi1, List.rev r2, pairs) let merge_row_fields fi1 fi2 = match fi1, fi2 with [], _ | _, [] -> (fi1, fi2, []) | [p1], _ when not (List.mem_assoc (fst p1) fi2) -> (fi1, fi2, []) | _, [p2] when not (List.mem_assoc (fst p2) fi1) -> (fi1, fi2, []) | _ -> merge_rf [] [] [] (sort_row_fields fi1) (sort_row_fields fi2) let rec filter_row_fields erase = function [] -> [] | (l,f as p)::fi -> let fi = filter_row_fields erase fi in match row_field_repr f with Rabsent -> fi | Reither(_,_,false,e) when erase -> set_row_field e Rabsent; fi | _ -> p :: fi (**************************************) (* Check genericity of type schemes *) (**************************************) exception Non_closed let rec closed_schema_rec ty = let ty = repr ty in if ty.level >= lowest_level then begin let level = ty.level in ty.level <- pivot_level - level; match ty.desc with Tvar when level <> generic_level -> raise Non_closed | Tfield(_, kind, t1, t2) -> if field_kind_repr kind = Fpresent then closed_schema_rec t1; closed_schema_rec t2 | Tvariant row -> let row = row_repr row in iter_row closed_schema_rec row; if not (static_row row) then closed_schema_rec row.row_more | _ -> iter_type_expr closed_schema_rec ty end (* Return whether all variables of type [ty] are generic. *) let closed_schema ty = try closed_schema_rec ty; unmark_type ty; true with Non_closed -> unmark_type ty; false exception Non_closed of type_expr * bool let free_variables = ref [] let really_closed = ref None let rec free_vars_rec real ty = let ty = repr ty in if ty.level >= lowest_level then begin ty.level <- pivot_level - ty.level; begin match ty.desc, !really_closed with Tvar, _ -> free_variables := (ty, real) :: !free_variables | Tconstr (path, tl, _), Some env -> begin try let (_, body) = Env.find_type_expansion path env in if (repr body).level <> generic_level then free_variables := (ty, real) :: !free_variables with Not_found -> () end; List.iter (free_vars_rec true) tl (* Do not count "virtual" free variables | Tobject(ty, {contents = Some (_, p)}) -> free_vars_rec false ty; List.iter (free_vars_rec true) p *) | Tobject (ty, _), _ -> free_vars_rec false ty | Tfield (_, _, ty1, ty2), _ -> free_vars_rec true ty1; free_vars_rec false ty2 | Tvariant row, _ -> let row = row_repr row in iter_row (free_vars_rec true) row; if not (static_row row) then free_vars_rec false row.row_more | _ -> iter_type_expr (free_vars_rec true) ty end; end let free_vars ?env ty = free_variables := []; really_closed := env; free_vars_rec true ty; let res = !free_variables in free_variables := []; really_closed := None; res let free_variables ?env ty = let tl = List.map fst (free_vars ?env ty) in unmark_type ty; tl let rec closed_type ty = match free_vars ty with [] -> () | (v, real) :: _ -> raise (Non_closed (v, real)) let closed_parameterized_type params ty = List.iter mark_type params; let ok = try closed_type ty; true with Non_closed _ -> false in List.iter unmark_type params; unmark_type ty; ok let closed_type_decl decl = try List.iter mark_type decl.type_params; begin match decl.type_kind with Type_abstract -> () | Type_variant v -> List.iter (fun (_, tyl) -> List.iter closed_type tyl) v | Type_record(r, rep) -> List.iter (fun (_, _, ty) -> closed_type ty) r end; begin match decl.type_manifest with None -> () | Some ty -> closed_type ty end; unmark_type_decl decl; None with Non_closed (ty, _) -> unmark_type_decl decl; Some ty type closed_class_failure = CC_Method of type_expr * bool * string * type_expr | CC_Value of type_expr * bool * string * type_expr exception Failure of closed_class_failure let closed_class params sign = let ty = object_fields (repr sign.cty_self) in let (fields, rest) = flatten_fields ty in List.iter mark_type params; mark_type rest; List.iter (fun (lab, _, ty) -> if lab = dummy_method then mark_type ty) fields; try mark_type_node (repr sign.cty_self); List.iter (fun (lab, kind, ty) -> if field_kind_repr kind = Fpresent then try closed_type ty with Non_closed (ty0, real) -> raise (Failure (CC_Method (ty0, real, lab, ty)))) fields; mark_type_params (repr sign.cty_self); List.iter unmark_type params; unmark_class_signature sign; None with Failure reason -> mark_type_params (repr sign.cty_self); List.iter unmark_type params; unmark_class_signature sign; Some reason (**********************) (* Type duplication *) (**********************) (* Duplicate a type, preserving only type variables *) let duplicate_type ty = Subst.type_expr Subst.identity ty (* Same, for class types *) let duplicate_class_type ty = Subst.class_type Subst.identity ty (*****************************) (* Type level manipulation *) (*****************************) (* It would be a bit more efficient to remove abbreviation expansions rather than generalizing them: these expansions will usually not be used anymore. However, this is not possible in the general case, as [expand_abbrev] (via [subst]) requires these expansions to be preserved. Does it worth duplicating this code ? *) let rec iter_generalize tyl ty = let ty = repr ty in if (ty.level > !current_level) && (ty.level <> generic_level) then begin set_level ty generic_level; begin match ty.desc with Tconstr (_, _, abbrev) -> iter_abbrev (iter_generalize tyl) !abbrev | _ -> () end; iter_type_expr (iter_generalize tyl) ty end else tyl := ty :: !tyl let iter_generalize tyl ty = simple_abbrevs := Mnil; iter_generalize tyl ty let generalize ty = iter_generalize (ref []) ty (* Efficient repeated generalisation of the same type *) let iterative_generalization min_level tyl = let tyl' = ref [] in List.iter (iter_generalize tyl') tyl; List.fold_right (fun ty l -> if ty.level <= min_level then l else ty::l) !tyl' [] (* Generalize the structure and lower the variables *) let rec generalize_structure var_level ty = let ty = repr ty in if ty.level <> generic_level then begin if ty.desc = Tvar && ty.level > var_level then set_level ty var_level else if ty.level > !current_level then begin set_level ty generic_level; begin match ty.desc with Tconstr (_, _, abbrev) -> abbrev := Mnil | _ -> () end; iter_type_expr (generalize_structure var_level) ty end end let generalize_structure var_level ty = simple_abbrevs := Mnil; generalize_structure var_level ty (* let generalize_expansive ty = generalize_structure !nongen_level ty *) let generalize_global ty = generalize_structure !global_level ty let generalize_structure ty = generalize_structure !current_level ty (* Generalize the spine of a function, if the level >= !current_level *) let rec generalize_spine ty = let ty = repr ty in if ty.level < !current_level || ty.level = generic_level then () else match ty.desc with Tarrow (_, _, ty', _) | Tpoly (ty', _) -> set_level ty generic_level; generalize_spine ty' | _ -> () let forward_try_expand_once = (* Forward declaration *) ref (fun env ty -> raise Cannot_expand) (* Lower the levels of a type (assume [level] is not [generic_level]). *) (* The level of a type constructor must be greater than its binding time. That way, a type constructor cannot escape the scope of its definition, as would be the case in let x = ref [] module M = struct type t let _ = (x : t list ref) end (without this constraint, the type system would actually be unsound.) *) let rec update_level env level ty = let ty = repr ty in if ty.level > level then begin begin match ty.desc with Tconstr(p, tl, abbrev) when level < Path.binding_time p -> (* Try first to replace an abbreviation by its expansion. *) begin try link_type ty (!forward_try_expand_once env ty); update_level env level ty with Cannot_expand -> (* +++ Levels should be restored... *) raise (Unify [(ty, newvar2 level)]) end | Tobject(_, ({contents=Some(p, tl)} as nm)) when level < Path.binding_time p -> set_name nm None; update_level env level ty | Tvariant row -> let row = row_repr row in begin match row.row_name with | Some (p, tl) when level < Path.binding_time p -> log_type ty; ty.desc <- Tvariant {row with row_name = None} | _ -> () end; set_level ty level; iter_type_expr (update_level env level) ty | Tfield(lab, _, _, _) when lab = dummy_method -> raise (Unify [(ty, newvar2 level)]) | _ -> set_level ty level; (* XXX what about abbreviations in Tconstr ? *) iter_type_expr (update_level env level) ty end end (* Generalize and lower levels of contravariant branches simultaneously *) let rec generalize_expansive env var_level ty = let ty = repr ty in if ty.level <> generic_level then begin if ty.level > var_level then begin set_level ty generic_level; match ty.desc with Tconstr (path, tyl, abbrev) -> let variance = try (Env.find_type path env).type_variance with Not_found -> List.map (fun _ -> (true,true,true)) tyl in abbrev := Mnil; List.iter2 (fun (co,cn,ct) t -> if ct then update_level env var_level t else generalize_expansive env var_level t) variance tyl | Tarrow (_, t1, t2, _) -> update_level env var_level t1; generalize_expansive env var_level t2 | _ -> iter_type_expr (generalize_expansive env var_level) ty end end let generalize_expansive env ty = simple_abbrevs := Mnil; try generalize_expansive env !nongen_level ty with Unify [_, ty'] -> raise (Unify [ty, ty']) (* Correct the levels of type [ty]. *) let correct_levels ty = duplicate_type ty (* Only generalize the type ty0 in ty *) let limited_generalize ty0 ty = let ty0 = repr ty0 in let graph = Hashtbl.create 17 in let idx = ref lowest_level in let roots = ref [] in let rec inverse pty ty = let ty = repr ty in if (ty.level > !current_level) || (ty.level = generic_level) then begin decr idx; Hashtbl.add graph !idx (ty, ref pty); if (ty.level = generic_level) || (ty == ty0) then roots := ty :: !roots; set_level ty !idx; iter_type_expr (inverse [ty]) ty end else if ty.level < lowest_level then begin let (_, parents) = Hashtbl.find graph ty.level in parents := pty @ !parents end and generalize_parents ty = let idx = ty.level in if idx <> generic_level then begin set_level ty generic_level; List.iter generalize_parents !(snd (Hashtbl.find graph idx)); (* Special case for rows: must generalize the row variable *) match ty.desc with Tvariant row -> let more = row_more row in let lv = more.level in if (lv < lowest_level || lv > !current_level) && lv <> generic_level then set_level more generic_level | _ -> () end in inverse [] ty; if ty0.level < lowest_level then iter_type_expr (inverse []) ty0; List.iter generalize_parents !roots; Hashtbl.iter (fun _ (ty, _) -> if ty.level <> generic_level then set_level ty !current_level) graph (*******************) (* Instantiation *) (*******************) let rec find_repr p1 = function Mnil -> None | Mcons (Public, p2, ty, _, _) when Path.same p1 p2 -> Some ty | Mcons (_, _, _, _, rem) -> find_repr p1 rem | Mlink {contents = rem} -> find_repr p1 rem (* Generic nodes are duplicated, while non-generic nodes are left as-is. During instantiation, the description of a generic node is first replaced by a link to a stub ([Tsubst (newvar ())]). Once the copy is made, it replaces the stub. After instantiation, the description of generic node, which was stored by [save_desc], must be put back, using [cleanup_types]. *) let abbreviations = ref (ref Mnil) (* Abbreviation memorized. *) let rec copy ty = let ty = repr ty in match ty.desc with Tsubst ty -> ty | _ -> if ty.level <> generic_level then ty else let desc = ty.desc in save_desc ty desc; let t = newvar() in (* Stub *) ty.desc <- Tsubst t; t.desc <- begin match desc with | Tconstr (p, tl, _) -> let abbrevs = proper_abbrevs p tl !abbreviations in begin match find_repr p !abbrevs with Some ty when repr ty != t -> (* XXX Commentaire... *) Tlink ty | _ -> (* One must allocate a new reference, so that abbrevia- tions belonging to different branches of a type are independent. Moreover, a reference containing a [Mcons] must be shared, so that the memorized expansion of an abbrevi- ation can be released by changing the content of just one reference. *) Tconstr (p, List.map copy tl, ref (match !(!abbreviations) with Mcons _ -> Mlink !abbreviations | abbrev -> abbrev)) end | Tvariant row0 -> let row = row_repr row0 in let more = repr row.row_more in (* We must substitute in a subtle way *) (* Tsubst takes a tuple containing the row var and the variant *) begin match more.desc with Tsubst {desc = Ttuple [_;ty2]} -> (* This variant type has been already copied *) ty.desc <- Tsubst ty2; (* avoid Tlink in the new type *) Tlink ty2 | _ -> (* If the row variable is not generic, we must keep it *) let keep = more.level <> generic_level in let more' = match more.desc with Tsubst ty -> ty | Tconstr _ -> if keep then save_desc more more.desc; copy more | Tvar | Tunivar -> save_desc more more.desc; if keep then more else newty more.desc | _ -> assert false in (* Register new type first for recursion *) more.desc <- Tsubst(newgenty(Ttuple[more';t])); (* Return a new copy *) Tvariant (copy_row copy true row keep more') end | Tfield (p, k, ty1, ty2) -> begin match field_kind_repr k with Fabsent -> Tlink (copy ty2) | Fpresent -> copy_type_desc copy desc | Fvar r -> dup_kind r; copy_type_desc copy desc end | _ -> copy_type_desc copy desc end; t (**** Variants of instantiations ****) let instance sch = let ty = copy sch in cleanup_types (); ty let instance_list schl = let tyl = List.map copy schl in cleanup_types (); tyl let instance_constructor cstr = let ty_res = copy cstr.cstr_res in let ty_args = List.map copy cstr.cstr_args in cleanup_types (); (ty_args, ty_res) let instance_parameterized_type sch_args sch = let ty_args = List.map copy sch_args in let ty = copy sch in cleanup_types (); (ty_args, ty) let instance_parameterized_type_2 sch_args sch_lst sch = let ty_args = List.map copy sch_args in let ty_lst = List.map copy sch_lst in let ty = copy sch in cleanup_types (); (ty_args, ty_lst, ty) let instance_class params cty = let rec copy_class_type = function Tcty_constr (path, tyl, cty) -> Tcty_constr (path, List.map copy tyl, copy_class_type cty) | Tcty_signature sign -> Tcty_signature {cty_self = copy sign.cty_self; cty_vars = Vars.map (function (m, v, ty) -> (m, v, copy ty)) sign.cty_vars; cty_concr = sign.cty_concr; cty_inher = List.map (fun (p,tl) -> (p, List.map copy tl)) sign.cty_inher} | Tcty_fun (l, ty, cty) -> Tcty_fun (l, copy ty, copy_class_type cty) in let params' = List.map copy params in let cty' = copy_class_type cty in cleanup_types (); (params', cty') (**** Instanciation for types with free universal variables ****) module TypeHash = Hashtbl.Make(TypeOps) module TypeSet = Set.Make(TypeOps) type inv_type_expr = { inv_type : type_expr; mutable inv_parents : inv_type_expr list } let rec inv_type hash pty ty = let ty = repr ty in try let inv = TypeHash.find hash ty in inv.inv_parents <- pty @ inv.inv_parents with Not_found -> let inv = { inv_type = ty; inv_parents = pty } in TypeHash.add hash ty inv; iter_type_expr (inv_type hash [inv]) ty let compute_univars ty = let inverted = TypeHash.create 17 in inv_type inverted [] ty; let node_univars = TypeHash.create 17 in let rec add_univar univ inv = match inv.inv_type.desc with Tpoly (ty, tl) when List.memq univ (List.map repr tl) -> () | _ -> try let univs = TypeHash.find node_univars inv.inv_type in if not (TypeSet.mem univ !univs) then begin univs := TypeSet.add univ !univs; List.iter (add_univar univ) inv.inv_parents end with Not_found -> TypeHash.add node_univars inv.inv_type (ref(TypeSet.singleton univ)); List.iter (add_univar univ) inv.inv_parents in TypeHash.iter (fun ty inv -> if ty.desc = Tunivar then add_univar ty inv) inverted; fun ty -> try !(TypeHash.find node_univars ty) with Not_found -> TypeSet.empty let rec diff_list l1 l2 = if l1 == l2 then [] else match l1 with [] -> invalid_arg "Ctype.diff_list" | a :: l1 -> a :: diff_list l1 l2 let conflicts free bound = let bound = List.map repr bound in TypeSet.exists (fun t -> List.memq (repr t) bound) free let delayed_copy = ref [] (* copying to do later *) (* Copy without sharing until there are no free univars left *) (* all free univars must be included in [visited] *) let rec copy_sep fixed free bound visited ty = let ty = repr ty in let univars = free ty in if TypeSet.is_empty univars then if ty.level <> generic_level then ty else let t = newvar () in delayed_copy := lazy (t.desc <- Tlink (copy ty)) :: !delayed_copy; t else try let t, bound_t = List.assq ty visited in let dl = if ty.desc = Tunivar then [] else diff_list bound bound_t in if dl <> [] && conflicts univars dl then raise Not_found; t with Not_found -> begin let t = newvar() in (* Stub *) let visited = match ty.desc with Tarrow _ | Ttuple _ | Tvariant _ | Tconstr _ | Tobject _ -> (ty,(t,bound)) :: visited | _ -> visited in let copy_rec = copy_sep fixed free bound visited in t.desc <- begin match ty.desc with | Tvariant row0 -> let row = row_repr row0 in let more = repr row.row_more in (* We shall really check the level on the row variable *) let keep = more.desc = Tvar && more.level <> generic_level in let more' = copy_rec more in let fixed' = fixed && (repr more').desc = Tvar in let row = copy_row copy_rec fixed' row keep more' in Tvariant row | Tpoly (t1, tl) -> let tl = List.map repr tl in let tl' = List.map (fun t -> newty Tunivar) tl in let bound = tl @ bound in let visited = List.map2 (fun ty t -> ty,(t,bound)) tl tl' @ visited in Tpoly (copy_sep fixed free bound visited t1, tl') | _ -> copy_type_desc copy_rec ty.desc end; t end let instance_poly fixed univars sch = let vars = List.map (fun _ -> newvar ()) univars in let pairs = List.map2 (fun u v -> repr u, (v, [])) univars vars in delayed_copy := []; let ty = copy_sep fixed (compute_univars sch) [] pairs sch in List.iter Lazy.force !delayed_copy; delayed_copy := []; cleanup_types (); vars, ty let instance_label fixed lbl = let ty_res = copy lbl.lbl_res in let vars, ty_arg = match repr lbl.lbl_arg with {desc = Tpoly (ty, tl)} -> instance_poly fixed tl ty | ty -> [], copy lbl.lbl_arg in cleanup_types (); (vars, ty_arg, ty_res) (**** Instantiation with parameter substitution ****) let unify' = (* Forward declaration *) ref (fun env ty1 ty2 -> raise (Unify [])) let rec subst env level priv abbrev ty params args body = if List.length params <> List.length args then raise (Unify []); let old_level = !current_level in current_level := level; try let body0 = newvar () in (* Stub *) begin match ty with None -> () | Some ({desc = Tconstr (path, tl, _)} as ty) -> let abbrev = proper_abbrevs path tl abbrev in memorize_abbrev abbrev priv path ty body0 | _ -> assert false end; abbreviations := abbrev; let (params', body') = instance_parameterized_type params body in abbreviations := ref Mnil; !unify' env body0 body'; List.iter2 (!unify' env) params' args; current_level := old_level; body' with Unify _ as exn -> current_level := old_level; raise exn (* Only the shape of the type matters, not whether is is generic or not. [generic_level] might be somewhat slower, but it ensures invariants on types are enforced (decreasing levels.), and we don't care about efficiency here. *) let apply env params body args = try subst env generic_level Public (ref Mnil) None params args body with Unify _ -> raise Cannot_apply (****************************) (* Abbreviation expansion *) (****************************) (* If the environnement has changed, memorized expansions might not be correct anymore, and so we flush the cache. This is safe but quite pessimistic: it would be enough to flush the cache when a type or module definition is overriden in the environnement. *) let previous_env = ref Env.empty let string_of_kind = function Public -> "public" | Private -> "private" let check_abbrev_env env = if env != !previous_env then begin (* prerr_endline "cleanup expansion cache"; *) cleanup_abbrev (); previous_env := env end (* Expand an abbreviation. The expansion is memorized. *) (* Assume the level is greater than the path binding time of the expanded abbreviation. *) (* An abbreviation expansion will fail in either of these cases: 1. The type constructor does not correspond to a manifest type. 2. The type constructor is defined in an external file, and this file is not in the path (missing -I options). 3. The type constructor is not in the "local" environment. This can happens when a non-generic type variable has been instantiated afterwards to the not yet defined type constructor. (Actually, this cannot happen at the moment due to the strong constraints between type levels and constructor binding time.) 4. The expansion requires the expansion of another abbreviation, and this other expansion fails. *) let expand_abbrev_gen kind find_type_expansion env ty = check_abbrev_env env; match ty with {desc = Tconstr (path, args, abbrev); level = level} -> let lookup_abbrev = proper_abbrevs path args abbrev in begin match find_expans kind path !lookup_abbrev with Some ty -> (* prerr_endline ("found a "^string_of_kind kind^" expansion for "^Path.name path);*) if level <> generic_level then begin try update_level env level ty with Unify _ -> (* XXX This should not happen. However, levels are not correctly restored after a typing error *) () end; ty | None -> let (params, body) = try find_type_expansion path env with Not_found -> raise Cannot_expand in (* prerr_endline ("add a "^string_of_kind kind^" expansion for "^Path.name path);*) let ty' = subst env level kind abbrev (Some ty) params args body in (* Hack to name the variant type *) begin match repr ty' with {desc=Tvariant row} as ty when static_row row -> ty.desc <- Tvariant { row with row_name = Some (path, args) } | _ -> () end; ty' end | _ -> assert false let expand_abbrev = expand_abbrev_gen Public Env.find_type_expansion let safe_abbrev env ty = let snap = Btype.snapshot () in try ignore (expand_abbrev env ty); true with Cannot_expand | Unify _ -> Btype.backtrack snap; false let try_expand_once env ty = let ty = repr ty in match ty.desc with Tconstr _ -> repr (expand_abbrev env ty) | _ -> raise Cannot_expand let _ = forward_try_expand_once := try_expand_once (* Fully expand the head of a type. Raise Cannot_expand if the type cannot be expanded. May raise Unify, if a recursion was hidden in the type. *) let rec try_expand_head env ty = let ty' = try_expand_once env ty in begin try try_expand_head env ty' with Cannot_expand -> ty' end (* Expand once the head of a type *) let expand_head_once env ty = try expand_abbrev env (repr ty) with Cannot_expand -> assert false (* Fully expand the head of a type. *) let expand_head_unif env ty = try try_expand_head env ty with Cannot_expand -> repr ty let expand_head env ty = let snap = Btype.snapshot () in try try_expand_head env ty with Cannot_expand | Unify _ -> (* expand_head shall never fail *) Btype.backtrack snap; repr ty (* Implementing function [expand_head_opt], the compiler's own version of [expand_head] used for type-based optimisations. [expand_head_opt] uses [Env.find_type_expansion_opt] to access the manifest type information of private abstract data types which is normally hidden to the type-checker out of the implementation module of the private abbreviation. *) let expand_abbrev_opt = expand_abbrev_gen Private Env.find_type_expansion_opt let try_expand_once_opt env ty = let ty = repr ty in match ty.desc with Tconstr _ -> repr (expand_abbrev_opt env ty) | _ -> raise Cannot_expand let rec try_expand_head_opt env ty = let ty' = try_expand_once_opt env ty in begin try try_expand_head_opt env ty' with Cannot_expand -> ty' end let expand_head_opt env ty = let snap = Btype.snapshot () in try try_expand_head_opt env ty with Cannot_expand | Unify _ -> (* expand_head shall never fail *) Btype.backtrack snap; repr ty (* Make sure that the type parameters of the type constructor [ty] respect the type constraints *) let enforce_constraints env ty = match ty with {desc = Tconstr (path, args, abbrev); level = level} -> let decl = Env.find_type path env in ignore (subst env level Public (ref Mnil) None decl.type_params args (newvar2 level)) | _ -> assert false (* Recursively expand the head of a type. Also expand #-types. *) let rec full_expand env ty = let ty = repr (expand_head env ty) in match ty.desc with Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar -> newty2 ty.level (Tobject (fi, ref None)) | _ -> ty (* Check whether the abbreviation expands to a well-defined type. During the typing of a class, abbreviations for correspondings types expand to non-generic types. *) let generic_abbrev env path = try let (_, body) = Env.find_type_expansion path env in (repr body).level = generic_level with Not_found -> false (*****************) (* Occur check *) (*****************) exception Occur (* The marks are already used by [expand_abbrev]... *) let visited = ref [] let rec non_recursive_abbrev env ty0 ty = let ty = repr ty in if ty == repr ty0 then raise Recursive_abbrev; if not (List.memq ty !visited) then begin visited := ty :: !visited; match ty.desc with Tconstr(p, args, abbrev) -> begin try non_recursive_abbrev env ty0 (try_expand_once env ty) with Cannot_expand -> if !Clflags.recursive_types then () else iter_type_expr (non_recursive_abbrev env ty0) ty end | Tobject _ | Tvariant _ -> () | _ -> if !Clflags.recursive_types then () else iter_type_expr (non_recursive_abbrev env ty0) ty end let correct_abbrev env path params ty = check_abbrev_env env; let ty0 = newgenvar () in visited := []; let abbrev = Mcons (Public, path, ty0, ty0, Mnil) in simple_abbrevs := abbrev; try non_recursive_abbrev env ty0 (subst env generic_level Public (ref abbrev) None [] [] ty); simple_abbrevs := Mnil; visited := [] with exn -> simple_abbrevs := Mnil; visited := []; raise exn let rec occur_rec env visited ty0 ty = if ty == ty0 then raise Occur; match ty.desc with Tconstr(p, tl, abbrev) -> begin try if List.memq ty visited || !Clflags.recursive_types then raise Occur; iter_type_expr (occur_rec env (ty::visited) ty0) ty with Occur -> try let ty' = try_expand_head env ty in (* Maybe we could simply make a recursive call here, but it seems it could make the occur check loop (see change in rev. 1.58) *) if ty' == ty0 || List.memq ty' visited then raise Occur; match ty'.desc with Tobject _ | Tvariant _ -> () | _ -> if not !Clflags.recursive_types then iter_type_expr (occur_rec env (ty'::visited) ty0) ty' with Cannot_expand -> if not !Clflags.recursive_types then raise Occur end | Tobject _ | Tvariant _ -> () | _ -> if not !Clflags.recursive_types then iter_type_expr (occur_rec env visited ty0) ty let type_changed = ref false (* trace possible changes to the studied type *) let merge r b = if b then r := true let occur env ty0 ty = let old = !type_changed in try while type_changed := false; occur_rec env [] ty0 ty; !type_changed do () (* prerr_endline "changed" *) done; merge type_changed old with exn -> merge type_changed old; raise (match exn with Occur -> Unify [] | _ -> exn) (*****************************) (* Polymorphic Unification *) (*****************************) (* Since we cannot duplicate universal variables, unification must be done at meta-level, using bindings in univar_pairs *) let rec unify_univar t1 t2 = function (cl1, cl2) :: rem -> let find_univ t cl = try let (_, r) = List.find (fun (t',_) -> t == repr t') cl in Some r with Not_found -> None in begin match find_univ t1 cl1, find_univ t2 cl2 with Some {contents=Some t'2}, Some _ when t2 == repr t'2 -> () | Some({contents=None} as r1), Some({contents=None} as r2) -> set_univar r1 t2; set_univar r2 t1 | None, None -> unify_univar t1 t2 rem | _ -> raise (Unify []) end | [] -> raise (Unify []) module TypeMap = Map.Make (TypeOps) (* Test the occurence of free univars in a type *) (* that's way too expansive. Must do some kind of cacheing *) let occur_univar env ty = let visited = ref TypeMap.empty in let rec occur_rec bound ty = let ty = repr ty in if ty.level >= lowest_level && if TypeSet.is_empty bound then (ty.level <- pivot_level - ty.level; true) else try let bound' = TypeMap.find ty !visited in if TypeSet.exists (fun x -> not (TypeSet.mem x bound)) bound' then (visited := TypeMap.add ty (TypeSet.inter bound bound') !visited; true) else false with Not_found -> visited := TypeMap.add ty bound !visited; true then match ty.desc with Tunivar -> if not (TypeSet.mem ty bound) then raise (Unify [ty, newgenvar()]) | Tpoly (ty, tyl) -> let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in occur_rec bound ty | Tconstr (_, [], _) -> () | Tconstr (p, tl, _) -> begin try let td = Env.find_type p env in List.iter2 (fun t (pos,neg,_) -> if pos || neg then occur_rec bound t) tl td.type_variance with Not_found -> List.iter (occur_rec bound) tl end | _ -> iter_type_expr (occur_rec bound) ty in try occur_rec TypeSet.empty ty; unmark_type ty with exn -> unmark_type ty; raise exn (* Grouping univars by families according to their binders *) let add_univars = List.fold_left (fun s (t,_) -> TypeSet.add (repr t) s) let get_univar_family univar_pairs univars = if univars = [] then TypeSet.empty else let rec insert s = function cl1, (_::_ as cl2) -> if List.exists (fun (t1,_) -> TypeSet.mem (repr t1) s) cl1 then add_univars s cl2 else s | _ -> s in let s = List.fold_right TypeSet.add univars TypeSet.empty in List.fold_left insert s univar_pairs (* Whether a family of univars escapes from a type *) let univars_escape env univar_pairs vl ty = let family = get_univar_family univar_pairs vl in let visited = ref TypeSet.empty in let rec occur t = let t = repr t in if TypeSet.mem t !visited then () else begin visited := TypeSet.add t !visited; match t.desc with Tpoly (t, tl) -> if List.exists (fun t -> TypeSet.mem (repr t) family) tl then () else occur t | Tunivar -> if TypeSet.mem t family then raise Occur | Tconstr (_, [], _) -> () | Tconstr (p, tl, _) -> begin try let td = Env.find_type p env in List.iter2 (fun t (pos,neg,_) -> if pos || neg then occur t) tl td.type_variance with Not_found -> List.iter occur tl end | _ -> iter_type_expr occur t end in try occur ty; false with Occur -> true (* Wrapper checking that no variable escapes and updating univar_pairs *) let enter_poly env univar_pairs t1 tl1 t2 tl2 f = let old_univars = !univar_pairs in let known_univars = List.fold_left (fun s (cl,_) -> add_univars s cl) TypeSet.empty old_univars in let tl1 = List.map repr tl1 and tl2 = List.map repr tl2 in if List.exists (fun t -> TypeSet.mem t known_univars) tl1 && univars_escape env old_univars tl1 (newty(Tpoly(t2,tl2))) || List.exists (fun t -> TypeSet.mem t known_univars) tl2 && univars_escape env old_univars tl2 (newty(Tpoly(t1,tl1))) then raise (Unify []); let cl1 = List.map (fun t -> t, ref None) tl1 and cl2 = List.map (fun t -> t, ref None) tl2 in univar_pairs := (cl1,cl2) :: (cl2,cl1) :: old_univars; try let res = f t1 t2 in univar_pairs := old_univars; res with exn -> univar_pairs := old_univars; raise exn let univar_pairs = ref [] (*****************) (* Unification *) (*****************) let rec has_cached_expansion p abbrev = match abbrev with Mnil -> false | Mcons(_, p', _, _, rem) -> Path.same p p' || has_cached_expansion p rem | Mlink rem -> has_cached_expansion p !rem (**** Transform error trace ****) (* +++ Move it to some other place ? *) let expand_trace env trace = List.fold_right (fun (t1, t2) rem -> (repr t1, full_expand env t1)::(repr t2, full_expand env t2)::rem) trace [] (* build a dummy variant type *) let mkvariant fields closed = newgenty (Tvariant {row_fields = fields; row_closed = closed; row_more = newvar(); row_bound = (); row_fixed = false; row_name = None }) (* force unification in Reither when one side has as non-conjunctive type *) let rigid_variants = ref false (**** Unification ****) (* Return whether [t0] occurs in [ty]. Objects are also traversed. *) let deep_occur t0 ty = let rec occur_rec ty = let ty = repr ty in if ty.level >= lowest_level then begin if ty == t0 then raise Occur; ty.level <- pivot_level - ty.level; iter_type_expr occur_rec ty end in try occur_rec ty; unmark_type ty; false with Occur -> unmark_type ty; true (* 1. When unifying two non-abbreviated types, one type is made a link to the other. When unifying an abbreviated type with a non-abbreviated type, the non-abbreviated type is made a link to the other one. When unifying to abbreviated types, these two types are kept distincts, but they are made to (temporally) expand to the same type. 2. Abbreviations with at least one parameter are systematically expanded. The overhead does not seem to high, and that way abbreviations where some parameters does not appear in the expansion, such as ['a t = int], are correctly handled. In particular, for this example, unifying ['a t] with ['b t] keeps ['a] and ['b] distincts. (Is it really important ?) 3. Unifying an abbreviation ['a t = 'a] with ['a] should not yield ['a t as 'a]. Indeed, the type variable would otherwise be lost. This problem occurs for abbreviations expanding to a type variable, but also to many other constrained abbreviations (for instance, [(< x : 'a > -> unit) t = ]). The solution is that, if an abbreviation is unified with some subpart of its parameters, then the parameter actually does not get abbreviated. It would be possible to check whether some information is indeed lost, but it probably does not worth it. *) let rec unify env t1 t2 = (* First step: special cases (optimizations) *) if t1 == t2 then () else let t1 = repr t1 in let t2 = repr t2 in if t1 == t2 then () else try type_changed := true; match (t1.desc, t2.desc) with (Tvar, Tconstr _) when deep_occur t1 t2 -> unify2 env t1 t2 | (Tconstr _, Tvar) when deep_occur t2 t1 -> unify2 env t1 t2 | (Tvar, _) -> occur env t1 t2; occur_univar env t2; update_level env t1.level t2; link_type t1 t2 | (_, Tvar) -> occur env t2 t1; occur_univar env t1; update_level env t2.level t1; link_type t2 t1 | (Tunivar, Tunivar) -> unify_univar t1 t2 !univar_pairs; update_level env t1.level t2; link_type t1 t2 | (Tconstr (p1, [], a1), Tconstr (p2, [], a2)) when Path.same p1 p2 (* This optimization assumes that t1 does not expand to t2 (and conversely), so we fall back to the general case when any of the types has a cached expansion. *) && not (has_cached_expansion p1 !a1 || has_cached_expansion p2 !a2) -> update_level env t1.level t2; link_type t1 t2 | _ -> unify2 env t1 t2 with Unify trace -> raise (Unify ((t1, t2)::trace)) and unify2 env t1 t2 = (* Second step: expansion of abbreviations *) let rec expand_both t1'' t2'' = let t1' = expand_head_unif env t1 in let t2' = expand_head_unif env t2 in (* Expansion may have changed the representative of the types... *) if t1' == t1'' && t2' == t2'' then (t1',t2') else expand_both t1' t2' in let t1', t2' = expand_both t1 t2 in if t1' == t2' then () else let t1 = repr t1 and t2 = repr t2 in if (t1 == t1') || (t2 != t2') then unify3 env t1 t1' t2 t2' else try unify3 env t2 t2' t1 t1' with Unify trace -> raise (Unify (List.map (fun (x, y) -> (y, x)) trace)) and unify3 env t1 t1' t2 t2' = (* Third step: truly unification *) (* Assumes either [t1 == t1'] or [t2 != t2'] *) let d1 = t1'.desc and d2 = t2'.desc in let create_recursion = (t2 != t2') && (deep_occur t1' t2) in occur env t1' t2; update_level env t1'.level t2; link_type t1' t2; try begin match (d1, d2) with (Tvar, _) -> occur_univar env t2 | (_, Tvar) -> let td1 = newgenty d1 in occur env t2' td1; occur_univar env td1; if t1 == t1' then begin (* The variable must be instantiated... *) let ty = newty2 t1'.level d1 in update_level env t2'.level ty; link_type t2' ty end else begin log_type t1'; t1'.desc <- d1; update_level env t2'.level t1; link_type t2' t1 end | (Tarrow (l1, t1, u1, c1), Tarrow (l2, t2, u2, c2)) when l1 = l2 || !Clflags.classic && not (is_optional l1 || is_optional l2) -> unify env t1 t2; unify env u1 u2; begin match commu_repr c1, commu_repr c2 with Clink r, c2 -> set_commu r c2 | c1, Clink r -> set_commu r c1 | _ -> () end | (Ttuple tl1, Ttuple tl2) -> unify_list env tl1 tl2 | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 -> unify_list env tl1 tl2 | (Tobject (fi1, nm1), Tobject (fi2, _)) -> unify_fields env fi1 fi2; (* Type [t2'] may have been instantiated by [unify_fields] *) (* XXX One should do some kind of unification... *) begin match (repr t2').desc with Tobject (_, {contents = Some (_, va::_)}) when let va = repr va in List.mem va.desc [Tvar; Tunivar; Tnil] -> () | Tobject (_, nm2) -> set_name nm2 !nm1 | _ -> () end | (Tvariant row1, Tvariant row2) -> unify_row env row1 row2 | (Tfield _, Tfield _) -> (* Actually unused *) unify_fields env t1' t2' | (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) -> begin match field_kind_repr kind with Fvar r when f <> dummy_method -> set_kind r Fabsent | _ -> raise (Unify []) end | (Tnil, Tnil) -> () | (Tpoly (t1, []), Tpoly (t2, [])) -> unify env t1 t2 | (Tpoly (t1, tl1), Tpoly (t2, tl2)) -> enter_poly env univar_pairs t1 tl1 t2 tl2 (unify env) | (_, _) -> raise (Unify []) end; (* XXX Commentaires + changer "create_recursion" *) if create_recursion then begin match t2.desc with Tconstr (p, tl, abbrev) -> forget_abbrev abbrev p; let t2'' = expand_head_unif env t2 in if not (closed_parameterized_type tl t2'') then link_type (repr t2) (repr t2') | _ -> () (* t2 has already been expanded by update_level *) end (* (* Can only be done afterwards, once the row variable has (possibly) been instantiated. *) if t1 != t1' (* && t2 != t2' *) then begin match (t1.desc, t2.desc) with (Tconstr (p, ty::_, _), _) when ((repr ty).desc <> Tvar) && weak_abbrev p && not (deep_occur t1 t2) -> update_level env t1.level t2; link_type t1 t2 | (_, Tconstr (p, ty::_, _)) when ((repr ty).desc <> Tvar) && weak_abbrev p && not (deep_occur t2 t1) -> update_level env t2.level t1; link_type t2 t1; link_type t1' t2' | _ -> () end *) with Unify trace -> t1'.desc <- d1; raise (Unify trace) and unify_list env tl1 tl2 = if List.length tl1 <> List.length tl2 then raise (Unify []); List.iter2 (unify env) tl1 tl2 and unify_fields env ty1 ty2 = (* Optimization *) let (fields1, rest1) = flatten_fields ty1 and (fields2, rest2) = flatten_fields ty2 in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in let l1 = (repr ty1).level and l2 = (repr ty2).level in let va = if miss1 = [] then rest2 else if miss2 = [] then rest1 else newty2 (min l1 l2) Tvar in let d1 = rest1.desc and d2 = rest2.desc in try unify env (build_fields l1 miss1 va) rest2; unify env rest1 (build_fields l2 miss2 va); List.iter (fun (n, k1, t1, k2, t2) -> unify_kind k1 k2; try unify env t1 t2 with Unify trace -> raise (Unify ((newty (Tfield(n, k1, t1, va)), newty (Tfield(n, k2, t2, va)))::trace))) pairs with exn -> log_type rest1; rest1.desc <- d1; log_type rest2; rest2.desc <- d2; raise exn and unify_kind k1 k2 = let k1 = field_kind_repr k1 in let k2 = field_kind_repr k2 in if k1 == k2 then () else match k1, k2 with (Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2 | (Fpresent, Fvar r) -> set_kind r k1 | (Fpresent, Fpresent) -> () | _ -> assert false and unify_pairs env tpl = List.iter (fun (t1, t2) -> unify env t1 t2) tpl and unify_row env row1 row2 = let row1 = row_repr row1 and row2 = row_repr row2 in let rm1 = row_more row1 and rm2 = row_more row2 in if rm1 == rm2 then () else let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in if r1 <> [] && r2 <> [] then begin let ht = Hashtbl.create (List.length r1) in List.iter (fun (l,_) -> Hashtbl.add ht (hash_variant l) l) r1; List.iter (fun (l,_) -> try raise (Tags(l, Hashtbl.find ht (hash_variant l))) with Not_found -> ()) r2 end; let more = if row1.row_fixed then rm1 else if row2.row_fixed then rm2 else newgenvar () in update_level env (min rm1.level rm2.level) more; let fixed = row1.row_fixed || row2.row_fixed and closed = row1.row_closed || row2.row_closed in let keep switch = List.for_all (fun (_,f1,f2) -> let f1, f2 = switch f1 f2 in row_field_repr f1 = Rabsent || row_field_repr f2 <> Rabsent) pairs in let empty fields = List.for_all (fun (_,f) -> row_field_repr f = Rabsent) fields in (* Check whether we are going to build an empty type *) if closed && (empty r1 || row2.row_closed) && (empty r2 || row1.row_closed) && List.for_all (fun (_,f1,f2) -> row_field_repr f1 = Rabsent || row_field_repr f2 = Rabsent) pairs then raise (Unify [mkvariant [] true, mkvariant [] true]); let name = if row1.row_name <> None && (row1.row_closed || empty r2) && (not row2.row_closed || keep (fun f1 f2 -> f1, f2) && empty r1) then row1.row_name else if row2.row_name <> None && (row2.row_closed || empty r1) && (not row1.row_closed || keep (fun f1 f2 -> f2, f1) && empty r2) then row2.row_name else None in let row0 = {row_fields = []; row_more = more; row_bound = (); row_closed = closed; row_fixed = fixed; row_name = name} in let set_more row rest = let rest = if closed then filter_row_fields row.row_closed rest else rest in if rest <> [] && (row.row_closed || row.row_fixed) || closed && row.row_fixed && not row.row_closed then begin let t1 = mkvariant [] true and t2 = mkvariant rest false in raise (Unify [if row == row1 then (t1,t2) else (t2,t1)]) end; let rm = row_more row in if row.row_fixed then if row0.row_more == rm then () else if rm.desc = Tvar then link_type rm row0.row_more else unify env rm row0.row_more else let ty = newty2 generic_level (Tvariant {row0 with row_fields = rest}) in update_level env rm.level ty; link_type rm ty in let md1 = rm1.desc and md2 = rm2.desc in begin try set_more row2 r1; set_more row1 r2; List.iter (fun (l,f1,f2) -> try unify_row_field env row1.row_fixed row2.row_fixed l f1 f2 with Unify trace -> raise (Unify ((mkvariant [l,f1] true, mkvariant [l,f2] true) :: trace))) pairs; with exn -> log_type rm1; rm1.desc <- md1; log_type rm2; rm2.desc <- md2; raise exn end and unify_row_field env fixed1 fixed2 l f1 f2 = let f1 = row_field_repr f1 and f2 = row_field_repr f2 in if f1 == f2 then () else match f1, f2 with Rpresent(Some t1), Rpresent(Some t2) -> unify env t1 t2 | Rpresent None, Rpresent None -> () | Reither(c1, tl1, m1, e1), Reither(c2, tl2, m2, e2) -> if e1 == e2 then () else let redo = (m1 || m2 || !rigid_variants && (List.length tl1 = 1 || List.length tl2 = 1)) && begin match tl1 @ tl2 with [] -> false | t1 :: tl -> if c1 || c2 then raise (Unify []); List.iter (unify env t1) tl; !e1 <> None || !e2 <> None end in if redo then unify_row_field env fixed1 fixed2 l f1 f2 else let tl1 = List.map repr tl1 and tl2 = List.map repr tl2 in let rec remq tl = function [] -> [] | ty :: tl' -> if List.memq ty tl then remq tl tl' else ty :: remq tl tl' in let tl2' = remq tl2 tl1 and tl1' = remq tl1 tl2 in let e = ref None in let f1' = Reither(c1 || c2, tl1', m1 || m2, e) and f2' = Reither(c1 || c2, tl2', m1 || m2, e) in set_row_field e1 f1'; set_row_field e2 f2'; | Reither(_, _, false, e1), Rabsent -> set_row_field e1 f2 | Rabsent, Reither(_, _, false, e2) -> set_row_field e2 f1 | Rabsent, Rabsent -> () | Reither(false, tl, _, e1), Rpresent(Some t2) when not fixed1 -> set_row_field e1 f2; (try List.iter (fun t1 -> unify env t1 t2) tl with exn -> e1 := None; raise exn) | Rpresent(Some t1), Reither(false, tl, _, e2) when not fixed2 -> set_row_field e2 f1; (try List.iter (unify env t1) tl with exn -> e2 := None; raise exn) | Reither(true, [], _, e1), Rpresent None when not fixed1 -> set_row_field e1 f2 | Rpresent None, Reither(true, [], _, e2) when not fixed2 -> set_row_field e2 f1 | _ -> raise (Unify []) let unify env ty1 ty2 = try unify env ty1 ty2 with Unify trace -> raise (Unify (expand_trace env trace)) let unify_var env t1 t2 = let t1 = repr t1 and t2 = repr t2 in if t1 == t2 then () else match t1.desc with Tvar -> begin try occur env t1 t2; update_level env t1.level t2; link_type t1 t2 with Unify trace -> raise (Unify (expand_trace env ((t1,t2)::trace))) end | _ -> unify env t1 t2 let _ = unify' := unify_var let unify_pairs env ty1 ty2 pairs = univar_pairs := pairs; unify env ty1 ty2 let unify env ty1 ty2 = univar_pairs := []; unify env ty1 ty2 (**** Special cases of unification ****) (* Unify [t] and [l:'a -> 'b]. Return ['a] and ['b]. In label mode, label mismatch is accepted when (1) the requested label is "" (2) the original label is not optional *) let rec filter_arrow env t l = let t = expand_head_unif env t in match t.desc with Tvar -> let t1 = newvar () and t2 = newvar () in let t' = newty (Tarrow (l, t1, t2, Cok)) in update_level env t.level t'; link_type t t'; (t1, t2) | Tarrow(l', t1, t2, _) when l = l' || !Clflags.classic && l = "" && not (is_optional l') -> (t1, t2) | _ -> raise (Unify []) (* Used by [filter_method]. *) let rec filter_method_field env name priv ty = let ty = repr ty in match ty.desc with Tvar -> let level = ty.level in let ty1 = newvar2 level and ty2 = newvar2 level in let ty' = newty2 level (Tfield (name, begin match priv with Private -> Fvar (ref None) | Public -> Fpresent end, ty1, ty2)) in link_type ty ty'; ty1 | Tfield(n, kind, ty1, ty2) -> let kind = field_kind_repr kind in if (n = name) && (kind <> Fabsent) then begin if priv = Public then unify_kind kind Fpresent; ty1 end else filter_method_field env name priv ty2 | _ -> raise (Unify []) (* Unify [ty] and [< name : 'a; .. >]. Return ['a]. *) let rec filter_method env name priv ty = let ty = expand_head_unif env ty in match ty.desc with Tvar -> let ty1 = newvar () in let ty' = newobj ty1 in update_level env ty.level ty'; link_type ty ty'; filter_method_field env name priv ty1 | Tobject(f, _) -> filter_method_field env name priv f | _ -> raise (Unify []) let check_filter_method env name priv ty = ignore(filter_method env name priv ty) let filter_self_method env lab priv meths ty = let ty' = filter_method env lab priv ty in try Meths.find lab !meths with Not_found -> let pair = (Ident.create lab, ty') in meths := Meths.add lab pair !meths; pair (***********************************) (* Matching between type schemes *) (***********************************) (* Update the level of [ty]. First check that the levels of generic variables from the subject are not lowered. *) let moregen_occur env level ty = let rec occur ty = let ty = repr ty in if ty.level > level then begin if ty.desc = Tvar && ty.level >= generic_level - 1 then raise Occur; ty.level <- pivot_level - ty.level; match ty.desc with Tvariant row when static_row row -> iter_row occur row | _ -> iter_type_expr occur ty end in begin try occur ty; unmark_type ty with Occur -> unmark_type ty; raise (Unify []) end; (* also check for free univars *) occur_univar env ty; update_level env level ty let may_instantiate inst_nongen t1 = if inst_nongen then t1.level <> generic_level - 1 else t1.level = generic_level let rec moregen inst_nongen type_pairs env t1 t2 = if t1 == t2 then () else let t1 = repr t1 in let t2 = repr t2 in if t1 == t2 then () else try match (t1.desc, t2.desc) with (Tunivar, Tunivar) -> unify_univar t1 t2 !univar_pairs | (Tvar, _) when may_instantiate inst_nongen t1 -> moregen_occur env t1.level t2; occur env t1 t2; link_type t1 t2 | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 -> () | _ -> let t1' = expand_head_unif env t1 in let t2' = expand_head_unif env t2 in (* Expansion may have changed the representative of the types... *) let t1' = repr t1' and t2' = repr t2' in if t1' == t2' then () else begin try TypePairs.find type_pairs (t1', t2') with Not_found -> TypePairs.add type_pairs (t1', t2') (); match (t1'.desc, t2'.desc) with (Tvar, _) when may_instantiate inst_nongen t1' -> moregen_occur env t1'.level t2; link_type t1' t2 | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2 || !Clflags.classic && not (is_optional l1 || is_optional l2) -> moregen inst_nongen type_pairs env t1 t2; moregen inst_nongen type_pairs env u1 u2 | (Ttuple tl1, Ttuple tl2) -> moregen_list inst_nongen type_pairs env tl1 tl2 | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 -> moregen_list inst_nongen type_pairs env tl1 tl2 | (Tvariant row1, Tvariant row2) -> moregen_row inst_nongen type_pairs env row1 row2 | (Tobject (fi1, nm1), Tobject (fi2, nm2)) -> moregen_fields inst_nongen type_pairs env fi1 fi2 | (Tfield _, Tfield _) -> (* Actually unused *) moregen_fields inst_nongen type_pairs env t1' t2' | (Tnil, Tnil) -> () | (Tpoly (t1, []), Tpoly (t2, [])) -> moregen inst_nongen type_pairs env t1 t2 | (Tpoly (t1, tl1), Tpoly (t2, tl2)) -> enter_poly env univar_pairs t1 tl1 t2 tl2 (moregen inst_nongen type_pairs env) | (_, _) -> raise (Unify []) end with Unify trace -> raise (Unify ((t1, t2)::trace)) and moregen_list inst_nongen type_pairs env tl1 tl2 = if List.length tl1 <> List.length tl2 then raise (Unify []); List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2 and moregen_fields inst_nongen type_pairs env ty1 ty2 = let (fields1, rest1) = flatten_fields ty1 and (fields2, rest2) = flatten_fields ty2 in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in if miss1 <> [] then raise (Unify []); moregen inst_nongen type_pairs env rest1 (build_fields (repr ty2).level miss2 rest2); List.iter (fun (n, k1, t1, k2, t2) -> moregen_kind k1 k2; try moregen inst_nongen type_pairs env t1 t2 with Unify trace -> raise (Unify ((newty (Tfield(n, k1, t1, rest2)), newty (Tfield(n, k2, t2, rest2)))::trace))) pairs and moregen_kind k1 k2 = let k1 = field_kind_repr k1 in let k2 = field_kind_repr k2 in if k1 == k2 then () else match k1, k2 with (Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2 | (Fpresent, Fpresent) -> () | _ -> raise (Unify []) and moregen_row inst_nongen type_pairs env row1 row2 = let row1 = row_repr row1 and row2 = row_repr row2 in let rm1 = repr row1.row_more and rm2 = repr row2.row_more in if rm1 == rm2 then () else let may_inst = rm1.desc = Tvar && may_instantiate inst_nongen rm1 in let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in let r1, r2 = if row2.row_closed then filter_row_fields may_inst r1, filter_row_fields false r2 else r1, r2 in if r1 <> [] || row1.row_closed && (not row2.row_closed || r2 <> []) then raise (Unify []); begin match rm1.desc, rm2.desc with Tunivar, Tunivar -> unify_univar rm1 rm2 !univar_pairs | Tunivar, _ | _, Tunivar -> raise (Unify []) | _ when static_row row1 -> () | _ when may_inst -> if not (static_row row2) then moregen_occur env rm1.level rm2; let ext = if r2 = [] then rm2 else let row_ext = {row2 with row_fields = r2} in iter_row (moregen_occur env rm1.level) row_ext; newty2 rm1.level (Tvariant row_ext) in link_type rm1 ext | Tconstr _, Tconstr _ -> moregen inst_nongen type_pairs env rm1 rm2 | _ -> raise (Unify []) end; List.iter (fun (l,f1,f2) -> let f1 = row_field_repr f1 and f2 = row_field_repr f2 in if f1 == f2 then () else match f1, f2 with Rpresent(Some t1), Rpresent(Some t2) -> moregen inst_nongen type_pairs env t1 t2 | Rpresent None, Rpresent None -> () | Reither(false, tl1, _, e1), Rpresent(Some t2) when may_inst -> set_row_field e1 f2; List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2) tl1 | Reither(c1, tl1, _, e1), Reither(c2, tl2, m2, e2) -> if e1 != e2 then begin if c1 && not c2 then raise(Unify []); set_row_field e1 (Reither (c2, [], m2, e2)); if List.length tl1 = List.length tl2 then List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2 else match tl2 with t2 :: _ -> List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2) tl1 | [] -> if tl1 <> [] then raise (Unify []) end | Reither(true, [], _, e1), Rpresent None when may_inst -> set_row_field e1 f2 | Reither(_, _, _, e1), Rabsent when may_inst -> set_row_field e1 f2 | Rabsent, Rabsent -> () | _ -> raise (Unify [])) pairs (* Must empty univar_pairs first *) let moregen inst_nongen type_pairs env patt subj = univar_pairs := []; moregen inst_nongen type_pairs env patt subj (* Non-generic variable can be instanciated only if [inst_nongen] is true. So, [inst_nongen] should be set to false if the subject might contain non-generic variables (and we do not want them to be instanciated). Usually, the subject is given by the user, and the pattern is unimportant. So, no need to propagate abbreviations. *) let moregeneral env inst_nongen pat_sch subj_sch = let old_level = !current_level in current_level := generic_level - 1; (* Generic variables are first duplicated with [instance]. So, their levels are lowered to [generic_level - 1]. The subject is then copied with [duplicate_type]. That way, its levels won't be changed. *) let subj = duplicate_type (instance subj_sch) in current_level := generic_level; (* Duplicate generic variables *) let patt = instance pat_sch in let res = try moregen inst_nongen (TypePairs.create 13) env patt subj; true with Unify _ -> false in current_level := old_level; res (* Alternative approach: "rigidify" a type scheme, and check validity after unification *) (* Simpler, no? *) let rec rigidify_rec vars ty = let ty = repr ty in if ty.level >= lowest_level then begin ty.level <- pivot_level - ty.level; match ty.desc with | Tvar -> if not (List.memq ty !vars) then vars := ty :: !vars | Tvariant row -> let row = row_repr row in let more = repr row.row_more in if more.desc = Tvar && not row.row_fixed then begin let more' = newty2 more.level Tvar in let row' = {row with row_fixed=true; row_fields=[]; row_more=more'} in link_type more (newty2 ty.level (Tvariant row')) end; iter_row (rigidify_rec vars) row; (* only consider the row variable if the variant is not static *) if not (static_row row) then rigidify_rec vars (row_more row) | _ -> iter_type_expr (rigidify_rec vars) ty end let rigidify ty = let vars = ref [] in rigidify_rec vars ty; unmark_type ty; !vars let all_distinct_vars env vars = let tyl = ref [] in List.for_all (fun ty -> let ty = expand_head env ty in if List.memq ty !tyl then false else (tyl := ty :: !tyl; ty.desc = Tvar)) vars let matches env ty ty' = let snap = snapshot () in let vars = rigidify ty in cleanup_abbrev (); let ok = try unify env ty ty'; all_distinct_vars env vars with Unify _ -> false in backtrack snap; ok (*********************************************) (* Equivalence between parameterized types *) (*********************************************) let expand_head_rigid env ty = let old = !rigid_variants in rigid_variants := true; let ty' = expand_head_unif env ty in rigid_variants := old; ty' let normalize_subst subst = if List.exists (function {desc=Tlink _}, _ | _, {desc=Tlink _} -> true | _ -> false) !subst then subst := List.map (fun (t1,t2) -> repr t1, repr t2) !subst let rec eqtype rename type_pairs subst env t1 t2 = if t1 == t2 then () else let t1 = repr t1 in let t2 = repr t2 in if t1 == t2 then () else try match (t1.desc, t2.desc) with (Tvar, Tvar) when rename -> begin try normalize_subst subst; if List.assq t1 !subst != t2 then raise (Unify []) with Not_found -> subst := (t1, t2) :: !subst end | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 -> () | _ -> let t1' = expand_head_rigid env t1 in let t2' = expand_head_rigid env t2 in (* Expansion may have changed the representative of the types... *) let t1' = repr t1' and t2' = repr t2' in if t1' == t2' then () else begin try TypePairs.find type_pairs (t1', t2') with Not_found -> TypePairs.add type_pairs (t1', t2') (); match (t1'.desc, t2'.desc) with (Tvar, Tvar) when rename -> begin try normalize_subst subst; if List.assq t1' !subst != t2' then raise (Unify []) with Not_found -> subst := (t1', t2') :: !subst end | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2 || !Clflags.classic && not (is_optional l1 || is_optional l2) -> eqtype rename type_pairs subst env t1 t2; eqtype rename type_pairs subst env u1 u2; | (Ttuple tl1, Ttuple tl2) -> eqtype_list rename type_pairs subst env tl1 tl2 | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 -> eqtype_list rename type_pairs subst env tl1 tl2 | (Tvariant row1, Tvariant row2) -> eqtype_row rename type_pairs subst env row1 row2 | (Tobject (fi1, nm1), Tobject (fi2, nm2)) -> eqtype_fields rename type_pairs subst env fi1 fi2 | (Tfield _, Tfield _) -> (* Actually unused *) eqtype_fields rename type_pairs subst env t1' t2' | (Tnil, Tnil) -> () | (Tpoly (t1, []), Tpoly (t2, [])) -> eqtype rename type_pairs subst env t1 t2 | (Tpoly (t1, tl1), Tpoly (t2, tl2)) -> enter_poly env univar_pairs t1 tl1 t2 tl2 (eqtype rename type_pairs subst env) | (Tunivar, Tunivar) -> unify_univar t1' t2' !univar_pairs | (_, _) -> raise (Unify []) end with Unify trace -> raise (Unify ((t1, t2)::trace)) and eqtype_list rename type_pairs subst env tl1 tl2 = if List.length tl1 <> List.length tl2 then raise (Unify []); List.iter2 (eqtype rename type_pairs subst env) tl1 tl2 and eqtype_fields rename type_pairs subst env ty1 ty2 = let (fields2, rest2) = flatten_fields ty2 in (* Try expansion, needed when called from Includecore.type_manifest *) match expand_head_rigid env rest2 with {desc=Tobject(ty2,_)} -> eqtype_fields rename type_pairs subst env ty1 ty2 | _ -> let (fields1, rest1) = flatten_fields ty1 in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in eqtype rename type_pairs subst env rest1 rest2; if (miss1 <> []) || (miss2 <> []) then raise (Unify []); List.iter (function (n, k1, t1, k2, t2) -> eqtype_kind k1 k2; try eqtype rename type_pairs subst env t1 t2 with Unify trace -> raise (Unify ((newty (Tfield(n, k1, t1, rest2)), newty (Tfield(n, k2, t2, rest2)))::trace))) pairs and eqtype_kind k1 k2 = let k1 = field_kind_repr k1 in let k2 = field_kind_repr k2 in match k1, k2 with (Fvar _, Fvar _) | (Fpresent, Fpresent) -> () | _ -> raise (Unify []) and eqtype_row rename type_pairs subst env row1 row2 = (* Try expansion, needed when called from Includecore.type_manifest *) match expand_head_rigid env (row_more row2) with {desc=Tvariant row2} -> eqtype_row rename type_pairs subst env row1 row2 | _ -> let row1 = row_repr row1 and row2 = row_repr row2 in let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in if row1.row_closed <> row2.row_closed || not row1.row_closed && (r1 <> [] || r2 <> []) || filter_row_fields false (r1 @ r2) <> [] then raise (Unify []); if not (static_row row1) then eqtype rename type_pairs subst env row1.row_more row2.row_more; List.iter (fun (_,f1,f2) -> match row_field_repr f1, row_field_repr f2 with Rpresent(Some t1), Rpresent(Some t2) -> eqtype rename type_pairs subst env t1 t2 | Reither(true, [], _, _), Reither(true, [], _, _) -> () | Reither(false, t1::tl1, _, _), Reither(false, t2::tl2, _, _) -> eqtype rename type_pairs subst env t1 t2; if List.length tl1 = List.length tl2 then (* if same length allow different types (meaning?) *) List.iter2 (eqtype rename type_pairs subst env) tl1 tl2 else begin (* otherwise everything must be equal *) List.iter (eqtype rename type_pairs subst env t1) tl2; List.iter (fun t1 -> eqtype rename type_pairs subst env t1 t2) tl1 end | Rpresent None, Rpresent None -> () | Rabsent, Rabsent -> () | _ -> raise (Unify [])) pairs (* Two modes: with or without renaming of variables *) let equal env rename tyl1 tyl2 = try univar_pairs := []; eqtype_list rename (TypePairs.create 11) (ref []) env tyl1 tyl2; true with Unify _ -> false (* Must empty univar_pairs first *) let eqtype rename type_pairs subst env t1 t2 = univar_pairs := []; eqtype rename type_pairs subst env t1 t2 (*************************) (* Class type matching *) (*************************) type class_match_failure = CM_Virtual_class | CM_Parameter_arity_mismatch of int * int | CM_Type_parameter_mismatch of (type_expr * type_expr) list | CM_Class_type_mismatch of class_type * class_type | CM_Parameter_mismatch of (type_expr * type_expr) list | CM_Val_type_mismatch of string * (type_expr * type_expr) list | CM_Meth_type_mismatch of string * (type_expr * type_expr) list | CM_Non_mutable_value of string | CM_Non_concrete_value of string | CM_Missing_value of string | CM_Missing_method of string | CM_Hide_public of string | CM_Hide_virtual of string * string | CM_Public_method of string | CM_Private_method of string | CM_Virtual_method of string exception Failure of class_match_failure list let rec moregen_clty trace type_pairs env cty1 cty2 = try match cty1, cty2 with Tcty_constr (_, _, cty1), _ -> moregen_clty true type_pairs env cty1 cty2 | _, Tcty_constr (_, _, cty2) -> moregen_clty true type_pairs env cty1 cty2 | Tcty_fun (l1, ty1, cty1'), Tcty_fun (l2, ty2, cty2') when l1 = l2 -> begin try moregen true type_pairs env ty1 ty2 with Unify trace -> raise (Failure [CM_Parameter_mismatch (expand_trace env trace)]) end; moregen_clty false type_pairs env cty1' cty2' | Tcty_signature sign1, Tcty_signature sign2 -> let ty1 = object_fields (repr sign1.cty_self) in let ty2 = object_fields (repr sign2.cty_self) in let (fields1, rest1) = flatten_fields ty1 and (fields2, rest2) = flatten_fields ty2 in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in List.iter (fun (lab, k1, t1, k2, t2) -> begin try moregen true type_pairs env t1 t2 with Unify trace -> raise (Failure [CM_Meth_type_mismatch (lab, expand_trace env trace)]) end) pairs; Vars.iter (fun lab (mut, v, ty) -> let (mut', v', ty') = Vars.find lab sign1.cty_vars in try moregen true type_pairs env ty' ty with Unify trace -> raise (Failure [CM_Val_type_mismatch (lab, expand_trace env trace)])) sign2.cty_vars | _ -> raise (Failure []) with Failure error when trace -> raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error)) let match_class_types env pat_sch subj_sch = let type_pairs = TypePairs.create 53 in let old_level = !current_level in current_level := generic_level - 1; (* Generic variables are first duplicated with [instance]. So, their levels are lowered to [generic_level - 1]. The subject is then copied with [duplicate_type]. That way, its levels won't be changed. *) let (_, subj_inst) = instance_class [] subj_sch in let subj = duplicate_class_type subj_inst in current_level := generic_level; (* Duplicate generic variables *) let (_, patt) = instance_class [] pat_sch in let res = let sign1 = signature_of_class_type patt in let sign2 = signature_of_class_type subj in let t1 = repr sign1.cty_self in let t2 = repr sign2.cty_self in TypePairs.add type_pairs (t1, t2) (); let (fields1, rest1) = flatten_fields (object_fields t1) and (fields2, rest2) = flatten_fields (object_fields t2) in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in let error = List.fold_right (fun (lab, k, _) err -> let err = let k = field_kind_repr k in begin match k with Fvar r -> set_kind r Fabsent; err | _ -> CM_Hide_public lab::err end in if Concr.mem lab sign1.cty_concr then err else CM_Hide_virtual ("method", lab) :: err) miss1 [] in let missing_method = List.map (fun (m, _, _) -> m) miss2 in let error = (List.map (fun m -> CM_Missing_method m) missing_method) @ error in (* Always succeeds *) moregen true type_pairs env rest1 rest2; let error = List.fold_right (fun (lab, k1, t1, k2, t2) err -> try moregen_kind k1 k2; err with Unify _ -> CM_Public_method lab::err) pairs error in let error = Vars.fold (fun lab (mut, vr, ty) err -> try let (mut', vr', ty') = Vars.find lab sign1.cty_vars in if mut = Mutable && mut' <> Mutable then CM_Non_mutable_value lab::err else if vr = Concrete && vr' <> Concrete then CM_Non_concrete_value lab::err else err with Not_found -> CM_Missing_value lab::err) sign2.cty_vars error in let error = Vars.fold (fun lab (_,vr,_) err -> if vr = Virtual && not (Vars.mem lab sign2.cty_vars) then CM_Hide_virtual ("instance variable", lab) :: err else err) sign1.cty_vars error in let error = List.fold_right (fun e l -> if List.mem e missing_method then l else CM_Virtual_method e::l) (Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr)) error in match error with [] -> begin try moregen_clty true type_pairs env patt subj; [] with Failure r -> r end | error -> CM_Class_type_mismatch (patt, subj)::error in current_level := old_level; res let rec equal_clty trace type_pairs subst env cty1 cty2 = try match cty1, cty2 with Tcty_constr (_, _, cty1), Tcty_constr (_, _, cty2) -> equal_clty true type_pairs subst env cty1 cty2 | Tcty_constr (_, _, cty1), _ -> equal_clty true type_pairs subst env cty1 cty2 | _, Tcty_constr (_, _, cty2) -> equal_clty true type_pairs subst env cty1 cty2 | Tcty_fun (l1, ty1, cty1'), Tcty_fun (l2, ty2, cty2') when l1 = l2 -> begin try eqtype true type_pairs subst env ty1 ty2 with Unify trace -> raise (Failure [CM_Parameter_mismatch (expand_trace env trace)]) end; equal_clty false type_pairs subst env cty1' cty2' | Tcty_signature sign1, Tcty_signature sign2 -> let ty1 = object_fields (repr sign1.cty_self) in let ty2 = object_fields (repr sign2.cty_self) in let (fields1, rest1) = flatten_fields ty1 and (fields2, rest2) = flatten_fields ty2 in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in List.iter (fun (lab, k1, t1, k2, t2) -> begin try eqtype true type_pairs subst env t1 t2 with Unify trace -> raise (Failure [CM_Meth_type_mismatch (lab, expand_trace env trace)]) end) pairs; Vars.iter (fun lab (_, _, ty) -> let (_, _, ty') = Vars.find lab sign1.cty_vars in try eqtype true type_pairs subst env ty ty' with Unify trace -> raise (Failure [CM_Val_type_mismatch (lab, expand_trace env trace)])) sign2.cty_vars | _ -> raise (Failure (if trace then [] else [CM_Class_type_mismatch (cty1, cty2)])) with Failure error when trace -> raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error)) (* XXX On pourrait autoriser l'instantiation du type des parametres... *) (* XXX Correct ? (variables de type dans parametres et corps de classe *) let match_class_declarations env patt_params patt_type subj_params subj_type = let type_pairs = TypePairs.create 53 in let subst = ref [] in let sign1 = signature_of_class_type patt_type in let sign2 = signature_of_class_type subj_type in let t1 = repr sign1.cty_self in let t2 = repr sign2.cty_self in TypePairs.add type_pairs (t1, t2) (); let (fields1, rest1) = flatten_fields (object_fields t1) and (fields2, rest2) = flatten_fields (object_fields t2) in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in let error = List.fold_right (fun (lab, k, _) err -> let err = let k = field_kind_repr k in begin match k with Fvar r -> err | _ -> CM_Hide_public lab::err end in if Concr.mem lab sign1.cty_concr then err else CM_Hide_virtual ("method", lab) :: err) miss1 [] in let missing_method = List.map (fun (m, _, _) -> m) miss2 in let error = (List.map (fun m -> CM_Missing_method m) missing_method) @ error in (* Always succeeds *) eqtype true type_pairs subst env rest1 rest2; let error = List.fold_right (fun (lab, k1, t1, k2, t2) err -> let k1 = field_kind_repr k1 in let k2 = field_kind_repr k2 in match k1, k2 with (Fvar _, Fvar _) | (Fpresent, Fpresent) -> err | (Fvar _, Fpresent) -> CM_Private_method lab::err | (Fpresent, Fvar _) -> CM_Public_method lab::err | _ -> assert false) pairs error in let error = Vars.fold (fun lab (mut, vr, ty) err -> try let (mut', vr', ty') = Vars.find lab sign1.cty_vars in if mut = Mutable && mut' <> Mutable then CM_Non_mutable_value lab::err else if vr = Concrete && vr' <> Concrete then CM_Non_concrete_value lab::err else err with Not_found -> CM_Missing_value lab::err) sign2.cty_vars error in let error = Vars.fold (fun lab (_,vr,_) err -> if vr = Virtual && not (Vars.mem lab sign2.cty_vars) then CM_Hide_virtual ("instance variable", lab) :: err else err) sign1.cty_vars error in let error = List.fold_right (fun e l -> if List.mem e missing_method then l else CM_Virtual_method e::l) (Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr)) error in match error with [] -> begin try let lp = List.length patt_params in let ls = List.length subj_params in if lp <> ls then raise (Failure [CM_Parameter_arity_mismatch (lp, ls)]); List.iter2 (fun p s -> try eqtype true type_pairs subst env p s with Unify trace -> raise (Failure [CM_Type_parameter_mismatch (expand_trace env trace)])) patt_params subj_params; equal_clty false type_pairs subst env patt_type subj_type; [] with Failure r -> r end | error -> error (***************) (* Subtyping *) (***************) (**** Build a subtype of a given type. ****) (* build_subtype: [visited] traces traversed object and variant types [loops] is a mapping from variables to variables, to reproduce positive loops in a class type [posi] true if the current variance is positive [level] number of expansions/enlargement allowed on this branch *) let warn = ref false (* whether double coercion might do better *) let pred_expand n = if n mod 2 = 0 && n > 0 then pred n else n let pred_enlarge n = if n mod 2 = 1 then pred n else n type change = Unchanged | Equiv | Changed let collect l = List.fold_left (fun c1 (_, c2) -> max c1 c2) Unchanged l let rec filter_visited = function [] -> [] | {desc=Tobject _|Tvariant _} :: _ as l -> l | _ :: l -> filter_visited l let memq_warn t visited = if List.memq t visited then (warn := true; true) else false let rec lid_of_path sharp = function Path.Pident id -> Longident.Lident (sharp ^ Ident.name id) | Path.Pdot (p1, s, _) -> Longident.Ldot (lid_of_path "" p1, sharp ^ s) | Path.Papply (p1, p2) -> Longident.Lapply (lid_of_path sharp p1, lid_of_path "" p2) let find_cltype_for_path env p = let path, cl_abbr = Env.lookup_type (lid_of_path "#" p) env in match cl_abbr.type_manifest with Some ty -> begin match (repr ty).desc with Tobject(_,{contents=Some(p',_)}) when Path.same p p' -> cl_abbr, ty | _ -> raise Not_found end | None -> assert false let has_constr_row' env t = has_constr_row (expand_abbrev env t) let rec build_subtype env visited loops posi level t = let t = repr t in match t.desc with Tvar -> if posi then try let t' = List.assq t loops in warn := true; (t', Equiv) with Not_found -> (t, Unchanged) else (t, Unchanged) | Tarrow(l, t1, t2, _) -> if memq_warn t visited then (t, Unchanged) else let visited = t :: visited in let (t1', c1) = build_subtype env visited loops (not posi) level t1 in let (t2', c2) = build_subtype env visited loops posi level t2 in let c = max c1 c2 in if c > Unchanged then (newty (Tarrow(l, t1', t2', Cok)), c) else (t, Unchanged) | Ttuple tlist -> if memq_warn t visited then (t, Unchanged) else let visited = t :: visited in let tlist' = List.map (build_subtype env visited loops posi level) tlist in let c = collect tlist' in if c > Unchanged then (newty (Ttuple (List.map fst tlist')), c) else (t, Unchanged) | Tconstr(p, tl, abbrev) when level > 0 && generic_abbrev env p && safe_abbrev env t && not (has_constr_row' env t) -> let t' = repr (expand_abbrev env t) in let level' = pred_expand level in begin try match t'.desc with Tobject _ when posi && not (opened_object t') -> let cl_abbr, body = find_cltype_for_path env p in let ty = subst env !current_level Public abbrev None cl_abbr.type_params tl body in let ty = repr ty in let ty1, tl1 = match ty.desc with Tobject(ty1,{contents=Some(p',tl1)}) when Path.same p p' -> ty1, tl1 | _ -> raise Not_found in (* Fix PR4505: do not set ty to Tvar when it appears in tl1, as this occurence might break the occur check. XXX not clear whether this correct anyway... *) if List.exists (deep_occur ty) tl1 then raise Not_found; ty.desc <- Tvar; let t'' = newvar () in let loops = (ty, t'') :: loops in (* May discard [visited] as level is going down *) let (ty1', c) = build_subtype env [t'] loops posi (pred_enlarge level') ty1 in assert (t''.desc = Tvar); let nm = if c > Equiv || deep_occur ty ty1' then None else Some(p,tl1) in t''.desc <- Tobject (ty1', ref nm); (try unify_var env ty t with Unify _ -> assert false); (t'', Changed) | _ -> raise Not_found with Not_found -> let (t'',c) = build_subtype env visited loops posi level' t' in if c > Unchanged then (t'',c) else (t, Unchanged) end | Tconstr(p, tl, abbrev) -> (* Must check recursion on constructors, since we do not always expand them *) if memq_warn t visited then (t, Unchanged) else let visited = t :: visited in begin try let decl = Env.find_type p env in if level = 0 && generic_abbrev env p && safe_abbrev env t && not (has_constr_row' env t) then warn := true; let tl' = List.map2 (fun (co,cn,_) t -> if cn then if co then (t, Unchanged) else build_subtype env visited loops (not posi) level t else if co then build_subtype env visited loops posi level t else (newvar(), Changed)) decl.type_variance tl in let c = collect tl' in if c > Unchanged then (newconstr p (List.map fst tl'), c) else (t, Unchanged) with Not_found -> (t, Unchanged) end | Tvariant row -> let row = row_repr row in if memq_warn t visited || not (static_row row) then (t, Unchanged) else let level' = pred_enlarge level in let visited = t :: if level' < level then [] else filter_visited visited in let fields = filter_row_fields false row.row_fields in let fields = List.map (fun (l,f as orig) -> match row_field_repr f with Rpresent None -> if posi then (l, Reither(true, [], false, ref None)), Unchanged else orig, Unchanged | Rpresent(Some t) -> let (t', c) = build_subtype env visited loops posi level' t in let f = if posi && level > 0 then Reither(false, [t'], false, ref None) else Rpresent(Some t') in (l, f), c | _ -> assert false) fields in let c = collect fields in let row = { row_fields = List.map fst fields; row_more = newvar(); row_bound = (); row_closed = posi; row_fixed = false; row_name = if c > Unchanged then None else row.row_name } in (newty (Tvariant row), Changed) | Tobject (t1, _) -> if memq_warn t visited || opened_object t1 then (t, Unchanged) else let level' = pred_enlarge level in let visited = t :: if level' < level then [] else filter_visited visited in let (t1', c) = build_subtype env visited loops posi level' t1 in if c > Unchanged then (newty (Tobject (t1', ref None)), c) else (t, Unchanged) | Tfield(s, _, t1, t2) (* Always present *) -> let (t1', c1) = build_subtype env visited loops posi level t1 in let (t2', c2) = build_subtype env visited loops posi level t2 in let c = max c1 c2 in if c > Unchanged then (newty (Tfield(s, Fpresent, t1', t2')), c) else (t, Unchanged) | Tnil -> if posi then let v = newvar () in (v, Changed) else begin warn := true; (t, Unchanged) end | Tsubst _ | Tlink _ -> assert false | Tpoly(t1, tl) -> let (t1', c) = build_subtype env visited loops posi level t1 in if c > Unchanged then (newty (Tpoly(t1', tl)), c) else (t, Unchanged) | Tunivar -> (t, Unchanged) let enlarge_type env ty = warn := false; (* [level = 4] allows 2 expansions involving objects/variants *) let (ty', _) = build_subtype env [] [] true 4 ty in (ty', !warn) (**** Check whether a type is a subtype of another type. ****) (* During the traversal, a trace of visited types is maintained. It is printed in case of error. Constraints (pairs of types that must be equals) are accumulated rather than being enforced straight. Indeed, the result would otherwise depend on the order in which these constraints are enforced. A function enforcing these constraints is returned. That way, type variables can be bound to their actual values before this function is called (see Typecore). Only well-defined abbreviations are expanded (hence the tests [generic_abbrev ...]). *) let subtypes = TypePairs.create 17 let subtype_error env trace = raise (Subtype (expand_trace env (List.rev trace), [])) let private_abbrev env path = try let decl = Env.find_type path env in decl.type_private = Private && decl.type_manifest <> None with Not_found -> false let rec subtype_rec env trace t1 t2 cstrs = let t1 = repr t1 in let t2 = repr t2 in if t1 == t2 then cstrs else begin try TypePairs.find subtypes (t1, t2); cstrs with Not_found -> TypePairs.add subtypes (t1, t2) (); match (t1.desc, t2.desc) with (Tvar, _) | (_, Tvar) -> (trace, t1, t2, !univar_pairs)::cstrs | (Tarrow(l1, t1, u1, _), Tarrow(l2, t2, u2, _)) when l1 = l2 || !Clflags.classic && not (is_optional l1 || is_optional l2) -> let cstrs = subtype_rec env ((t2, t1)::trace) t2 t1 cstrs in subtype_rec env ((u1, u2)::trace) u1 u2 cstrs | (Ttuple tl1, Ttuple tl2) -> subtype_list env trace tl1 tl2 cstrs | (Tconstr(p1, [], _), Tconstr(p2, [], _)) when Path.same p1 p2 -> cstrs | (Tconstr(p1, tl1, abbrev1), _) when generic_abbrev env p1 && safe_abbrev env t1 -> subtype_rec env trace (expand_abbrev env t1) t2 cstrs | (_, Tconstr(p2, tl2, abbrev2)) when generic_abbrev env p2 && safe_abbrev env t2 -> subtype_rec env trace t1 (expand_abbrev env t2) cstrs | (Tconstr(p1, tl1, _), Tconstr(p2, tl2, _)) when Path.same p1 p2 -> begin try let decl = Env.find_type p1 env in List.fold_left2 (fun cstrs (co, cn, _) (t1, t2) -> if co then if cn then (trace, newty2 t1.level (Ttuple[t1]), newty2 t2.level (Ttuple[t2]), !univar_pairs) :: cstrs else subtype_rec env ((t1, t2)::trace) t1 t2 cstrs else if cn then subtype_rec env ((t2, t1)::trace) t2 t1 cstrs else cstrs) cstrs decl.type_variance (List.combine tl1 tl2) with Not_found -> (trace, t1, t2, !univar_pairs)::cstrs end | (Tconstr(p1, tl1, _), _) when private_abbrev env p1 -> subtype_rec env trace (expand_abbrev_opt env t1) t2 cstrs | (Tobject (f1, _), Tobject (f2, _)) when (object_row f1).desc = Tvar && (object_row f2).desc = Tvar -> (* Same row variable implies same object. *) (trace, t1, t2, !univar_pairs)::cstrs | (Tobject (f1, _), Tobject (f2, _)) -> subtype_fields env trace f1 f2 cstrs | (Tvariant row1, Tvariant row2) -> begin try subtype_row env trace row1 row2 cstrs with Exit -> (trace, t1, t2, !univar_pairs)::cstrs end | (Tpoly (u1, []), Tpoly (u2, [])) -> subtype_rec env trace u1 u2 cstrs | (Tpoly (u1, tl1), Tpoly (u2, [])) -> let _, u1' = instance_poly false tl1 u1 in subtype_rec env trace u1' u2 cstrs | (Tpoly (u1, tl1), Tpoly (u2,tl2)) -> begin try enter_poly env univar_pairs u1 tl1 u2 tl2 (fun t1 t2 -> subtype_rec env trace t1 t2 cstrs) with Unify _ -> (trace, t1, t2, !univar_pairs)::cstrs end | (_, _) -> (trace, t1, t2, !univar_pairs)::cstrs end and subtype_list env trace tl1 tl2 cstrs = if List.length tl1 <> List.length tl2 then subtype_error env trace; List.fold_left2 (fun cstrs t1 t2 -> subtype_rec env ((t1, t2)::trace) t1 t2 cstrs) cstrs tl1 tl2 and subtype_fields env trace ty1 ty2 cstrs = (* Assume that either rest1 or rest2 is not Tvar *) let (fields1, rest1) = flatten_fields ty1 in let (fields2, rest2) = flatten_fields ty2 in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in let cstrs = if rest2.desc = Tnil then cstrs else if miss1 = [] then subtype_rec env ((rest1, rest2)::trace) rest1 rest2 cstrs else (trace, build_fields (repr ty1).level miss1 rest1, rest2, !univar_pairs) :: cstrs in let cstrs = if miss2 = [] then cstrs else (trace, rest1, build_fields (repr ty2).level miss2 (newvar ()), !univar_pairs) :: cstrs in List.fold_left (fun cstrs (_, k1, t1, k2, t2) -> (* Theses fields are always present *) subtype_rec env ((t1, t2)::trace) t1 t2 cstrs) cstrs pairs and subtype_row env trace row1 row2 cstrs = let row1 = row_repr row1 and row2 = row_repr row2 in let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in let more1 = repr row1.row_more and more2 = repr row2.row_more in match more1.desc, more2.desc with Tconstr(p1,_,_), Tconstr(p2,_,_) when Path.same p1 p2 -> subtype_rec env ((more1,more2)::trace) more1 more2 cstrs | (Tvar|Tconstr _), (Tvar|Tconstr _) when row1.row_closed && r1 = [] -> List.fold_left (fun cstrs (_,f1,f2) -> match row_field_repr f1, row_field_repr f2 with (Rpresent None|Reither(true,_,_,_)), Rpresent None -> cstrs | Rpresent(Some t1), Rpresent(Some t2) -> subtype_rec env ((t1, t2)::trace) t1 t2 cstrs | Reither(false, t1::_, _, _), Rpresent(Some t2) -> subtype_rec env ((t1, t2)::trace) t1 t2 cstrs | Rabsent, _ -> cstrs | _ -> raise Exit) cstrs pairs | Tunivar, Tunivar when row1.row_closed = row2.row_closed && r1 = [] && r2 = [] -> let cstrs = subtype_rec env ((more1,more2)::trace) more1 more2 cstrs in List.fold_left (fun cstrs (_,f1,f2) -> match row_field_repr f1, row_field_repr f2 with Rpresent None, Rpresent None | Reither(true,[],_,_), Reither(true,[],_,_) | Rabsent, Rabsent -> cstrs | Rpresent(Some t1), Rpresent(Some t2) | Reither(false,[t1],_,_), Reither(false,[t2],_,_) -> subtype_rec env ((t1, t2)::trace) t1 t2 cstrs | _ -> raise Exit) cstrs pairs | _ -> raise Exit let subtype env ty1 ty2 = TypePairs.clear subtypes; univar_pairs := []; (* Build constraint set. *) let cstrs = subtype_rec env [(ty1, ty2)] ty1 ty2 [] in TypePairs.clear subtypes; (* Enforce constraints. *) function () -> List.iter (function (trace0, t1, t2, pairs) -> try unify_pairs env t1 t2 pairs with Unify trace -> raise (Subtype (expand_trace env (List.rev trace0), List.tl (List.tl trace)))) (List.rev cstrs) (*******************) (* Miscellaneous *) (*******************) (* Utility for printing. The resulting type is not used in computation. *) let rec unalias_object ty = let ty = repr ty in match ty.desc with Tfield (s, k, t1, t2) -> newty2 ty.level (Tfield (s, k, t1, unalias_object t2)) | Tvar | Tnil -> newty2 ty.level ty.desc | Tunivar -> ty | Tconstr _ -> newty2 ty.level Tvar | _ -> assert false let unalias ty = let ty = repr ty in match ty.desc with Tvar | Tunivar -> ty | Tvariant row -> let row = row_repr row in let more = row.row_more in newty2 ty.level (Tvariant {row with row_more = newty2 more.level more.desc}) | Tobject (ty, nm) -> newty2 ty.level (Tobject (unalias_object ty, nm)) | _ -> newty2 ty.level ty.desc let unroll_abbrev id tl ty = let ty = repr ty in if (ty.desc = Tvar) || (List.exists (deep_occur ty) tl) then ty else let ty' = newty2 ty.level ty.desc in link_type ty (newty2 ty.level (Tconstr (Path.Pident id, tl, ref Mnil))); ty' (* Return the arity (as for curried functions) of the given type. *) let rec arity ty = match (repr ty).desc with Tarrow(_, t1, t2, _) -> 1 + arity t2 | _ -> 0 (* Check whether an abbreviation expands to itself. *) let cyclic_abbrev env id ty = let rec check_cycle seen ty = let ty = repr ty in match ty.desc with Tconstr (p, tl, abbrev) -> p = Path.Pident id || List.memq ty seen || begin try check_cycle (ty :: seen) (expand_abbrev env ty) with Cannot_expand -> false | Unify _ -> true end | _ -> false in check_cycle [] ty (* Normalize a type before printing, saving... *) (* Cannot use mark_type because deep_occur uses it too *) let rec normalize_type_rec env visited ty = let ty = repr ty in if not (TypeSet.mem ty !visited) then begin visited := TypeSet.add ty !visited; begin match ty.desc with | Tvariant row -> let row = row_repr row in let fields = List.map (fun (l,f0) -> let f = row_field_repr f0 in l, match f with Reither(b, ty::(_::_ as tyl), m, e) -> let tyl' = List.fold_left (fun tyl ty -> if List.exists (fun ty' -> equal env false [ty] [ty']) tyl then tyl else ty::tyl) [ty] tyl in if f != f0 || List.length tyl' < List.length tyl then Reither(b, List.rev tyl', m, e) else f | _ -> f) row.row_fields in let fields = List.sort (fun (p,_) (q,_) -> compare p q) (List.filter (fun (_,fi) -> fi <> Rabsent) fields) in log_type ty; ty.desc <- Tvariant {row with row_fields = fields} | Tobject (fi, nm) -> begin match !nm with | None -> () | Some (n, v :: l) -> if deep_occur ty (newgenty (Ttuple l)) then (* The abbreviation may be hiding something, so remove it *) set_name nm None else let v' = repr v in begin match v'.desc with | Tvar|Tunivar -> if v' != v then set_name nm (Some (n, v' :: l)) | Tnil -> log_type ty; ty.desc <- Tconstr (n, l, ref Mnil) | _ -> set_name nm None end | _ -> fatal_error "Ctype.normalize_type_rec" end; let fi = repr fi in if fi.level < lowest_level then () else let fields, row = flatten_fields fi in let fi' = build_fields fi.level fields row in log_type ty; fi.desc <- fi'.desc | _ -> () end; iter_type_expr (normalize_type_rec env visited) ty end let normalize_type env ty = normalize_type_rec env (ref TypeSet.empty) ty (*************************) (* Remove dependencies *) (*************************) (* Variables are left unchanged. Other type nodes are duplicated, with levels set to generic level. During copying, the description of a (non-variable) node is first replaced by a link to a stub ([Tsubst (newgenvar ())]). Once the copy is made, it replaces the stub. After copying, the description of node, which was stored by [save_desc], must be put back, using [cleanup_types]. *) let rec nondep_type_rec env id ty = let ty = repr ty in match ty.desc with Tvar | Tunivar -> ty | Tsubst ty -> ty | _ -> let desc = ty.desc in save_desc ty desc; let ty' = newgenvar () in (* Stub *) ty.desc <- Tsubst ty'; ty'.desc <- begin match desc with | Tconstr(p, tl, abbrev) -> if Path.isfree id p then begin try Tlink (nondep_type_rec env id (expand_abbrev env (newty2 ty.level desc))) (* The [Tlink] is important. The expanded type may be a variable, or may not be completely copied yet (recursive type), so one cannot just take its description. *) with Cannot_expand | Unify _ -> (* expand_abbrev failed *) raise Not_found (* cf. PR4775 for Unify *) end else Tconstr(p, List.map (nondep_type_rec env id) tl, ref Mnil) | Tobject (t1, name) -> Tobject (nondep_type_rec env id t1, ref (match !name with None -> None | Some (p, tl) -> if Path.isfree id p then None else Some (p, List.map (nondep_type_rec env id) tl))) | Tvariant row -> let row = row_repr row in let more = repr row.row_more in (* We must substitute in a subtle way *) (* Tsubst denotes the variant itself, as the row var is unchanged *) begin match more.desc with Tsubst ty2 -> (* This variant type has been already copied *) ty.desc <- Tsubst ty2; (* avoid Tlink in the new type *) Tlink ty2 | _ -> let static = static_row row in (* Register new type first for recursion *) save_desc more more.desc; more.desc <- ty.desc; let more' = if static then newgenvar () else more in (* Return a new copy *) let row = copy_row (nondep_type_rec env id) true row true more' in match row.row_name with Some (p, tl) when Path.isfree id p -> Tvariant {row with row_name = None} | _ -> Tvariant row end | _ -> copy_type_desc (nondep_type_rec env id) desc end; ty' let nondep_type env id ty = try let ty' = nondep_type_rec env id ty in cleanup_types (); unmark_type ty'; ty' with Not_found -> cleanup_types (); raise Not_found (* Preserve sharing inside type declarations. *) let nondep_type_decl env mid id is_covariant decl = try let params = List.map (nondep_type_rec env mid) decl.type_params in let tk = try match decl.type_kind with Type_abstract -> Type_abstract | Type_variant cstrs -> Type_variant (List.map (fun (c, tl) -> (c, List.map (nondep_type_rec env mid) tl)) cstrs) | Type_record(lbls, rep) -> Type_record (List.map (fun (c, mut, t) -> (c, mut, nondep_type_rec env mid t)) lbls, rep) with Not_found when is_covariant -> Type_abstract and tm = try match decl.type_manifest with None -> None | Some ty -> Some (unroll_abbrev id params (nondep_type_rec env mid ty)) with Not_found when is_covariant -> None in cleanup_types (); List.iter unmark_type decl.type_params; begin match decl.type_kind with Type_abstract -> () | Type_variant cstrs -> List.iter (fun (c, tl) -> List.iter unmark_type tl) cstrs | Type_record(lbls, rep) -> List.iter (fun (c, mut, t) -> unmark_type t) lbls end; begin match decl.type_manifest with None -> () | Some ty -> unmark_type ty end; let priv = match tm with | Some ty when Btype.has_constr_row ty -> Private | _ -> decl.type_private in { type_params = params; type_arity = decl.type_arity; type_kind = tk; type_manifest = tm; type_private = priv; type_variance = decl.type_variance; } with Not_found -> cleanup_types (); raise Not_found (* Preserve sharing inside class types. *) let nondep_class_signature env id sign = { cty_self = nondep_type_rec env id sign.cty_self; cty_vars = Vars.map (function (m, v, t) -> (m, v, nondep_type_rec env id t)) sign.cty_vars; cty_concr = sign.cty_concr; cty_inher = List.map (fun (p,tl) -> (p, List.map (nondep_type_rec env id) tl)) sign.cty_inher } let rec nondep_class_type env id = function Tcty_constr (p, _, cty) when Path.isfree id p -> nondep_class_type env id cty | Tcty_constr (p, tyl, cty) -> Tcty_constr (p, List.map (nondep_type_rec env id) tyl, nondep_class_type env id cty) | Tcty_signature sign -> Tcty_signature (nondep_class_signature env id sign) | Tcty_fun (l, ty, cty) -> Tcty_fun (l, nondep_type_rec env id ty, nondep_class_type env id cty) let nondep_class_declaration env id decl = assert (not (Path.isfree id decl.cty_path)); let decl = { cty_params = List.map (nondep_type_rec env id) decl.cty_params; cty_variance = decl.cty_variance; cty_type = nondep_class_type env id decl.cty_type; cty_path = decl.cty_path; cty_new = begin match decl.cty_new with None -> None | Some ty -> Some (nondep_type_rec env id ty) end } in cleanup_types (); List.iter unmark_type decl.cty_params; unmark_class_type decl.cty_type; begin match decl.cty_new with None -> () | Some ty -> unmark_type ty end; decl let nondep_cltype_declaration env id decl = assert (not (Path.isfree id decl.clty_path)); let decl = { clty_params = List.map (nondep_type_rec env id) decl.clty_params; clty_variance = decl.clty_variance; clty_type = nondep_class_type env id decl.clty_type; clty_path = decl.clty_path } in cleanup_types (); List.iter unmark_type decl.clty_params; unmark_class_type decl.clty_type; decl (* collapse conjonctive types in class parameters *) let rec collapse_conj env visited ty = let ty = repr ty in if List.memq ty visited then () else let visited = ty :: visited in match ty.desc with Tvariant row -> let row = row_repr row in List.iter (fun (l,fi) -> match row_field_repr fi with Reither (c, t1::(_::_ as tl), m, e) -> List.iter (unify env t1) tl; set_row_field e (Reither (c, [t1], m, ref None)) | _ -> ()) row.row_fields; iter_row (collapse_conj env visited) row | _ -> iter_type_expr (collapse_conj env visited) ty let collapse_conj_params env params = List.iter (collapse_conj env []) params