diff --git a/middle_end/flambda/types/template/flambda_type.templ.ml b/middle_end/flambda/types/template/flambda_type.templ.ml index ed2e09a46add..0025a8a213f7 100644 --- a/middle_end/flambda/types/template/flambda_type.templ.ml +++ b/middle_end/flambda/types/template/flambda_type.templ.ml @@ -301,26 +301,16 @@ let prove_is_int env t : bool proof = match expand_head t env with | Const (Tagged_immediate _) -> Proved true | Const _ -> wrong_kind () - | Value (Ok (Variant blocks_imms)) -> - begin match blocks_imms.blocks, blocks_imms.immediates with - | Unknown, Unknown -> Unknown - | Unknown, Known imms -> - if is_bottom env imms - then Proved false - else Unknown - | Known blocks, Unknown -> - if Row_like.For_blocks.is_bottom blocks - then Proved true - else Unknown - | Known blocks, Known imms -> - (* CR mshinwell: Should we tighten things up by causing fatal errors - in cases such as [blocks] and [imms] both being bottom? *) - if Row_like.For_blocks.is_bottom blocks then - if is_bottom env imms then Invalid - else Proved true - else - if is_bottom env imms then Proved false - else Unknown + | Value (Ok (Variant variant)) -> + begin match variant with + (* CR vlaviron: We fail to return Invalid if the underlying variant is + bottom. However, in practice this should never happen: bottom variants + can only be created by either an explicit call to Variant.create with + bottom values, or if for some reason a meet returns a bottom type + instead of the Bottom constructor. *) + | Immediates _ -> Proved true + | Blocks _ -> Proved false + | Either _ -> Unknown end | Value (Ok (Boxed_float _ | Boxed_int32 _ | Boxed_int64 _ | Boxed_nativeint _ | Closures _ | String _ | Array _)) -> Proved false @@ -340,29 +330,19 @@ let prove_tags_must_be_a_block env t : Tag.Set.t proof = match expand_head t env with | Const (Tagged_immediate _) -> Unknown | Const _ -> wrong_kind () - | Value (Ok (Variant blocks_imms)) -> - begin match blocks_imms.immediates with - | Unknown -> Unknown - | Known imms -> - if not (is_bottom env imms) then - (* CR vlaviron: This case could be completely ignored if we're - only interested in the set of tags this type can have. - It is there because this function used to return Invalid - when it couldn't definitively prove that this type represents - a block, but this caused a number of problems so this was - switched to Unknown (which, unlike Invalid, is always sound). - There remain a question of whether we actually want two - different variants of this function, one for simplification - of the get_tag primitive which may reasonably expect to error - if its argument cannot be proved to be a block, and one for - simplification of CSE parameters containing a get_tag equation, - which can occur at places where the type is not known to be a block. - *) - Unknown - else - match blocks_imms.blocks with - | Unknown -> Unknown - | Known blocks -> + | Value (Ok (Variant variant)) -> + begin match variant with + | Immediates _ -> Invalid + | Blocks { blocks; is_unique = _; } + | Either { immediates = _; + immediates_extension = _; + blocks; + blocks_extension = _; + is_unique = _; + } -> + begin match blocks with + | Unknown -> Unknown + | Known blocks -> (* CR mshinwell: maybe [all_tags] should return the [Invalid] case directly? *) match Row_like.For_blocks.all_tags blocks with @@ -370,6 +350,7 @@ let prove_tags_must_be_a_block env t : Tag.Set.t proof = | Known tags -> if Tag.Set.is_empty tags then Invalid else Proved tags + end end | Value (Ok (Boxed_float _ | Boxed_int32 _ | Boxed_int64 _ | Boxed_nativeint _)) -> Proved (Tag.Set.singleton Tag.custom_tag) @@ -441,15 +422,13 @@ let prove_equals_tagged_immediates env t : Targetint_31_63.Set.t proof = | Const (Tagged_immediate imm) -> Proved (Targetint_31_63.Set.singleton imm) | Const (Naked_immediate _ | Naked_float _ | Naked_int32 _ | Naked_int64 _ | Naked_nativeint _) -> wrong_kind () - | Value (Ok (Variant blocks_imms)) -> - begin match blocks_imms.blocks, blocks_imms.immediates with - | Unknown, Unknown | Unknown, Known _ | Known _, Unknown -> Unknown - | Known blocks, Known imms -> - (* CR mshinwell: Check this. Again it depends on the context; is - this a context where variants are ok? *) - if not (Row_like.For_blocks.is_bottom blocks) - then Unknown - else prove_naked_immediates env imms + | Value (Ok (Variant variant)) -> + begin match variant with + | Blocks _ -> Invalid + | Either _ -> Unknown + | Immediates { immediates = Unknown; } -> Unknown + | Immediates { immediates = Known immediates; } -> + prove_naked_immediates env immediates end | Value (Ok _) -> Invalid | Value Unknown -> Unknown @@ -478,22 +457,16 @@ let prove_tags_and_sizes env t : Targetint_31_63.Imm.t Tag.Map.t proof = match expand_head t env with | Const (Tagged_immediate _) -> Unknown | Const _ -> wrong_kind () - | Value (Ok (Variant blocks_imms)) -> - begin match blocks_imms.immediates with - (* CR mshinwell: Care. Should this return [Unknown] or [Invalid] if - there is the possibility of the type representing a tagged - immediate? *) - | Unknown -> Unknown - | Known immediates -> - if is_bottom env immediates then - match blocks_imms.blocks with - | Unknown -> Unknown - | Known blocks -> - match Row_like.For_blocks.all_tags_and_sizes blocks with - | Unknown -> Unknown - | Known tags_and_sizes -> Proved tags_and_sizes - else - Unknown + | Value (Ok (Variant variant)) -> + begin match variant with + | Immediates _ -> Invalid + | Either _ -> Unknown + | Blocks { blocks = Unknown; is_unique = _; } -> Unknown + | Blocks { blocks = Known blocks; is_unique = _; } -> + begin match Row_like.For_blocks.all_tags_and_sizes blocks with + | Unknown -> Unknown + | Known tags_and_sizes -> Proved tags_and_sizes + end end | Value (Ok _) -> Invalid | Value Unknown -> Unknown @@ -533,43 +506,66 @@ let prove_variant_like env t : variant_like_proof proof_allowing_kind_mismatch = non_const_ctors_with_sizes = Tag.Scannable.Map.empty; } | Const _ -> Wrong_kind - | Value (Ok (Variant blocks_imms)) -> - begin match blocks_imms.blocks with - | Unknown -> Unknown - | Known blocks -> - match Row_like.For_blocks.all_tags_and_sizes blocks with - | Unknown -> Unknown - | Known non_const_ctors_with_sizes -> - let non_const_ctors_with_sizes = - Tag.Map.fold - (fun tag size (result : _ Or_unknown.t) : _ Or_unknown.t -> - match result with - | Unknown -> Unknown - | Known result -> - match Tag.Scannable.of_tag tag with - | None -> Unknown - | Some tag -> - Known (Tag.Scannable.Map.add tag size result)) - non_const_ctors_with_sizes - (Or_unknown.Known Tag.Scannable.Map.empty) - in - match non_const_ctors_with_sizes with + | Value (Ok (Variant variant)) -> + let const_ctors : _ Or_unknown.t = + match variant with + | Immediates { immediates; } + | Either { + immediates; + immediates_extension = _; + blocks = _; + blocks_extension = _; + is_unique = _; + } -> + begin match immediates with | Unknown -> Unknown - | Known non_const_ctors_with_sizes -> - let const_ctors : _ Or_unknown.t = - match blocks_imms.immediates with - | Unknown -> Unknown - | Known imms -> - begin match prove_naked_immediates env imms with - | Unknown -> Unknown - | Invalid -> Known Targetint_31_63.Set.empty - | Proved const_ctors -> Known const_ctors - end - in - Proved { - const_ctors; - non_const_ctors_with_sizes; - } + | Known imms -> + begin match prove_naked_immediates env imms with + | Unknown -> Unknown + | Invalid -> Known Targetint_31_63.Set.empty + | Proved const_ctors -> Known const_ctors + end + end + | Blocks _ -> Known Targetint_31_63.Set.empty + in + let non_const_ctors_with_sizes : _ Or_unknown.t = + match variant with + | Immediates _ -> Known Tag.Scannable.Map.empty + | Blocks { blocks; is_unique = _; } + | Either { + immediates = _; + immediates_extension = _; + blocks; + blocks_extension = _; + is_unique = _; + } -> + begin match blocks with + | Unknown -> Unknown + | Known blocks -> + begin match Row_like.For_blocks.all_tags_and_sizes blocks with + | Unknown -> Unknown + | Known non_const_ctors_with_sizes -> + Tag.Map.fold + (fun tag size (result : _ Or_unknown.t) : _ Or_unknown.t -> + match result with + | Unknown -> Unknown + | Known result -> + match Tag.Scannable.of_tag tag with + | None -> Unknown + | Some tag -> + Known (Tag.Scannable.Map.add tag size result)) + non_const_ctors_with_sizes + (Or_unknown.Known Tag.Scannable.Map.empty) + end + end + in + begin match non_const_ctors_with_sizes with + | Unknown -> Unknown + | Known non_const_ctors_with_sizes -> + Proved { + const_ctors; + non_const_ctors_with_sizes; + } end | Value (Ok _) -> Invalid | Value Unknown -> Unknown @@ -587,24 +583,13 @@ let prove_is_a_boxed_number env t | Const (Tagged_immediate _) -> Proved Untagged_immediate | Const _ -> Wrong_kind | Value Unknown -> Unknown - | Value (Ok (Variant { blocks; immediates; is_unique = _; })) -> - begin match blocks, immediates with - | Unknown, Unknown -> Unknown - | Unknown, Known imms -> - if is_bottom env imms - then Invalid - else Unknown - | Known blocks, Unknown -> - if Row_like.For_blocks.is_bottom blocks - then Proved Untagged_immediate - else Unknown - | Known blocks, Known imms -> - if is_bottom env imms then - Invalid - else if Row_like.For_blocks.is_bottom blocks then - Proved Untagged_immediate - else - Unknown + | Value (Ok (Variant variant)) -> + begin match variant with + | Immediates _ -> Proved Untagged_immediate + (* CR vlaviron: The previous code returned Invalid for blocks. + I'm not sure it's correct, and Invalid is probably handled the + same way as Unknown by callers, so I'm returning Unknown. *) + | Blocks _ | Either _ -> Unknown end | Value (Ok (Boxed_float _)) -> Proved Naked_float | Value (Ok (Boxed_int32 _)) -> Proved Naked_int32 @@ -766,39 +751,43 @@ let prove_is_tagging_of_simple match expand_head t env with | Const (Tagged_immediate imm) -> Proved (Simple.const (Reg_width_const.naked_immediate imm)) - | Value (Ok (Variant { immediates; blocks; is_unique = _; })) -> - begin match blocks with - | Unknown -> Unknown - | Known blocks -> - match prove_function with - | Prove_is_always_tagging_of_simple - when not (Row_like.For_blocks.is_bottom blocks) -> - Unknown - | Prove_is_always_tagging_of_simple - (* when (Row_like.For_blocks.is_bottom blocks) *) - | Prove_could_be_tagging_of_simple -> - match immediates with - | Unknown -> Unknown - | Known t -> - let from_alias = - match - Typing_env.get_canonical_simple_exn - env ~min_name_mode (get_alias_exn t) - with - | simple -> Some simple - | exception Not_found -> None - in - match from_alias with - | Some simple -> Proved simple - | None -> - match prove_naked_immediates env t with - | Unknown -> Unknown - | Invalid -> Invalid - | Proved imms -> - match Targetint_31_63.Set.get_singleton imms with - | Some imm -> - Proved (Simple.const (Reg_width_const.naked_immediate imm)) - | None -> Unknown + | Value (Ok (Variant variant)) -> + begin match variant, prove_function with + | Immediates { immediates; }, _ + | Either { + immediates; + immediates_extension = _; + blocks = _; + blocks_extension = _; + is_unique = _; + }, Prove_could_be_tagging_of_simple -> + begin match immediates with + | Unknown -> Unknown + | Known t -> + let from_alias = + match + Typing_env.get_canonical_simple_exn + env ~min_name_mode (get_alias_exn t) + with + | simple -> Some simple + | exception Not_found -> None + in + begin match from_alias with + | Some simple -> Proved simple + | None -> + begin match prove_naked_immediates env t with + | Unknown -> Unknown + | Invalid -> Invalid + | Proved imms -> + begin match Targetint_31_63.Set.get_singleton imms with + | Some imm -> + Proved (Simple.const (Reg_width_const.naked_immediate imm)) + | None -> Unknown + end + end + end + end + | Blocks _, _ | Either _, Prove_is_always_tagging_of_simple -> Unknown end | Value Unknown -> Unknown | Value _ -> Invalid @@ -873,33 +862,30 @@ let[@inline] prove_block_field_simple_aux env ~min_name_mode t get_field : Simpl | Const _ -> if K.equal (kind t) K.value then Invalid else wrong_kind () - | Value (Ok (Variant { immediates; blocks; is_unique = _; })) -> - begin match immediates with - | Unknown -> Unknown - | Known imms -> + | Value (Ok (Variant variant)) -> + begin match variant with + | Immediates _ -> Invalid + | Either _ -> Unknown + | Blocks { blocks; is_unique = _; } -> begin match blocks with | Unknown -> Unknown | Known blocks -> - if Row_like.For_blocks.is_bottom blocks then Invalid - else if not (is_obviously_bottom imms) then - Unknown - else - begin match (get_field blocks : _ Or_unknown_or_bottom.t) with - | Bottom -> Invalid - | Unknown -> Unknown - | Ok ty -> - begin match get_alias_exn ty with - | simple -> - begin match - Typing_env.get_canonical_simple_exn env ~min_name_mode simple - with - | simple -> Proved simple - | exception Not_found -> Unknown - end + begin match (get_field blocks : _ Or_unknown_or_bottom.t) with + | Bottom -> Invalid + | Unknown -> Unknown + | Ok ty -> + begin match get_alias_exn ty with + | simple -> + begin match + Typing_env.get_canonical_simple_exn env ~min_name_mode simple + with + | simple -> Proved simple | exception Not_found -> Unknown end + | exception Not_found -> Unknown end end + end end | Value (Ok _) -> Invalid | Value Unknown -> Unknown @@ -1020,13 +1006,13 @@ let reify ?allowed_if_free_vars_defined_in ?additional_free_var_criterion in match expand_head t env with | Const const -> Simple (Simple.const_from_descr const) - | Value (Ok (Variant blocks_imms)) -> - if blocks_imms.is_unique && not allow_unique then try_canonical_simple () - else - begin match blocks_imms.blocks, blocks_imms.immediates with - | Known blocks, Known imms -> - if is_bottom env imms then - begin match Row_like.For_blocks.get_singleton blocks with + | Value (Ok (Variant variant)) -> + begin match variant with + | Either _ | Blocks { blocks = Unknown; is_unique = _; } + | Immediates { immediates = Unknown; } -> try_canonical_simple () + | Blocks { blocks = Known blocks; is_unique; } -> + if is_unique && not allow_unique then try_canonical_simple () + else begin match Row_like.For_blocks.get_singleton blocks with | None -> try_canonical_simple () | Some ((tag, size), field_types) -> assert (Targetint_31_63.Imm.equal size @@ -1066,26 +1052,24 @@ let reify ?allowed_if_free_vars_defined_in ?additional_free_var_criterion vars_or_symbols_or_tagged_immediates = 0 then Lift (Immutable_block { tag; - is_unique = blocks_imms.is_unique; + is_unique; fields = vars_or_symbols_or_tagged_immediates; }) else try_canonical_simple () end + end + | Immediates { immediates = Known immediates; } -> + begin match prove_naked_immediates env immediates with + | Proved imms -> + begin match Targetint_31_63.Set.get_singleton imms with + | None -> try_canonical_simple () + | Some imm -> + Simple (Simple.const (Reg_width_const.tagged_immediate imm)) end - else if Row_like.For_blocks.is_bottom blocks then - match prove_naked_immediates env imms with - | Proved imms -> - begin match Targetint_31_63.Set.get_singleton imms with - | None -> try_canonical_simple () - | Some imm -> - Simple (Simple.const (Reg_width_const.tagged_immediate imm)) - end - | Unknown -> try_canonical_simple () - | Invalid -> Invalid - else - try_canonical_simple () - | _, _ -> try_canonical_simple () + | Unknown -> try_canonical_simple () + | Invalid -> Invalid + end end | Value (Ok (Closures closures)) -> (* CR mshinwell: Here and above, move to separate function. *) diff --git a/middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.ml b/middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.ml index 43bb69a97663..cf27d9f224eb 100644 --- a/middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.ml +++ b/middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.ml @@ -37,17 +37,9 @@ type t = let print_with_cache ~cache ppf t = match t with - | Variant { blocks; immediates; is_unique } -> - (* CR mshinwell: Improve so that we elide blocks and/or immediates when - they're empty. *) - Format.fprintf ppf - "@[(Variant%s@ \ - @[(blocks@ %a)@]@ \ - @[(tagged_imms@ %a)@]\ - )@]" - (if is_unique then " unique" else "") - (Or_unknown.print (Blocks.print_with_cache ~cache)) blocks - (Or_unknown.print (T.print_with_cache ~cache)) immediates + | Variant variant -> + Format.fprintf ppf "@[(Variant@ %a)@]" + (Variant.print_with_cache ~cache) variant | Boxed_float naked_ty -> Format.fprintf ppf "@[(Boxed_float@ %a)@]" (T.print_with_cache ~cache) naked_ty @@ -72,30 +64,12 @@ let print_with_cache ~cache ppf t = let print ppf t = print_with_cache ~cache:(Printing_cache.create ()) ppf t -let apply_renaming_variant blocks immediates perm = - let immediates' = - Or_unknown.map immediates ~f:(fun immediates -> - T.apply_renaming immediates perm) - in - let blocks' = - Or_unknown.map blocks ~f:(fun blocks -> - Blocks.apply_renaming blocks perm) - in - if immediates == immediates' && blocks == blocks' then - None - else - Some (blocks', immediates') - let apply_renaming t perm = match t with - | Variant { blocks; immediates; is_unique; } -> - begin match - apply_renaming_variant blocks immediates perm - with - | None -> t - | Some (blocks, immediates) -> - Variant (Variant.create ~is_unique ~blocks ~immediates) - end + | Variant variant -> + let variant' = Variant.apply_renaming variant perm in + if variant == variant' then t + else Variant variant' | Boxed_float ty -> let ty' = T.apply_renaming ty perm in if ty == ty' then t @@ -127,10 +101,7 @@ let apply_renaming t perm = let free_names t = match t with - | Variant { blocks; immediates; is_unique = _; } -> - Name_occurrences.union - (Or_unknown.free_names Blocks.free_names blocks) - (Or_unknown.free_names T.free_names immediates) + | Variant variant -> Variant.free_names variant | Boxed_float ty -> T.free_names ty | Boxed_int32 ty -> T.free_names ty | Boxed_int64 ty -> T.free_names ty @@ -142,10 +113,7 @@ let free_names t = let all_ids_for_export t = match t with - | Variant { blocks; immediates; is_unique = _; } -> - Ids_for_export.union - (Or_unknown.all_ids_for_export Blocks.all_ids_for_export blocks) - (Or_unknown.all_ids_for_export T.all_ids_for_export immediates) + | Variant variant -> Variant.all_ids_for_export variant | Boxed_float ty -> T.all_ids_for_export ty | Boxed_int32 ty -> T.all_ids_for_export ty | Boxed_int64 ty -> T.all_ids_for_export ty @@ -199,98 +167,12 @@ let eviscerate t : _ Or_unknown.t = | String _ | Array _ -> Unknown -let meet_unknown meet_contents ~contents_is_bottom env - (or_unknown1 : _ Or_unknown.t) (or_unknown2 : _ Or_unknown.t) - : ((_ Or_unknown.t) * TEE.t) Or_bottom.t = - match or_unknown1, or_unknown2 with - | Unknown, Unknown -> Ok (Unknown, TEE.empty ()) - (* CR mshinwell: Think about the next two cases more *) - | Known contents, _ when contents_is_bottom contents -> Bottom - | _, Known contents when contents_is_bottom contents -> Bottom - | _, Unknown -> Ok (or_unknown1, TEE.empty ()) - | Unknown, _ -> Ok (or_unknown2, TEE.empty ()) - | Known contents1, Known contents2 -> - let result = - Or_bottom.map (meet_contents env contents1 contents2) - ~f:(fun (contents, env_extension) -> - Or_unknown.Known contents, env_extension) - in - match result with - | Bottom | Ok (Unknown, _) -> result - | Ok (Known contents, _env_extension) -> - (* XXX Why isn't [meet_contents] returning bottom? *) - if contents_is_bottom contents then Bottom - else result - -let join_unknown join_contents (env : Join_env.t) - (or_unknown1 : _ Or_unknown.t) (or_unknown2 : _ Or_unknown.t) - : _ Or_unknown.t = - match or_unknown1, or_unknown2 with - | _, Unknown - | Unknown, _ -> Unknown - | Known contents1, Known contents2 -> - join_contents env contents1 contents2 - -let meet_variant env - ~blocks1 ~imms1 ~blocks2 ~imms2 : _ Or_bottom.t = - let blocks = - meet_unknown Blocks.meet ~contents_is_bottom:Blocks.is_bottom - env blocks1 blocks2 - in - let blocks : _ Or_bottom.t = - (* XXX Clean this up *) - match blocks with - | Bottom | Ok (Or_unknown.Unknown, _) -> blocks - | Ok (Or_unknown.Known blocks', _) -> - if Blocks.is_bottom blocks' then Bottom else blocks - in - let imms = - meet_unknown T.meet ~contents_is_bottom:T.is_obviously_bottom - env imms1 imms2 - in - let imms : _ Or_bottom.t = - match imms with - | Bottom | Ok (Or_unknown.Unknown, _) -> imms - | Ok (Or_unknown.Known imms', _) -> - if T.is_obviously_bottom imms' then Bottom else imms - in - match blocks, imms with - | Bottom, Bottom -> Bottom - | Ok (blocks, env_extension), Bottom -> - let immediates : _ Or_unknown.t = Known (T.bottom K.naked_immediate) in - Ok (blocks, immediates, env_extension) - | Bottom, Ok (immediates, env_extension) -> - let blocks : _ Or_unknown.t = Known (Blocks.create_bottom ()) in - Ok (blocks, immediates, env_extension) - | Ok (blocks, env_extension1), Ok (immediates, env_extension2) -> - begin match (blocks : _ Or_unknown.t) with - | Unknown -> () - | Known blocks -> assert (not (Blocks.is_bottom blocks)); - end; - begin match (immediates : _ Or_unknown.t) with - | Unknown -> () - | Known imms -> assert (not (T.is_obviously_bottom imms)); - end; - let env_extension = - let env = Meet_env.env env in - let join_env = - Join_env.create env ~left_env:env ~right_env:env - in - TEE.join join_env env_extension1 env_extension2 - in - Ok (blocks, immediates, env_extension) - let meet env t1 t2 : _ Or_bottom.t = match t1, t2 with - | Variant { blocks = blocks1; immediates = imms1; is_unique = is_unique1; }, - Variant { blocks = blocks2; immediates = imms2; is_unique = is_unique2; } -> + | Variant variant1, Variant variant2 -> Or_bottom.map - (meet_variant env ~blocks1 ~imms1 ~blocks2 ~imms2) - ~f:(fun (blocks, immediates, env_extension) -> - (* Uniqueness tracks whether duplication/lifting is allowed. - It must always be propagated, both for meet and join. *) - let is_unique = is_unique1 || is_unique2 in - Variant (Variant.create ~is_unique ~blocks ~immediates), env_extension) + (Variant.meet env variant1 variant2) + ~f:(fun (variant, env_extension) -> Variant variant, env_extension) | Boxed_float n1, Boxed_float n2 -> Or_bottom.map (T.meet env n1 n2) @@ -334,33 +216,10 @@ let meet env t1 t2 : _ Or_bottom.t = incompatible. This could break very hard for users of Obj. *) Bottom -let join_variant env - ~blocks1 ~imms1 ~blocks2 ~imms2 : _ Or_unknown.t = - let blocks_join env b1 b2 : _ Or_unknown.t = - Known (Blocks.join env b1 b2) - in - let blocks = - join_unknown blocks_join env blocks1 blocks2 - in - let imms = - join_unknown (T.join ?bound_name:None) env imms1 imms2 - in - match blocks, imms with - | Unknown, Unknown -> Unknown - | Known _, Unknown | Unknown, Known _ | Known _, Known _ -> - Known (blocks, imms) - let join env t1 t2 : _ Or_unknown.t = match t1, t2 with - | Variant { blocks = blocks1; immediates = imms1; is_unique = is_unique1; }, - Variant { blocks = blocks2; immediates = imms2; is_unique = is_unique2; } -> - Or_unknown.map - (join_variant env ~blocks1 ~imms1 ~blocks2 ~imms2) - ~f:(fun (blocks, immediates) -> - (* Uniqueness tracks whether duplication/lifting is allowed. - It must always be propagated, both for meet and join. *) - let is_unique = is_unique1 || is_unique2 in - Variant (Variant.create ~is_unique ~blocks ~immediates)) + | Variant variant1, Variant variant2 -> + Known (Variant (Variant.join env variant1 variant2)) | Boxed_float n1, Boxed_float n2 -> Or_unknown.map (T.join env n1 n2) diff --git a/middle_end/flambda/types/type_of_kind/variant.rec.ml b/middle_end/flambda/types/type_of_kind/variant.rec.ml index 646045cd177f..088810e20b36 100644 --- a/middle_end/flambda/types/type_of_kind/variant.rec.ml +++ b/middle_end/flambda/types/type_of_kind/variant.rec.ml @@ -17,22 +17,408 @@ [@@@ocaml.warning "+a-30-40-41-42"] module T = Type_grammar +module TEE = Typing_env_extension +module B = Row_like.For_blocks -type t = { - immediates : Type_grammar.t Or_unknown.t; - blocks : Row_like.For_blocks.t Or_unknown.t; - is_unique : bool; -} +type t = +| Immediates of { immediates : Type_grammar.t Or_unknown.t; } +| Blocks of { blocks : Row_like.For_blocks.t Or_unknown.t; is_unique : bool; } +| Either of { + immediates : Type_grammar.t Or_unknown.t; + immediates_extension : Typing_env_extension.t; + blocks : Row_like.For_blocks.t Or_unknown.t; + blocks_extension : Typing_env_extension.t; + is_unique : bool; + } + +let print_with_cache ~cache ppf t = + match t with + | Immediates { immediates; } -> + Format.fprintf ppf + "@[(tagged_imms@ %a)@]" + (Or_unknown.print (T.print_with_cache ~cache)) immediates + | Blocks { blocks; is_unique; } -> + Format.fprintf ppf + "@[(blocks%s@ %a)@]" + (if is_unique then " unique" else "") + (Or_unknown.print (B.print_with_cache ~cache)) blocks + | Either { + immediates; + immediates_extension = _; + blocks; + blocks_extension = _; + is_unique; + } -> + Format.fprintf ppf + "@[(blocks%s@ %a)@]@ \ + @[(tagged_imms@ %a)@]" + (if is_unique then " unique" else "") + (Or_unknown.print (B.print_with_cache ~cache)) blocks + (Or_unknown.print (T.print_with_cache ~cache)) immediates (* CR mshinwell: This can now return [Or_bottom.t] *) let create ~is_unique ~immediates ~blocks = - begin match immediates with - | Or_unknown.Unknown -> () - | Or_unknown.Known immediates -> - if not (K.equal (T.kind immediates) K.naked_immediate) then begin - Misc.fatal_errorf "Cannot create [immediates] with type that is not \ - of kind [Naked_immediate]:@ %a" - T.print immediates + let blocks_is_bottom = + match blocks with + | Or_unknown.Unknown -> false + | Or_unknown.Known blocks -> B.is_bottom blocks + in + let immediates_is_bottom = + match immediates with + | Or_unknown.Unknown -> false + | Or_unknown.Known immediates -> + if not (K.equal (T.kind immediates) K.naked_immediate) then begin + Misc.fatal_errorf "Cannot create [immediates] with type that is not \ + of kind [Naked_immediate]:@ %a" + T.print immediates + end; + T.is_obviously_bottom immediates + in + if blocks_is_bottom then Immediates { immediates; } + else if immediates_is_bottom then Blocks { blocks; is_unique; } + else + Either { + immediates; + immediates_extension = TEE.empty (); + blocks; + blocks_extension = TEE.empty (); + is_unique; + } + +let meet_immediates env immediates1 immediates2 extension_opt : _ Or_bottom.t = + let empty_ext () = + match extension_opt with + | None -> TEE.empty () + | Some ext -> ext + in + match (immediates1 : _ Or_unknown.t), (immediates2 : _ Or_unknown.t) with + | Unknown, _ -> Ok (immediates2, empty_ext ()) + | _, Unknown -> Ok (immediates1, empty_ext ()) + | Known immediates1, Known immediates2 -> + Or_bottom.bind (T.meet env immediates1 immediates2) + ~f:(fun (immediates, env_extension) -> + match extension_opt with + | None -> Ok (Or_unknown.Known immediates, env_extension) + | Some other_extension -> + Or_bottom.map + (TEE.meet env env_extension other_extension) + ~f:(fun env_extension -> + Or_unknown.Known immediates, env_extension)) + +let meet_blocks env blocks1 blocks2 extension_opt : _ Or_bottom.t = + let empty_ext () = + match extension_opt with + | None -> TEE.empty () + | Some ext -> ext + in + match (blocks1 : _ Or_unknown.t), (blocks2 : _ Or_unknown.t) with + | Unknown, _ -> Ok (blocks2, empty_ext ()) + | _, Unknown -> Ok (blocks1, empty_ext ()) + | Known blocks1, Known blocks2 -> + Or_bottom.bind (B.meet env blocks1 blocks2) + ~f:(fun (blocks, env_extension) -> + match extension_opt with + | None -> Ok (Or_unknown.Known blocks, env_extension) + | Some other_extension -> + Or_bottom.map + (TEE.meet env env_extension other_extension) + ~f:(fun env_extension -> + Or_unknown.Known blocks, env_extension)) + +let meet env t1 t2 : _ Or_bottom.t = + match t1, t2 with + | Immediates _, Blocks _ | Blocks _, Immediates _ -> Bottom + | Immediates { immediates = immediates1; }, + Immediates { immediates = immediates2; } -> + Or_bottom.map (meet_immediates env immediates1 immediates2 None) + ~f:(fun (immediates, env_extension) -> + Immediates { immediates; }, env_extension) + | Blocks { blocks = blocks1; is_unique = is_unique1; }, + Blocks { blocks = blocks2; is_unique = is_unique2; } -> + let is_unique = is_unique1 || is_unique2 in + Or_bottom.map (meet_blocks env blocks1 blocks2 None) + ~f:(fun (blocks, env_extension) -> + Blocks { blocks; is_unique; }, env_extension) + | Immediates { immediates = immediates1; }, + Either { immediates = immediates2; + immediates_extension = env_extension; + blocks = _; + blocks_extension = _; + is_unique = _; + } + | Either { immediates = immediates1; + immediates_extension = env_extension; + blocks = _; + blocks_extension = _; + is_unique = _; + }, + Immediates { immediates = immediates2; } -> + Or_bottom.map + (meet_immediates env immediates1 immediates2 (Some env_extension)) + ~f:(fun (immediates, env_extension) -> + Immediates { immediates; }, env_extension) + | Blocks { blocks = blocks1; is_unique = is_unique1; }, + Either { immediates = _; + immediates_extension = _; + blocks = blocks2; + blocks_extension = env_extension; + is_unique = is_unique2; + } + | Either { immediates = _; + immediates_extension = _; + blocks = blocks1; + blocks_extension = env_extension; + is_unique = is_unique1; + }, + Blocks { blocks = blocks2; is_unique = is_unique2 } -> + let is_unique = is_unique1 || is_unique2 in + Or_bottom.map (meet_blocks env blocks1 blocks2 (Some env_extension)) + ~f:(fun (blocks, env_extension) -> + Blocks { blocks; is_unique; }, env_extension) + | Either { immediates = immediates1; + immediates_extension = imms_extension1; + blocks = blocks1; + blocks_extension = blocks_extension1; + is_unique = is_unique1; + }, + Either { immediates = immediates2; + immediates_extension = imms_extension2; + blocks = blocks2; + blocks_extension = blocks_extension2; + is_unique = is_unique2; + } -> + let is_unique = is_unique1 || is_unique2 in + let immediates_res = + Or_bottom.bind (TEE.meet env imms_extension1 imms_extension2) + ~f:(fun env_extension -> + meet_immediates env immediates1 immediates2 (Some env_extension)) + in + let blocks_res = + Or_bottom.bind (TEE.meet env blocks_extension1 blocks_extension2) + ~f:(fun env_extension -> + meet_blocks env blocks1 blocks2 (Some env_extension)) + in + begin match immediates_res, blocks_res with + | Bottom, Bottom -> Bottom + | Bottom, Ok (blocks, env_extension) -> + Ok (Blocks { blocks; is_unique; }, env_extension) + | Ok (immediates, env_extension), Bottom -> + Ok (Immediates { immediates; }, env_extension) + | Ok (immediates, immediates_extension), + Ok (blocks, blocks_extension) -> + let env = Meet_env.env env in + let join_env = + Join_env.create env ~left_env:env ~right_env:env + in + Ok (Either { immediates; + immediates_extension; + blocks; + blocks_extension; + is_unique; }, + TEE.join join_env + immediates_extension blocks_extension) end - end; - { immediates; blocks; is_unique; } + +let join_immediates env immediates1 immediates2 : _ Or_unknown.t = + match (immediates1 : _ Or_unknown.t), (immediates2 : _ Or_unknown.t) with + | Unknown, _ | _, Unknown -> Unknown + | Known immediates1, Known immediates2 -> + T.join env immediates1 immediates2 + +let join_blocks env blocks1 blocks2 : _ Or_unknown.t = + match (blocks1 : _ Or_unknown.t), (blocks2 : _ Or_unknown.t) with + | Unknown, _ | _, Unknown -> Unknown + | Known blocks1, Known blocks2 -> + Known (B.join env blocks1 blocks2) + +let join env t1 t2 = + match t1, t2 with + | Immediates { immediates = immediates1; }, + Immediates { immediates = immediates2; } -> + let immediates = join_immediates env immediates1 immediates2 in + Immediates { immediates; } + | Blocks { blocks = blocks1; is_unique = is_unique1; }, + Blocks { blocks = blocks2; is_unique = is_unique2; } -> + let is_unique = is_unique1 || is_unique2 in + let blocks = join_blocks env blocks1 blocks2 in + Blocks { blocks; is_unique; } + | Immediates { immediates; }, Blocks { blocks; is_unique; } + | Blocks { blocks; is_unique; }, Immediates { immediates; } -> + (* CR vlaviron: We could actually compute extensions from the join env here. + However I expect this to be expensive, so unless we find examples where + it would make a difference, I think it's better to put empty extensions. + *) + let immediates_extension = TEE.empty () in + let blocks_extension = TEE.empty () in + Either { immediates; + immediates_extension; + blocks; + blocks_extension; + is_unique; + } + | Immediates { immediates = immediates1; }, + Either { immediates = immediates2; + immediates_extension = _; + blocks; + blocks_extension; + is_unique; + } + | Either { immediates = immediates1; + immediates_extension = _; + blocks; + blocks_extension; + is_unique; + }, + Immediates { immediates = immediates2; } -> + let immediates = join_immediates env immediates1 immediates2 in + (* See CR above about extensions *) + let immediates_extension = TEE.empty () in + Either { immediates; + immediates_extension; + blocks; + blocks_extension; + is_unique; + } + | Blocks { blocks = blocks1; is_unique = is_unique1; }, + Either { immediates; + immediates_extension; + blocks = blocks2; + blocks_extension = _; + is_unique = is_unique2; + } + | Either { immediates; + immediates_extension; + blocks = blocks1; + blocks_extension = _; + is_unique = is_unique1; + }, + Blocks { blocks = blocks2; is_unique = is_unique2 } -> + let is_unique = is_unique1 || is_unique2 in + let blocks = join_blocks env blocks1 blocks2 in + (* See CR above about extensions *) + let blocks_extension = TEE.empty () in + Either { immediates; + immediates_extension; + blocks; + blocks_extension; + is_unique; + } + | Either { immediates = immediates1; + immediates_extension = imms_extension1; + blocks = blocks1; + blocks_extension = blocks_extension1; + is_unique = is_unique1; + }, + Either { immediates = immediates2; + immediates_extension = imms_extension2; + blocks = blocks2; + blocks_extension = blocks_extension2; + is_unique = is_unique2; + } -> + let is_unique = is_unique1 || is_unique2 in + let immediates = join_immediates env immediates1 immediates2 in + let blocks = join_blocks env blocks1 blocks2 in + let immediates_extension = + TEE.join env imms_extension1 imms_extension2 + in + let blocks_extension = + TEE.join env blocks_extension1 blocks_extension2 + in + Either { immediates; + immediates_extension; + blocks; + blocks_extension; + is_unique; + } + +let apply_renaming t perm = + match t with + | Immediates { immediates; } -> + let immediates' = + Or_unknown.map_sharing immediates ~f:(fun immediates -> + T.apply_renaming immediates perm) + in + if immediates == immediates' then t + else Immediates { immediates = immediates'; } + | Blocks { blocks; is_unique; } -> + let blocks' = + Or_unknown.map_sharing blocks ~f:(fun blocks -> + B.apply_renaming blocks perm) + in + if blocks == blocks' then t + else Blocks { blocks = blocks'; is_unique; } + | Either { + immediates; + immediates_extension; + blocks; + blocks_extension; + is_unique; + } -> + let immediates' = + Or_unknown.map_sharing immediates ~f:(fun immediates -> + T.apply_renaming immediates perm) + in + let blocks' = + Or_unknown.map_sharing blocks ~f:(fun blocks -> + B.apply_renaming blocks perm) + in + let immediates_extension' = + TEE.apply_renaming immediates_extension perm + in + let blocks_extension' = + TEE.apply_renaming blocks_extension perm + in + if immediates == immediates' + && blocks == blocks' + && immediates_extension == immediates_extension' + && blocks_extension == blocks_extension' + then t + else Either { + immediates = immediates'; + immediates_extension = immediates_extension'; + blocks = blocks'; + blocks_extension = blocks_extension'; + is_unique; + } + +let free_names t = + match t with + | Immediates { immediates; } -> + Or_unknown.free_names T.free_names immediates + | Blocks { blocks; is_unique = _; } -> + Or_unknown.free_names B.free_names blocks + | Either { + immediates; + immediates_extension; + blocks; + blocks_extension; + is_unique = _; + } -> + Name_occurrences.union + (Name_occurrences.union + (Or_unknown.free_names B.free_names blocks) + (Or_unknown.free_names T.free_names immediates)) + (Name_occurrences.union + (TEE.free_names immediates_extension) + (TEE.free_names blocks_extension)) + +let all_ids_for_export t = + match t with + | Immediates { immediates; } -> + Or_unknown.all_ids_for_export T.all_ids_for_export immediates + | Blocks { blocks; is_unique = _; } -> + Or_unknown.all_ids_for_export B.all_ids_for_export blocks + | Either { + immediates; + immediates_extension; + blocks; + blocks_extension; + is_unique = _; + } -> + Ids_for_export.union + (Ids_for_export.union + (Or_unknown.all_ids_for_export B.all_ids_for_export blocks) + (Or_unknown.all_ids_for_export T.all_ids_for_export immediates)) + (Ids_for_export.union + (TEE.all_ids_for_export immediates_extension) + (TEE.all_ids_for_export blocks_extension)) diff --git a/middle_end/flambda/types/type_of_kind/variant.rec.mli b/middle_end/flambda/types/type_of_kind/variant.rec.mli index e51b7a05c23d..292d203ee1b0 100644 --- a/middle_end/flambda/types/type_of_kind/variant.rec.mli +++ b/middle_end/flambda/types/type_of_kind/variant.rec.mli @@ -16,14 +16,28 @@ [@@@ocaml.warning "+a-30-40-41-42"] -type t = private { - immediates : Type_grammar.t Or_unknown.t; - blocks : Row_like.For_blocks.t Or_unknown.t; - is_unique : bool; -} +type t = private +| Immediates of { immediates : Type_grammar.t Or_unknown.t; } +| Blocks of { blocks : Row_like.For_blocks.t Or_unknown.t; is_unique : bool; } +| Either of { + immediates : Type_grammar.t Or_unknown.t; + immediates_extension : Typing_env_extension.t; + blocks : Row_like.For_blocks.t Or_unknown.t; + blocks_extension : Typing_env_extension.t; + is_unique : bool; + } + +include Contains_names.S with type t := t +include Contains_ids.S with type t := t val create : is_unique:bool -> immediates:Type_grammar.t Or_unknown.t -> blocks:Row_like.For_blocks.t Or_unknown.t -> t + +val meet : Meet_env.t -> t -> t -> (t * Typing_env_extension.t) Or_bottom.t + +val join : Join_env.t -> t -> t -> t + +val print_with_cache : cache:Printing_cache.t -> Format.formatter -> t -> unit