From 83ae0ff6982834b91d1812171436c858dcb14bd9 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa Date: Tue, 24 Dec 2024 21:49:23 -0500 Subject: [PATCH] Move code --- typing/typedecl.ml | 108 ++++++++++++++++++++++----------------------- 1 file changed, 54 insertions(+), 54 deletions(-) diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 4f8d02cf356..23b437e946d 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -1948,60 +1948,6 @@ let update_decls_jkind env decls = - if -rectypes is not used, we only allow cycles in the type graph if they go through an object or polymorphic variant type *) -(* We only allow recursion in unboxed product types to occur through boxes, - otherwise the type is uninhabitable and usually also infinite-size. - See [typing-layouts-unboxed-records/recursive.ml]. - - Because `check_well_founded` already ruled out recursion through structural - types (for this check, we care about unboxed tuples and aliases), we just - look for a cycle in nominal unboxed types ([@@unboxed] types and unboxed - records), tracking the set of seen paths. - - An alternative implementation could have introduced layout variables (for - this check only), finding infinite-size types via the occurs check. Such an - implementation might be more principled, accepting finite-size recursive - types like [type t = #{ t : t }]. The current implementation gives more - informative error traces, and leaves the flexiblity to switch to a less - restrictive check in the future. -*) -let check_unboxed_recursion ~abs_env env loc path0 ty0 to_check = - let check_visited parents trace ty = - match get_desc ty with - | Tconstr (path, _, _) -> - if Path.Set.mem path parents then - let err = Unboxed_recursion(Path.name path0, abs_env, List.rev trace) in - raise (Error(loc, err)) - | _ -> () - in - let rec expand parents trace ty = - match Ctype.path_and_expansion env ty with - | Some (path, ty') -> - expand (Path.Set.add path parents) (Expands_to (ty, ty') :: trace) ty' - | None -> - parents, trace, ty - in - let rec visit parents trace ty = - (* Expand even if this type isn't part of the recursive group, because it - could be instantiated back into the group by a type parameter. *) - let parents, trace, ty = expand parents trace ty in - match get_desc ty with - | Tconstr (path, _, _) -> - (* If we get a Tconstr, we only need to visit if it's part of this group - of mutually recursive typedecls. *) - if not (to_check path) then () else - check_visited parents trace ty; - visit_subtypes (Path.Set.add path parents) trace ty - | _ -> - visit_subtypes parents trace ty - and visit_subtypes parents trace ty = - List.iter (fun ty' -> - let trace = Contains (ty, ty') :: trace in - check_visited parents trace ty'; - visit parents trace ty') - (Ctype.contained_without_boxing env ty) - in - Ctype.wrap_trace_gadt_instances env (visit Path.Set.empty []) ty0 - let check_well_founded ~abs_env env loc path to_check visited ty0 = let rec check parents trace ty = if TypeSet.mem ty parents then begin @@ -2116,6 +2062,60 @@ let check_well_founded_decl ~abs_env env loc path decl to_check = end)} in it.it_type_declaration it (Ctype.generic_instance_declaration decl) +(* We only allow recursion in unboxed product types to occur through boxes, + otherwise the type is uninhabitable and usually also infinite-size. + See [typing-layouts-unboxed-records/recursive.ml]. + + Because `check_well_founded` already ruled out recursion through structural + types (for this check, we care about unboxed tuples and aliases), we just + look for a cycle in nominal unboxed types ([@@unboxed] types and unboxed + records), tracking the set of seen paths. + + An alternative implementation could have introduced layout variables (for + this check only), finding infinite-size types via the occurs check. Such an + implementation might be more principled, accepting finite-size recursive + types like [type t = #{ t : t }]. The current implementation gives more + informative error traces, and leaves the flexiblity to switch to a less + restrictive check in the future. +*) +let check_unboxed_recursion ~abs_env env loc path0 ty0 to_check = + let check_visited parents trace ty = + match get_desc ty with + | Tconstr (path, _, _) -> + if Path.Set.mem path parents then + let err = Unboxed_recursion(Path.name path0, abs_env, List.rev trace) in + raise (Error(loc, err)) + | _ -> () + in + let rec expand parents trace ty = + match Ctype.path_and_expansion env ty with + | Some (path, ty') -> + expand (Path.Set.add path parents) (Expands_to (ty, ty') :: trace) ty' + | None -> + parents, trace, ty + in + let rec visit parents trace ty = + (* Expand even if this type isn't part of the recursive group, because it + could be instantiated back into the group by a type parameter. *) + let parents, trace, ty = expand parents trace ty in + match get_desc ty with + | Tconstr (path, _, _) -> + (* If we get a Tconstr, we only need to visit if it's part of this group + of mutually recursive typedecls. *) + if not (to_check path) then () else + check_visited parents trace ty; + visit_subtypes (Path.Set.add path parents) trace ty + | _ -> + visit_subtypes parents trace ty + and visit_subtypes parents trace ty = + List.iter (fun ty' -> + let trace = Contains (ty, ty') :: trace in + check_visited parents trace ty'; + visit parents trace ty') + (Ctype.contained_without_boxing env ty) + in + Ctype.wrap_trace_gadt_instances env (visit Path.Set.empty []) ty0 + let check_unboxed_recursion_decl ~abs_env env loc path decl to_check = let decl = Ctype.generic_instance_declaration decl in let ty = Btype.newgenty (Tconstr (path, decl.type_params, ref Mnil)) in