(***********************************************************************) (* *) (* Objective Caml *) (* *) (* Xavier Leroy and Jerome Vouillon, projet Cristal, INRIA Rocquencourt*) (* *) (* Copyright 1996 Institut National de Recherche en Informatique et *) (* Automatique. Distributed only by permission. *) (* *) (***********************************************************************) (* $Id$ *) (* Operations on core types *) open Misc open Asttypes open Types exception Unify of (type_expr * type_expr) list exception Subtype of (type_expr * type_expr) list * (type_expr * type_expr) list let current_level = ref 0 let global_level = ref 1 let generic_level = (-1) let init_def level = current_level := level let begin_def () = incr current_level let end_def () = decr current_level let reset_global_level () = global_level := !current_level + 1 let newty desc = { desc = desc; level = !current_level } let new_global_ty desc = { desc = desc; level = !global_level } let newgenty desc = { desc = desc; level = generic_level } let newvar () = { desc = Tvar; level = !current_level } let new_global_var () = new_global_ty Tvar let new_gen_var () = newgenty Tvar let newobj fields = newty (Tobject (fields, ref None)) let rec repr = function {desc = Tlink t'} as t -> let r = repr t' in if r != t' then t.desc <- Tlink r; r | t -> t let rec repr2 = function (* No path compression *) (* during unification *) {desc = Tlink ty} -> repr2 ty | t -> t let none = newty (Ttuple []) (* Clearly ill-formed type *) (* --- *) let flatten_fields ty = let rec flatten l ty = let ty = repr ty in match ty.desc with Tfield(s, ty1, ty2) -> flatten ((s, ty1)::l) ty2 | Tvar | Tnil -> (l, ty) | _ -> fatal_error "Ctype.flatten_fields" in let (l, r) = flatten [] ty in (List.rev l, r) let build_fields = List.fold_right (fun (s, ty1) ty2 -> {desc = Tfield(s, ty1, ty2); level = ty2.level}) 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, t)::r as l), ((n', t')::r' as l')) -> if n = n' then associate ((t, t')::p) s s' (r, r') else if n < n' then associate p ((n, t)::s) s' (r, l') else associate p s ((n', t')::s') (l, r') in let sort = Sort.list (fun (n, _) (n', _) -> n < n') in associate [] [] [] (sort fields1, sort fields2) (* Check whether an object is open *) let rec opened ty = match (repr ty).desc with Tfield(_, _, t) -> opened t | Tvar -> true | Tnil -> false | _ -> fatal_error "Ctype.opened" let opened_object ty = match (repr ty).desc with Tobject (ty', _) -> opened ty' | Tconstr (_, _, _) -> false | _ -> fatal_error "Ctype.opened_object" (* Type generalization *) let rec generalize ty = let ty = repr ty in if ty.level > !current_level then begin ty.level <- generic_level; match ty.desc with Tvar -> () | Tarrow(t1, t2) -> generalize t1; generalize t2 | Ttuple tl -> List.iter generalize tl | Tconstr(_, tl, ab) -> ab := []; List.iter generalize tl | Tobject(f, {contents = Some (_, p)}) -> generalize f; List.iter generalize p | Tobject(f, _) -> generalize f | Tfield(_, t1, t2) -> generalize t1; generalize t2 | Tnil -> () | Tlink _ -> fatal_error "Ctype.generalize" end let rec make_nongen ty = let ty = repr ty in if ty.level > !current_level then begin ty.level <- !current_level; match ty.desc with Tvar -> () | Tarrow(t1, t2) -> make_nongen t1; make_nongen t2 | Ttuple tl -> List.iter make_nongen tl | Tconstr(p, tl, _) -> List.iter make_nongen tl | Tobject(f, {contents = Some (_, p)}) -> make_nongen f; List.iter make_nongen p | Tobject(f, _) -> make_nongen f | Tfield(_, t1, t2) -> make_nongen t1; make_nongen t2 | Tnil -> () | Tlink _ -> fatal_error "Ctype.make_nongen" end (* Remove abbreviations from generalized types *) let visited = ref ([] : type_expr list) let remove_abbrev ty = let rec remove ty = let ty = repr ty in if ty.level = generic_level & not (List.memq ty !visited) then begin visited := ty :: !visited; match ty.desc with Tvar -> () | Tarrow(t1, t2) -> remove t1; remove t2 | Ttuple tl -> List.iter remove tl | Tconstr(_, tl, ab) -> ab := []; List.iter remove tl | Tobject(f, {contents = Some (_, p)}) -> remove f; List.iter remove p | Tobject(f, _) -> remove f | Tfield(_, t1, t2) -> remove t1; remove t2 | Tnil -> () | Tlink _ -> fatal_error "Ctype.remove_abbrev" end in visited := []; remove ty; visited := [] (* Taking instances of type schemes *) type 'a visited = Zero | One | Many of 'a let inst_subst = ref ([] : (type_expr * type_expr) list) let rec copy_rec abbrev visited ty = let ty = repr ty in if ty.level <> generic_level then ty else try match List.assq ty visited with {contents = Zero} as v -> let t = newvar () in v := Many t; let ty' = copy_rec_2 abbrev visited ty v in t.desc <- ty'.desc; t | {contents = One} as v -> let t = newvar () in v := Many t; t | {contents = Many t} -> t with Not_found -> let v = ref One in let ty' = copy_rec_2 abbrev ((ty, v)::visited) ty v in match v with {contents = Many t} -> t.desc <- ty'.desc; t | _ -> ty' and copy_rec_2 abbrev visited ty v = match ty.desc with Tvar -> begin try List.assq ty !inst_subst with Not_found -> let ty' = newvar () in inst_subst := (ty, ty') :: !inst_subst; ty' end | Tarrow (t1, t2) -> newty (Tarrow (copy_rec abbrev visited t1, copy_rec abbrev visited t2)) | Ttuple tl -> newty (Ttuple (List.map (copy_rec abbrev visited) tl)) | Tconstr (p, [], _) -> newty (Tconstr (p, [], ref abbrev)) | Tconstr (p, tl, _) -> newty (Tconstr (p, List.map (copy_rec abbrev visited) tl, ref abbrev)) | Tobject (t1, {contents = name}) -> let ty' () = let name' = match name with None -> None | Some (p, tl) -> Some (p, List.map (copy_rec abbrev visited) tl) in newty (Tobject (copy_rec abbrev visited t1, ref name')) in if opened_object ty then try List.assq ty !inst_subst with Not_found -> if v = ref One then begin let t = newvar () in v := Many t; inst_subst := (ty, t):: !inst_subst end; ty' () else ty' () | Tfield (label, t1, t2) -> newty (Tfield (label, copy_rec abbrev visited t1, copy_rec abbrev visited t2)) | Tnil -> newty Tnil | Tlink _ -> fatal_error "Ctype.copy_rec" let copy ty = copy_rec [] [] ty let subst abbrev ty = copy_rec abbrev [] ty let copy_parameterized params ty = copy_rec [] params ty let instance sch = inst_subst := []; let ty = copy sch in inst_subst := []; ty let instance_constructor cstr = inst_subst := []; let ty_res = copy cstr.cstr_res in let ty_args = List.map copy cstr.cstr_args in inst_subst := []; (ty_args, ty_res) let instance_label lbl = inst_subst := []; let ty_res = copy lbl.lbl_res in let ty_arg = copy lbl.lbl_arg in inst_subst := []; (ty_arg, ty_res) let substitute abbrev params args body = inst_subst := List.combine params args; let ty = subst abbrev body in inst_subst := []; ty let instance_parameterized_type sch_args sch = inst_subst := []; let params = List.map (function p -> (repr p, ref Zero)) sch_args in let ty_args = List.map (copy_parameterized params) sch_args in let ty = copy_parameterized params sch in inst_subst := []; (ty_args, ty) let instance_parameterized_type_2 sch_args sch_lst sch = inst_subst := []; let params = List.map (function p -> (repr p, ref Zero)) sch_args in let ty_args = List.map (copy_parameterized params) sch_args in let ty_lst = List.map (copy_parameterized params) sch_lst in let ty = copy_parameterized params sch in inst_subst := []; (ty_args, ty_lst, ty) let instance_class cl = inst_subst := []; let params0 = List.map (function p -> (repr p, ref Zero)) cl.cty_params in let params = List.map (copy_parameterized params0) cl.cty_params in let args = List.map (copy_parameterized params0) cl.cty_args in let vars = Vars.fold (fun lab (mut, ty) -> Vars.add lab (mut, copy_parameterized params0 ty)) cl.cty_vars Vars.empty in let self = copy_parameterized params0 cl.cty_self in inst_subst := []; (params, args, vars, self) (* Unification *) let rec update_level level ty = let ty = repr2 ty in if ty.level > level then begin ty.level <- level; match ty.desc with Tvar -> () | Tarrow(t1,t2) -> update_level level t1; update_level level t2 | Ttuple(ty_list) -> List.iter (update_level level) ty_list | Tconstr(_, tl, _) -> List.iter (update_level level) tl | Tobject(f, {contents = Some (_, p)}) -> update_level level f; List.iter (update_level level) p | Tobject (f, _) -> update_level level f | Tfield(_, t1, t2) -> update_level level t1; update_level level t2 | Tnil -> () | Tlink _ -> fatal_error "Ctype.update_level" end exception Cannot_expand let rec find_expans p1 = function [] -> None | (p2, ty)::l -> if Path.same p1 p2 then Some ty else find_expans p1 l let expand_abbrev env path args abbrev level = match find_expans path !abbrev with Some ty -> update_level level ty; ty | None -> let decl = try Env.find_type path env with Not_found -> raise Cannot_expand in match decl.type_manifest with Some body -> let v = newvar () in abbrev := (path, v)::!abbrev; let old_level = !current_level in current_level := level; let ty = substitute !abbrev decl.type_params args body in current_level := old_level; v.desc <- Tlink ty; ty | _ -> raise Cannot_expand let rec expand_root env ty = let ty = repr ty in match ty.desc with Tconstr(p, tl, abbrev) -> begin try expand_root env (expand_abbrev env p tl (ref !abbrev) ty.level) with Cannot_expand -> ty end | _ -> ty let rec full_expand env ty = let ty = repr (expand_root env ty) in match ty.desc with Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar -> { desc = Tobject (fi, ref None); level = ty.level } | _ -> ty let generic_abbrev env path = try let decl = Env.find_type path env in match decl.type_manifest with Some body -> body.level = generic_level | _ -> false with Not_found -> false let check_level env level ty = let visited = ref [] in let rec check ty = let ty = repr ty in match ty.desc with Tvar -> () | Tarrow(t1, t2) -> check t1; check t2 | Ttuple tl -> List.iter check tl | Tconstr(p, [], abbrev) -> if level < Path.binding_time p then begin if not (List.memq ty !visited) then begin visited := ty::!visited; let ty' = try expand_abbrev env p [] abbrev ty.level with Cannot_expand -> raise (Unify []) in check ty' end; end | Tconstr(p, tl, abbrev) -> if not (List.memq ty !visited) then begin visited := ty::!visited; if level < Path.binding_time p then begin let ty' = try expand_abbrev env p tl abbrev ty.level with Cannot_expand -> raise (Unify []) in check ty' end; List.iter check tl end | Tobject(f, _) -> if not (List.memq ty !visited) then begin visited := ty::!visited; check f end | Tfield(_, t1, t2) -> check t1; check t2 | Tnil -> () | Tlink _ -> fatal_error "Ctype.check_level" in check ty let occur env ty0 ty = let visited = ref ([] : type_expr list) in let rec occur_rec ty = let ty = repr ty in if ty == ty0 then raise (Unify []); match ty.desc with Tvar -> () | Tarrow(t1, t2) -> occur_rec t1; occur_rec t2 | Ttuple tl -> List.iter occur_rec tl | Tconstr(p, [], abbrev) -> () | Tconstr(p, tl, abbrev) -> if not (List.memq ty !visited) then begin visited := ty :: !visited; try List.iter occur_rec tl with Unify _ -> try let ty' = expand_abbrev env p tl abbrev ty.level in occur_rec ty' with Cannot_expand -> () end | Tobject (_, _) -> () | _ (* Tfield (_, _, _) | Tnil | Tlink _ *) -> fatal_error "Ctype.occur" in occur_rec ty let rec unify_rec env a1 a2 t1 t2 = (* Variables and abbreviations *) if t1 == t2 then () else let t1 = repr2 t1 in let t2 = repr2 t2 in if t1 == t2 then () else try match (t1.desc, t2.desc) with (Tvar, _) -> update_level t1.level t2; begin match a2 with None -> occur env t1 t2; check_level env t1.level t2; t1.desc <- Tlink t2 | Some l2 -> occur env t1 l2; check_level env t1.level l2; t1.desc <- Tlink l2 end | (_, Tvar) -> update_level t2.level t1; begin match a1 with None -> occur env t2 t1; check_level env t2.level t1; t2.desc <- Tlink t1 | Some l1 -> occur env t2 l1; check_level env t2.level l1; t2.desc <- Tlink l1 end | (Tconstr (p1, tl1, abbrev1), Tconstr (p2, tl2, abbrev2)) when Path.same p1 p2 -> begin try unify_core env a1 a2 t1 t2 with Unify lst -> try let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in update_level t2.level t1; unify_rec env (Some t1) a2 t3 t2 with Cannot_expand -> try let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in update_level t1.level t2; unify_rec env a1 (Some t2) t1 t3 with Cannot_expand -> raise (Unify lst) end | (Tconstr (p1, tl1, abbrev1), Tconstr (p2, tl2, abbrev2)) -> begin try let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in update_level t2.level t1; unify_rec env (Some t1) a2 t3 t2 with Cannot_expand -> try let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in update_level t1.level t2; unify_rec env a1 (Some t2) t1 t3 with Cannot_expand -> raise (Unify []) end | (Tconstr (p1, tl1, abbrev1), _) -> begin try let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in update_level t2.level t1; unify_rec env (Some t1) a2 t3 t2 with Cannot_expand -> unify_core env a1 a2 t1 t2 end | (_, Tconstr (p2, tl2, abbrev2)) -> begin try let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in update_level t1.level t2; unify_rec env a1 (Some t2) t1 t3 with Cannot_expand -> unify_core env a1 a2 t1 t2 end | (_, _) -> unify_core env a1 a2 t1 t2 with Unify [] -> raise (Unify [(t1, t2)]) | Unify (_::l) -> raise (Unify ((t1, t2)::l)) and unify_core env a1 a2 t1 t2 = (* Other cases *) let d1 = t1.desc and d2 = t2.desc in begin match (a1, a2) with (None, Some l2) -> update_level t1.level t2; t1.desc <- Tlink l2 | (Some l1, None) -> update_level t2.level t1; t2.desc <- Tlink l1 | (_, _) -> update_level t1.level t2; occur env t1 t2; t1.desc <- Tlink t2 end; try match (d1, d2) with (Tarrow (t1, u1), Tarrow (t2, u2)) -> unify_rec env None None t1 t2; unify_rec env None None u1 u2 | (Ttuple tl1, Ttuple tl2) -> unify_list env tl1 tl2 | (Tconstr (p1, [], _), Tconstr (p2, [], _)) (*when Path.same p1 p2*) -> () | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) (*when Path.same p1 p2*) -> unify_list env tl1 tl2 | (Tobject (fi1, nm1), Tobject (fi2, nm2)) -> unify_fields env fi1 fi2; begin match !nm2 with Some (_, va::_) when (repr va).desc = Tvar -> () | _ -> nm2 := !nm1 end | (_, _) -> raise (Unify []) with Unify l -> t1.desc <- d1; t2.desc <- d2; raise (Unify ((t1, t2)::l)) | exn -> t1.desc <- d1; t2.desc <- d2; raise exn and unify_list env tl1 tl2 = if List.length tl1 <> List.length tl2 then raise (Unify []); List.iter2 (unify_rec env None None) tl1 tl2 and unify_fields 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 let va = newvar () in begin match rest1.desc with Tvar -> let nr = build_fields miss2 va in update_level rest1.level nr; rest1.desc <- Tlink nr | Tnil -> if miss2 <> [] then raise (Unify []); va.desc <- Tlink {desc = Tnil; level = va.level} | _ -> fatal_error "Ctype.unify_fields (1)" end; begin match rest2.desc with Tvar -> let nr = build_fields miss1 va in update_level rest2.level nr; rest2.desc <- Tlink nr | Tnil -> if miss1 <> [] then raise (Unify []); va.desc <- Tlink {desc = Tnil; level = va.level} | _ -> fatal_error "Ctype.unify_fields (2)" end; List.iter (fun (t1, t2) -> unify_rec env None None t1 t2) pairs let expand_trace env trace = List.fold_right (fun (t1, t2) rem -> (t1, full_expand env t1)::(t2, full_expand env t2)::rem) trace [] let rec filter_trace = function (t1, t1')::(t2, t2')::rem -> let rem' = filter_trace rem in if (t1 == t1') & (t2 == t2') then rem' else (t1, t1')::(t2, t2')::rem | _ -> [] let unify env ty1 ty2 = try unify_rec env None None ty1 ty2 with Unify trace -> let trace = expand_trace env trace in match trace with t1::t2::rem -> raise (Unify (t1::t2::filter_trace rem)) | _ -> fatal_error "Ctype.unify" let rec filter_arrow env t = let t = repr t in match t.desc with Tvar -> let t1 = newvar () and t2 = newvar () in let t' = newty (Tarrow (t1, t2)) in update_level t.level t'; t.desc <- Tlink t'; (t1, t2) | Tarrow(t1, t2) -> (t1, t2) | Tconstr(p, tl, abbrev) -> begin try filter_arrow env (expand_abbrev env p tl abbrev t.level) with Cannot_expand -> raise (Unify []) end | _ -> raise (Unify []) let rec filter_method_field name ty = let ty = repr ty in match ty.desc with Tvar -> let ty1 = newvar () and ty2 = newvar () in let ty' = newty (Tfield (name, ty1, ty2)) in update_level ty.level ty'; ty.desc <- Tlink ty'; ty1 | Tfield(n, ty1, ty2) -> if n = name then ty1 else filter_method_field name ty2 | _ -> raise (Unify []) let rec filter_method env name ty = let ty = repr ty in match ty.desc with Tvar -> let ty1 = newvar ()in let ty' = newobj ty1 in update_level ty.level ty'; ty.desc <- Tlink ty'; filter_method_field name ty1 | Tobject(f, _) -> filter_method_field name f | Tconstr(p, tl, abbrev) -> begin try filter_method env name (expand_abbrev env p tl abbrev ty.level) with Cannot_expand -> raise (Unify []) end | _ -> raise (Unify []) (* Matching between type schemes *) let moregen_occur env ty0 ty = let visited = ref [] in let rec occur_rec ty = let ty = repr ty in match ty.desc with Tvar -> (* ty0 has level = !current_level iff it is generic in the original type scheme. In this case, it can be freely instantiated. Otherwise, ty0 is not generic and cannot be instantiated by a type that contains generic variables. *) if ty.level = generic_level & ty0.level < !current_level then raise (Unify []) | Tarrow(t1, t2) -> occur_rec t1; occur_rec t2 | Ttuple tl -> List.iter occur_rec tl | Tconstr(p, tl, abbrev) -> if not (List.memq ty !visited) then begin visited := ty::!visited; try List.iter occur_rec tl with Unify lst -> let ty' = try expand_abbrev env p tl abbrev ty.level with Cannot_expand -> raise (Unify lst) in occur_rec ty' end | Tobject(f, _) -> if not (List.memq ty !visited) then begin visited := ty::!visited; occur_rec f end | Tfield(_, t1, t2) -> occur_rec t1; occur_rec t2 | Tnil -> () | Tlink _ -> fatal_error "Ctype.moregen_occur" in occur_rec ty let rec moregen env t1 t2 = if t1 == t2 then () else let t1 = repr t1 in let t2 = repr t2 in if t1 == t2 then () else let d1 = t1.desc in try begin match (t1.desc, t2.desc) with (Tvar, _) -> if t1.level = generic_level then raise (Unify []); moregen_occur env t1 t2; t1.desc <- Tlink t2 | (Tarrow(t1, u1), Tarrow(t2, u2)) -> moregen env t1 t2; moregen env u1 u2 | (Ttuple tl1, Ttuple tl2) -> moregen_list env tl1 tl2 | (Tconstr(p1, tl1, abbrev1), Tconstr(p2, tl2, abbrev2)) -> if Path.same p1 p2 then begin try t1.desc <- Tlink t2; moregen_list env tl1 tl2; t1.desc <- d1 with Unify lst -> t1.desc <- d1; try moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2 with Cannot_expand -> try moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level) with Cannot_expand -> raise (Unify lst) end else begin try moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2 with Cannot_expand -> try moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level) with Cannot_expand -> raise (Unify []) end | (Tobject(f1, _), Tobject(f2, _)) -> t1.desc <- Tlink t2; moregen_fields env f1 f2 | (Tconstr(p1, tl1, abbrev1), _) -> begin try moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2 with Cannot_expand -> raise (Unify []) end | (_, Tconstr(p2, tl2, abbrev2)) -> begin try moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level) with Cannot_expand -> raise (Unify []) end | (_, _) -> raise (Unify []) end with exn -> t1.desc <- d1; raise exn and moregen_list env tl1 tl2 = if List.length tl1 <> List.length tl2 then raise (Unify []); List.iter2 (moregen env) tl1 tl2 and moregen_fields 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 []); begin match rest1.desc with Tvar -> if rest1.level = generic_level then raise (Unify []); let fi = build_fields miss2 rest2 in moregen_occur env rest1 fi | Tnil -> if miss2 <> [] then raise (Unify []); if rest2.desc <> Tnil then raise (Unify []) | _ -> fatal_error "moregen_fields" end; List.iter (fun (t1, t2) -> moregen env t1 t2) pairs let moregeneral env sch1 sch2 = begin_def(); try moregen env (instance sch1) sch2; remove_abbrev sch2; end_def(); true with Unify _ -> remove_abbrev sch2; end_def(); false (* Equivalence between parameterized types *) let equal env params1 ty1 params2 ty2 = let subst = ref (List.combine params1 params2) in let type_pairs = ref [] in let rec eqtype t1 t2 = let t1 = repr t1 in let t2 = repr t2 in match (t1.desc, t2.desc) with (Tvar, Tvar) -> begin try List.assq t1 !subst == t2 with Not_found -> subst := (t1, t2) :: !subst; true end | (Tarrow(t1, u1), Tarrow(t2, u2)) -> eqtype t1 t2 & eqtype u1 u2 | (Ttuple tl1, Ttuple tl2) -> eqtype_list tl1 tl2 | (Tconstr(p1, tl1, abbrev1), Tconstr(p2, tl2, abbrev2)) -> List.exists (function (t1', t2') -> t1 == t1' & t2 == t2') !type_pairs or begin type_pairs := (t1, t2) :: !type_pairs; if Path.same p1 p2 then eqtype_list tl1 tl2 else begin try eqtype (expand_abbrev env p1 tl1 abbrev1 t1.level) t2 with Cannot_expand -> try eqtype t1 (expand_abbrev env p2 tl2 abbrev2 t2.level) with Cannot_expand -> false end end | (Tobject (f1, _), Tobject (f2, _)) -> List.exists (function (t1', t2') -> t1 == t1' & t2 == t2') !type_pairs or begin type_pairs := (t1, t2) :: !type_pairs; eqtype_fields f1 f2 end | (Tconstr(p1, tl1, abbrev1), _) -> begin try eqtype (expand_abbrev env p1 tl1 abbrev1 t1.level) t2 with Cannot_expand -> false end | (_, Tconstr(p2, tl2, abbrev2)) -> begin try eqtype t1 (expand_abbrev env p2 tl2 abbrev2 t2.level) with Cannot_expand -> false end | (Tnil, Tnil) -> true | (_, _) -> false and eqtype_list tl1 tl2 = match (tl1, tl2) with ([], []) -> true | (t1::r1, t2::r2) -> eqtype t1 t2 & eqtype_list r1 r2 | (_, _) -> false and eqtype_fields ty1 ty2 = let (fields1, rest1) = flatten_fields ty1 and (fields2, rest2) = flatten_fields ty2 in List.length fields1 = List.length fields2 & eqtype rest1 rest2 & List.for_all (function (label, t) -> List.exists (function (label', t') -> (label = label') & (eqtype t t')) fields2) fields1 in let eq = eqtype ty1 ty2 in remove_abbrev ty1; remove_abbrev ty2; eq (* Subtyping *) let subtypes = ref [] let rec build_subtype env vars t = if List.memq t vars then (t, false) else match t.desc with Tlink t' -> build_subtype env vars t' | Tvar -> (t, false) | Tarrow(t1, t2) -> let (t1', c1) = (t1, false) in let (t2', c2) = build_subtype env vars t2 in if c1 or c2 then (new_global_ty (Tarrow(t1', t2')), true) else (t, false) | Ttuple tlist -> let (tlist', clist) = List.split (List.map (build_subtype env vars) tlist) in if List.exists (function c -> c) clist then (new_global_ty (Ttuple tlist'), true) else (t, false) | Tconstr(p, tl, abbrev) -> if generic_abbrev env p then begin let t' = expand_abbrev env p tl abbrev t.level in let (t'', c) = build_subtype env vars t' in if c then (t'', true) else (t, false) end else (t, false) | Tobject (t1, _) -> if opened t1 then (t, false) else (begin try List.assq t !subtypes with Not_found -> let t' = new_global_var () in subtypes := (t, t')::!subtypes; let (t1', _) = build_subtype env vars t1 in t'.desc <- Tobject (t1', ref None); t' end, true) | Tfield(s, t1, t2) -> let (t1', _) = build_subtype env vars t1 in let (t2', _) = build_subtype env vars t2 in (new_global_ty (Tfield(s, t1', t2')), true) | Tnil -> let v = new_global_var () in (v, true) let enlarge_type env vars ty = subtypes := []; let (ty', _) = build_subtype env vars ty in subtypes := []; ty' let subtypes = ref [];; let known_subtype t1 t2 = List.exists (fun (t1', t2') -> t1 == t1' & t2 == t2') !subtypes let unify_failure trace = match trace with (t1, t1')::(t2, t2')::rem -> raise (Subtype ([], rem)) | _ -> fatal_error "Ctype.unify_failure" let rec subtype_rec env vars t1 t2 = if t1 == t2 then () else if List.memq t1 vars or List.memq t2 vars then begin try unify env t1 t2 with Unify trace -> unify_failure trace end else try match (t1.desc, t2.desc) with (Tlink t1', _) -> begin try subtype_rec env vars t1' t2 with Subtype (tr1, tr2) -> raise (Subtype (List.tl tr1, tr2)) end | (_, Tlink t2') -> begin try subtype_rec env vars t1 t2' with Subtype (tr1, tr2) -> raise (Subtype (List.tl tr1, tr2)) end | (Tvar, _) | (_, Tvar) -> begin try unify env t1 t2 with Unify trace -> unify_failure trace end | (Tarrow(t1, u1), Tarrow(t2, u2)) -> subtype_rec env vars t2 t1; subtype_rec env vars u1 u2 | (Ttuple tl1, Ttuple tl2) -> subtype_list env vars tl1 tl2 | (Tconstr(p1, tl1, abbrev1), Tconstr(p2, tl2, abbrev2)) -> if generic_abbrev env p1 then begin try subtype_rec env vars (expand_abbrev env p1 tl1 abbrev1 t1.level) t2 with Subtype (tr1, tr2) -> raise (Subtype (List.tl tr1, tr2)) end else if generic_abbrev env p2 then begin try subtype_rec env vars t1 (expand_abbrev env p2 tl2 abbrev2 t2.level) with Subtype (tr1, tr2) -> raise (Subtype (List.tl tr1, tr2)) end else begin try unify env t1 t2 with Unify trace -> unify_failure trace end | (Tconstr(p1, tl1, abbrev1), _) -> if generic_abbrev env p1 then begin try subtype_rec env vars (expand_abbrev env p1 tl1 abbrev1 t1.level) t2 with Subtype (tr1, tr2) -> raise (Subtype (List.tl tr1, tr2)) end else begin try unify env t1 t2 with Unify trace -> unify_failure trace end | (_, Tconstr(p2, tl2, abbrev2)) -> if generic_abbrev env p2 then begin try subtype_rec env vars t1 (expand_abbrev env p2 tl2 abbrev2 t2.level) with Subtype (tr1, tr2) -> raise (Subtype (List.tl tr1, tr2)) end else begin try unify env t1 t2 with Unify trace -> unify_failure trace end | (Tobject (f1, _), Tobject (f2, _)) -> if not (known_subtype t1 t2) then begin if opened f1 & opened f2 then begin try unify env t1 t2 with Unify trace -> unify_failure trace end else begin subtypes := (t1, t2) :: !subtypes; subtype_fields env vars f1 f2 end end | (_, _) -> raise (Subtype ([], [])) with Subtype (tr1, tr2) -> raise (Subtype ((t1, t2)::tr1, tr2)) and subtype_list env vars tl1 tl2 = if List.length tl1 <> List.length tl2 then raise (Subtype ([], [])); List.iter2 (subtype_rec env vars) tl1 tl2 and subtype_fields env vars ty1 ty2 = let (fields1, rest1) = flatten_fields ty1 in let (fields2, rest2) = flatten_fields ty2 in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in begin match rest1.desc with Tvar -> let nr = build_fields miss2 (newvar ()) in update_level rest1.level nr; rest1.desc <- Tlink nr | Tnil -> if miss2 <> [] then raise (Subtype ([], [])) | _ -> fatal_error "Ctype.subtype_fields (1)" end; begin match rest2.desc with Tvar -> let nr = build_fields miss1 (newvar ()) in update_level rest2.level nr; rest2.desc <- Tlink nr | Tnil -> () | _ -> fatal_error "Ctype.subtype_fields (2)" end; List.iter (fun (t1, t2) -> subtype_rec env vars t1 t2) pairs let subtype env vars ty1 ty2 = subtypes := []; begin try subtype_rec env vars ty1 ty2 with Subtype (tr1, tr2) -> raise (Subtype (expand_trace env tr1, tr2)) end; subtypes := [] (* Remove dependencies *) let inst_subst = ref ([] : (type_expr * type_expr) list) let rec nondep_type_rec env id ty = let ty = repr ty in if ty.desc = Tvar then ty else try List.assq ty !inst_subst with Not_found -> let ty' = new_gen_var () in inst_subst := (ty, ty') :: !inst_subst; ty'.desc <- begin match ty.desc with Tvar -> Tvar | Tarrow(t1, t2) -> Tarrow(nondep_type_rec env id t1, nondep_type_rec env id t2) | Ttuple tl -> Ttuple(List.map (nondep_type_rec env id) tl) | Tconstr(p, tl, abbrev) -> if Path.isfree id p then begin try (nondep_type_rec env id (expand_abbrev env p tl (ref !abbrev) ty.level)).desc with Cannot_expand -> raise Not_found end else Tconstr(p, List.map (nondep_type_rec env id) tl, ref []) | 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))) | Tfield(label, t1, t2) -> Tfield(label, nondep_type_rec env id t1, nondep_type_rec env id t2) | Tnil -> Tnil | Tlink _ -> fatal_error "Ctype.nondep_type" end; ty' let nondep_type env id ty = inst_subst := []; let ty' = nondep_type_rec env id ty in inst_subst := []; ty' let nondep_class_type env id decl = inst_subst := []; let decl = { cty_params = List.map (nondep_type_rec env id) decl.cty_params; cty_args = List.map (nondep_type_rec env id) decl.cty_args; cty_vars = Vars.fold (fun l (m, t) -> Vars.add l (m, nondep_type_rec env id t)) decl.cty_vars Vars.empty; cty_self = nondep_type_rec env id decl.cty_self; cty_concr = decl.cty_concr; cty_new = begin match decl.cty_new with None -> None | Some ty -> Some (nondep_type_rec env id ty) end } in inst_subst := []; decl (* Type pruning *) let inst_subst = ref ([] : (type_expr * type_expr) list) let rec prune_rec top cstr ty = let ty = repr ty in try List.assq ty (if top then [] else cstr) with Not_found -> match ty.desc with Tvar -> if ty.level = generic_level then begin try List.assq ty !inst_subst with Not_found -> let ty' = newvar() in inst_subst := (ty, ty') :: !inst_subst; ty' end else ty | Tarrow(t1, t2) -> newty (Tarrow(prune_rec false cstr t1, prune_rec false cstr t2)) | Ttuple tl -> newty (Ttuple(List.map (prune_rec false cstr) tl)) | Tconstr(p, tl, _) -> begin try List.assq ty !inst_subst with Not_found -> let ty' = newvar() in inst_subst := (ty, ty') :: !inst_subst; let ty'' = newty (Tconstr(p, List.map (prune_rec false cstr) tl, ref [])) in ty'.desc <- Tlink ty''; ty'' end | Tobject (t1, name) -> begin try List.assq ty !inst_subst with Not_found -> let ty' = newvar() in inst_subst := (ty, ty') :: !inst_subst; let ty'' = newty (Tobject (prune_rec false cstr t1, ref (match !name with None -> None | Some (p, tl) -> Some (p, List.map (prune_rec false cstr) tl)))) in ty'.desc <- Tlink ty''; ty'' end | Tfield(label, t1, t2) -> newty (Tfield(label, prune_rec false cstr t1, prune_rec false cstr t2)) | Tnil -> newty Tnil | Tlink _ -> fatal_error "Ctype.prune_rec" let prune_cstr cstr (old_cstr, new_cstr) ((ty, v) as c) = let c' = try (v, List.assq ty old_cstr) with Not_found -> match ty.desc with Tvar -> (v, v) | _ -> (v, prune_rec true cstr ty) in (c :: old_cstr, c' :: new_cstr) let prune ty leaves = inst_subst := []; let cstr = List.map (fun leaf -> (repr leaf, newvar ())) leaves in let new_ty = prune_rec true cstr ty in inst_subst := []; (new_ty, List.map (fun (ty, v) -> (v, ty)) cstr) let prune_class_type cl = inst_subst := []; let cstr = List.map (fun leaf -> (repr leaf, newvar ())) cl.cty_params in let args = List.map (prune_rec false cstr) cl.cty_args in let vars = Vars.fold (fun lab (mut, ty) -> Vars.add lab (mut, prune_rec false cstr ty)) cl.cty_vars Vars.empty in let self = prune_rec true cstr cl.cty_self in let (_, cstr) = List.fold_left (prune_cstr cstr) ([], []) cstr in inst_subst := []; (List.rev cstr, args, vars, self) (* --- *) let rec row_variable ty = let ty = repr ty in match ty.desc with Tfield (_, _, ty) -> row_variable ty | Tvar -> ty | Tnil -> raise Not_found | _ -> fatal_error "Ctype.row_variable" let close_object ty = let rec close ty = let ty = repr ty in match ty.desc with Tvar -> ty.desc <- Tlink {desc = Tnil; level = ty.level} | Tfield(_, _, ty') -> close ty' | Tnil -> () | _ -> fatal_error "Ctype.close_object (1)" in match (repr ty).desc with Tobject (ty, _) -> close ty | Tconstr (_, _, _) -> () (* Already closed *) | _ -> fatal_error "Ctype.close_object (2)" let set_object_name ty params id = match (repr ty).desc with Tobject (fi, nm) -> begin try nm := Some (Path.Pident id, (row_variable fi)::params) with Not_found -> () end | Tconstr (_, _, _) -> () | _ -> fatal_error "Ctype.set_object_name" let remove_object_name ty = match (repr ty).desc with Tobject (_, nm) -> nm := None | Tconstr (_, _, _) -> () | _ -> fatal_error "Ctype.remove_object_name" (* Abbreviation correctness *) exception Nonlinear_abbrev exception Recursive_abbrev let rec non_recursive_abbrev env path constrs ty = let ty = repr ty in match ty.desc with Tarrow (ty1, ty2) -> non_recursive_abbrev env path constrs ty1; non_recursive_abbrev env path constrs ty2 | Ttuple tl -> List.iter (non_recursive_abbrev env path constrs) tl | Tconstr(p, args, abbrev) -> if Path.same path p then raise Recursive_abbrev else begin begin try let ty' = expand_abbrev env p args abbrev ty.level in if List.memq ty' constrs then () else non_recursive_abbrev env path (ty'::constrs) ty' with Cannot_expand -> () end end | _ (* Tvar | Tobject (_, _) | Tfield (_, _, _) | Tnil *) -> () let rec path_assoc x = function [] -> raise Not_found | (a,b)::l -> if Path.same a x then b else path_assoc x l let visited_abbrevs = ref [] let visited_abbrev p args = try let slot = path_assoc p !visited_abbrevs in if List.exists (function args' -> List.for_all2 (fun ty ty' -> repr ty == ty') args args') !slot then true else begin slot := (List.map repr args)::!slot; false end with Not_found -> visited_abbrevs := (p, ref [args])::!visited_abbrevs; false let rec linear_abbrev env path params visited ty = let ty = repr ty in match ty.desc with Tarrow (ty1, ty2) -> linear_abbrev env path params visited ty1; linear_abbrev env path params visited ty2 | Ttuple tl -> List.iter (linear_abbrev env path params visited) tl | Tconstr(p, args, abbrev) -> if Path.same p path then begin if List.exists (fun (ty1, ty2) -> repr ty1 != repr ty2) (List.combine params args) then raise Nonlinear_abbrev end else begin try let ty' = expand_abbrev env p args abbrev ty.level in if not (visited_abbrev p args) then linear_abbrev env path params visited ty' with Cannot_expand -> if not (List.memq ty visited) then begin List.iter (linear_abbrev env path params (ty::visited)) args end end | Tobject (ty', _) -> if not (List.memq ty visited) then linear_abbrev env path params (ty::visited) ty' | Tfield(_, ty1, ty2) -> linear_abbrev env path params visited ty1; linear_abbrev env path params visited ty2 | _ (* Tvar | Tnil *) -> () let correct_abbrev env ident params ty = let path = Path.Pident ident in non_recursive_abbrev env path [] ty; if params <> [] then begin visited_abbrevs := []; linear_abbrev env path params [] ty; visited_abbrevs := [] end; remove_abbrev ty (* Miscellaneous *) let unroll_abbrev id tl ty = let ty = repr ty in match ty.desc with Tobject (fi, nm) -> ty.desc <- Tlink {desc = Tconstr (Path.Pident id, tl, ref []); level = generic_level}; {desc = Tobject (fi, nm); level = ty.level} | _ -> ty type closed_schema_result = Var of type_expr | Row_var of type_expr exception Failed of closed_schema_result let visited = ref [] let rec closed_schema_rec ty = let ty = repr ty in match ty.desc with Tvar -> if ty.level != generic_level then raise (Failed (Var ty)) | Tarrow(t1, t2) -> closed_schema_rec t1; closed_schema_rec t2 | Ttuple tl -> List.iter closed_schema_rec tl | Tconstr(p, tl, _) -> if not (List.memq ty !visited) then begin visited := ty::!visited; List.iter closed_schema_rec tl end | Tobject(f, {contents = Some (_, p)}) -> if not (List.memq ty !visited) then begin visited := ty::!visited; begin try closed_schema_rec f with Failed (Row_var v) -> raise (Failed (Var v)) | Failed (Var v) -> raise (Failed (Row_var v)) end; List.iter closed_schema_rec p end | Tobject(f, _) -> if not (List.memq ty !visited) then begin visited := ty::!visited; try closed_schema_rec f with Failed (Row_var v) -> raise (Failed (Var v)) | Failed (Var v) -> raise (Failed (Row_var v)) end | Tfield(_, t1, t2) -> begin try closed_schema_rec t1 with Failed (Row_var v) -> raise (Failed (Var v)) | Failed (Var v) -> raise (Failed (Row_var v)) end; closed_schema_rec t2 | Tnil -> () | Tlink _ -> fatal_error "Ctype.closed_schema" let closed_schema ty = visited := []; try closed_schema_rec ty; visited := []; true with Failed _ -> visited := []; false let closed_schema_verbose ty = visited := []; try closed_schema_rec ty; visited := []; None with Failed status -> visited := []; Some status let is_generic ty = let ty = repr ty in match ty.desc with Tvar -> ty.level = generic_level | _ -> fatal_error "Ctype.is_generic" let rec arity ty = match (repr ty).desc with Tarrow(t1, t2) -> 1 + arity t2 | _ -> 0