diff --git a/typing/.ocamlformat b/typing/.ocamlformat new file mode 100644 index 00000000000..3c4cb177b69 --- /dev/null +++ b/typing/.ocamlformat @@ -0,0 +1,21 @@ +# Please make a pull request to change this file. +disable=true +# There is an .ocamlformat-enable file in this directory. +# Keep the remainder of this file in sync with other .ocamlformat files in this repo. +assignment-operator=begin-line +cases-exp-indent=2 +doc-comments=before +dock-collection-brackets=false +if-then-else=keyword-first +module-item-spacing=sparse +parens-tuple=multi-line-only +sequence-blank-line=compact +space-around-lists=false +space-around-variants=false +type-decl=sparse +version=0.24.1 + +# The existing comments are hand-formatted and lose a lot of readability +# if we wrap them. We should either convert the comments we care about to +# doc comments, or make this same setting change everywhere. +wrap-comments=false diff --git a/typing/.ocamlformat-enable b/typing/.ocamlformat-enable new file mode 100644 index 00000000000..a11192df5a8 --- /dev/null +++ b/typing/.ocamlformat-enable @@ -0,0 +1,6 @@ +jkind.ml +jkind.mli +mode.ml +mode.mli +uniqueness_analysis.ml +uniqueness_analysis.mli diff --git a/typing/jkind.ml b/typing/jkind.ml index 0373233e697..68f2faa2f5c 100644 --- a/typing/jkind.ml +++ b/typing/jkind.ml @@ -28,31 +28,31 @@ module Sort = struct type t = | Var of var | Const of const + and var = t option ref let var_name : var -> string = let next_id = ref 1 in let named = ref [] in fun v -> - match List.assq_opt v (!named) with + match List.assq_opt v !named with | Some name -> name | None -> - let id = !next_id in - let name = "'_representable_layout_" ^ Int.to_string id in - next_id := id + 1; - named := (v, name) :: !named; - name + let id = !next_id in + let name = "'_representable_layout_" ^ Int.to_string id in + next_id := id + 1; + named := (v, name) :: !named; + name let void = Const Void + let value = Const Value + let float64 = Const Float64 let some_value = Some value - let of_const = function - | Void -> void - | Value -> value - | Float64 -> float64 + let of_const = function Void -> void | Value -> value | Float64 -> float64 let of_var v = Var v @@ -61,17 +61,19 @@ module Sort = struct (* Post-condition: If the result is a [Var v], then [!v] is [None]. *) let rec get : t -> t = function | Const _ as t -> t - | Var r as t -> begin match !r with + | Var r as t -> ( + match !r with | None -> t - | Some s -> begin - let result = get s in - if result != s then r := Some result; (* path compression *) - result - end - end + | Some s -> + let result = get s in + if result != s then r := Some result; + (* path compression *) + result) let default_value : t option = Some (Const Value) + let default_void : t option = Some (Const Void) + let default_float64 : t option = Some (Const Float64) let[@inline] default = function @@ -81,14 +83,16 @@ module Sort = struct let rec get_default_value : t -> const = function | Const c -> c - | Var r -> begin match !r with - | None -> r := default_value; Value - | Some s -> begin - let result = get_default_value s in - r := default result; (* path compression *) - result - end - end + | Var r -> ( + match !r with + | None -> + r := default_value; + Value + | Some s -> + let result = get_default_value s in + r := default result; + (* path compression *) + result) let default_to_value t = ignore (get_default_value t) @@ -106,59 +110,66 @@ module Sort = struct | Equal_mutated_second -> Equal_mutated_first | (Unequal | Equal_no_mutation) as r -> r - let equal_const_const c1 c2 = match c1, c2 with - | Void, Void - | Value, Value - | Float64, Float64 -> Equal_no_mutation + let equal_const_const c1 c2 = + match c1, c2 with + | Void, Void | Value, Value | Float64, Float64 -> Equal_no_mutation | (Void | Value | Float64), _ -> Unequal - let rec equate_var_const v1 c2 = match !v1 with + let rec equate_var_const v1 c2 = + match !v1 with | Some s1 -> equate_sort_const s1 c2 - | None -> v1 := Some (of_const c2); Equal_mutated_first + | None -> + v1 := Some (of_const c2); + Equal_mutated_first - and equate_var v1 s2 = match s2 with + and equate_var v1 s2 = + match s2 with | Const c2 -> equate_var_const v1 c2 | Var v2 -> equate_var_var v1 v2 and equate_var_var v1 v2 = - if v1 == v2 then - Equal_no_mutation - else begin + if v1 == v2 + then Equal_no_mutation + else match !v1, !v2 with | Some s1, _ -> swap_equate_result (equate_var v2 s1) | _, Some s2 -> equate_var v1 s2 - | None, None -> v1 := Some (of_var v2); Equal_mutated_first - end + | None, None -> + v1 := Some (of_var v2); + Equal_mutated_first - and equate_sort_const s1 c2 = match s1 with + and equate_sort_const s1 c2 = + match s1 with | Const c1 -> equal_const_const c1 c2 | Var v1 -> equate_var_const v1 c2 - let equate_tracking_mutation s1 s2 = match s1 with + let equate_tracking_mutation s1 s2 = + match s1 with | Const c1 -> swap_equate_result (equate_sort_const s2 c1) | Var v1 -> equate_var v1 s2 (* Don't expose whether or not mutation happened; we just need that for [Jkind] *) - let equate s1 s2 = match equate_tracking_mutation s1 s2 with + let equate s1 s2 = + match equate_tracking_mutation s1 s2 with | Unequal -> false | Equal_mutated_first | Equal_mutated_second | Equal_no_mutation -> true let equal_const c1 c2 = match c1, c2 with - | Void, Void - | Value, Value - | Float64, Float64 -> true - | Void, (Value | Float64) - | Value, (Void | Float64) - | Float64, (Value | Void) -> false + | Void, Void | Value, Value | Float64, Float64 -> true + | Void, (Value | Float64) | Value, (Void | Float64) | Float64, (Value | Void) + -> + false let rec is_void_defaulting = function | Const Void -> true - | Var v -> begin match !v with + | Var v -> ( + match !v with (* CR layouts v5: this should probably default to void now *) - | None -> v := some_value; false - | Some s -> is_void_defaulting s - end + | None -> + v := some_value; + false + | Some s -> is_void_defaulting s) | Const Value -> false | Const Float64 -> false @@ -169,9 +180,8 @@ module Sort = struct | Void -> "void" | Float64 -> "float64" - let to_string s = match get s with - | Var v -> var_name v - | Const c -> string_of_const c + let to_string s = + match get s with Var v -> var_name v | Const c -> string_of_const c let format ppf t = Format.fprintf ppf "%s" (to_string t) @@ -181,38 +191,57 @@ module Sort = struct open Format let rec t ppf = function - | Var v -> fprintf ppf "Var %a" var v - | Const c -> fprintf ppf (match c with - | Void -> "Void" - | Value -> "Value" - | Float64 -> "Float64") - + | Var v -> fprintf ppf "Var %a" var v + | Const c -> + fprintf ppf + (match c with + | Void -> "Void" + | Value -> "Value" + | Float64 -> "Float64") and opt_t ppf = function | Some s -> fprintf ppf "Some %a" t s - | None -> fprintf ppf "None" + | None -> fprintf ppf "None" - and var ppf v = fprintf ppf "{ contents = %a }" opt_t (!v) + and var ppf v = fprintf ppf "{ contents = %a }" opt_t !v end let for_function = value + let for_predef_value = value + let for_block_element = value + let for_probe_body = value + let for_poly_variant = value + let for_record = value + let for_constructor_arg = value + let for_object = value + let for_lazy_body = value + let for_tuple_element = value + let for_instance_var = value + let for_class_arg = value + let for_method = value + let for_initializer = value + let for_module = value + let for_tuple = value + let for_array_get_result = value + let for_array_element = value + let for_list_element = value end @@ -284,8 +313,7 @@ type immediate64_creation_reason = | Gc_ignorable_check | Separability_check -type void_creation_reason = - | V1_safety_check +type void_creation_reason = V1_safety_check type any_creation_reason = | Missing_cmi of Path.t @@ -295,8 +323,7 @@ type any_creation_reason = | Dummy_jkind | Type_expression_call -type float64_creation_reason = - | Primitive of Ident.t +type float64_creation_reason = Primitive of Ident.t type annotation_context = | Type_declaration of Path.t @@ -308,7 +335,6 @@ type annotation_context = | Type_variable of string | Type_wildcard of Location.t - type creation_reason = | Annotated of annotation_context * Location.t | Value_creation of value_creation_reason @@ -332,7 +358,7 @@ type internal = | Any | Sort of sort | Immediate64 - (** We know for sure that values of types of this jkind are always immediate + (** We know for sure that values of types of this jkind are always immediate on 64-bit platforms. For other platforms, we know nothing about immediacy. *) | Immediate @@ -344,17 +370,19 @@ type internal = jkinds. *) type history = - | Interact of { reason : interact_reason - ; lhs_jkind : internal - ; lhs_history : history - ; rhs_jkind : internal - ; rhs_history : history - } + | Interact of + { reason : interact_reason; + lhs_jkind : internal; + lhs_history : history; + rhs_jkind : internal; + rhs_history : history + } | Creation of creation_reason type t = - { jkind : internal - ; history : history } + { jkind : internal; + history : history + } let fresh_jkind jkind ~why = { jkind; history = Creation why } @@ -363,24 +391,29 @@ let fresh_jkind jkind ~why = { jkind; history = Creation why } let any_dummy_jkind = { jkind = Any; history = Creation (Any_creation Dummy_jkind) } + let value_v1_safety_check = { jkind = Sort Sort.value; - history = Creation (Value_creation V1_safety_check) } + history = Creation (Value_creation V1_safety_check) + } -let any ~why = match why with - | Dummy_jkind -> any_dummy_jkind (* share this one common case *) +let any ~why = + match why with + | Dummy_jkind -> any_dummy_jkind (* share this one common case *) | _ -> fresh_jkind Any ~why:(Any_creation why) -let void ~why = - fresh_jkind (Sort Sort.void) ~why:(Void_creation why) -let value ~(why : value_creation_reason) = match why with + +let void ~why = fresh_jkind (Sort Sort.void) ~why:(Void_creation why) + +let value ~(why : value_creation_reason) = + match why with | V1_safety_check -> value_v1_safety_check | _ -> fresh_jkind (Sort Sort.value) ~why:(Value_creation why) -let immediate64 ~why = - fresh_jkind Immediate64 ~why:(Immediate64_creation why) -let immediate ~why = - fresh_jkind Immediate ~why:(Immediate_creation why) -let float64 ~why = - fresh_jkind (Sort Sort.float64) ~why:(Float64_creation why) + +let immediate64 ~why = fresh_jkind Immediate64 ~why:(Immediate64_creation why) + +let immediate ~why = fresh_jkind Immediate ~why:(Immediate_creation why) + +let float64 ~why = fresh_jkind (Sort Sort.float64) ~why:(Float64_creation why) type const = Jane_asttypes.const_jkind = | Any @@ -398,7 +431,8 @@ let string_of_const : const -> _ = function | Immediate -> "immediate" | Float64 -> "float64" -let equal_const (c1 : const) (c2 : const) = match c1, c2 with +let equal_const (c1 : const) (c2 : const) = + match c1, c2 with | Any, Any -> true | Immediate64, Immediate64 -> true | Immediate, Immediate -> true @@ -407,7 +441,8 @@ let equal_const (c1 : const) (c2 : const) = match c1, c2 with | Float64, Float64 -> true | (Any | Immediate64 | Immediate | Void | Value | Float64), _ -> false -let sub_const (c1 : const) (c2 : const) = match c1, c2 with +let sub_const (c1 : const) (c2 : const) = + match c1, c2 with | Any, Any -> Equal | _, Any -> Sub | c1, c2 when equal_const c1 c2 -> Equal @@ -422,12 +457,11 @@ type error = exception User_error of Location.t * error -let raise ~loc err = raise (User_error(loc, err)) +let raise ~loc err = raise (User_error (loc, err)) (*** extension requirements ***) -let get_required_layouts_level - (context : annotation_context) (jkind : const) : - Language_extension.maturity = +let get_required_layouts_level (context : annotation_context) (jkind : const) : + Language_extension.maturity = match context, jkind with | _, Value -> Stable | _, (Immediate | Immediate64 | Any | Float64) -> Beta @@ -439,8 +473,7 @@ let get_required_layouts_level let of_new_sort_var ~why = fresh_jkind (Sort (Sort.new_var ())) ~why:(Concrete_creation why) -let of_sort ~why s = - fresh_jkind (Sort s) ~why:(Concrete_creation why) +let of_sort ~why s = fresh_jkind (Sort s) ~why:(Concrete_creation why) let of_const ~why : const -> t = function | Any -> fresh_jkind Any ~why @@ -451,14 +484,14 @@ let of_const ~why : const -> t = function | Float64 -> fresh_jkind (Sort Sort.float64) ~why (* CR layouts v1.5: remove legacy_immediate *) -let of_annotation ?(legacy_immediate=false) ~context Location.{ loc; txt = const } = - begin match const with - | Immediate | Immediate64 | Value when legacy_immediate -> () +let of_annotation ?(legacy_immediate = false) ~context + Location.{ loc; txt = const } = + (match const with + | (Immediate | Immediate64 | Value) when legacy_immediate -> () | _ -> let required_layouts_level = get_required_layouts_level context const in if not (Language_extension.is_at_least Layouts required_layouts_level) - then raise ~loc (Insufficient_level (context, const)) - end; + then raise ~loc (Insufficient_level (context, const))); of_const ~why:(Annotated (context, loc)) const let of_annotation_option ?legacy_immediate ~context = @@ -468,12 +501,13 @@ let of_annotation_option_default ?legacy_immediate ~default ~context = Option.fold ~none:default ~some:(of_annotation ?legacy_immediate ~context) let of_attributes ~legacy_immediate ~context attrs = - Builtin_attributes.jkind ~legacy_immediate attrs |> - Result.map (of_annotation_option ~legacy_immediate ~context) + Builtin_attributes.jkind ~legacy_immediate attrs + |> Result.map (of_annotation_option ~legacy_immediate ~context) let of_attributes_default ~legacy_immediate ~context ~default attrs = - Builtin_attributes.jkind ~legacy_immediate attrs |> - Result.map (of_annotation_option_default ~legacy_immediate ~default ~context) + Builtin_attributes.jkind ~legacy_immediate attrs + |> Result.map + (of_annotation_option_default ~legacy_immediate ~default ~context) let for_boxed_record ~all_void = if all_void then immediate ~why:Empty_record else value ~why:Boxed_record @@ -488,43 +522,48 @@ type desc = | Const of const | Var of Sort.var -let format_desc ppf = let open Format in function +let format_desc ppf = + let open Format in + function | Const c -> fprintf ppf "%s" (string_of_const c) | Var v -> fprintf ppf "%s" (Sort.var_name v) (* considers sort variables < Any, but otherwise just checks for equality. Never does mutation. Pre-condition: no filled-in sort variables. *) -let sub_desc d1 d2 = match d1, d2 with +let sub_desc d1 d2 = + match d1, d2 with | Const c1, Const c2 -> sub_const c1 c2 | Var _, Const Any -> Sub | Var v1, Var v2 -> if v1 == v2 then Equal else Not_sub | Const _, Var _ | Var _, Const _ -> Not_sub (* Post-condition: If the result is [Var v], then [!v] is [None]. *) -let get_internal (lay : internal) : desc = match lay with +let get_internal (lay : internal) : desc = + match lay with | Any -> Const Any | Immediate -> Const Immediate | Immediate64 -> Const Immediate64 - | Sort s -> begin match Sort.get s with + | Sort s -> ( + match Sort.get s with (* NB: this match isn't as silly as it looks: those are different constructors on the left than on the right *) | Const Void -> Const Void | Const Value -> Const Value | Const Float64 -> Const Float64 - | Var v -> Var v - end + | Var v -> Var v) -let get_default_value (t : t) : const = match t.jkind with +let get_default_value (t : t) : const = + match t.jkind with | Any -> Any | Immediate -> Immediate | Immediate64 -> Immediate64 - | Sort s -> begin match Sort.get_default_value s with + | Sort s -> ( + match Sort.get_default_value s with (* As above, this turns Sort.consts to Jkind.consts *) | Value -> Value | Void -> Void - | Float64 -> Float64 - end + | Float64 -> Float64) let default_to_value t = ignore (get_default_value t) @@ -543,9 +582,8 @@ let sort_of_jkind l = (*********************************) (* pretty printing *) -let to_string lay = match get lay with - | Const c -> string_of_const c - | Var v -> Sort.var_name v +let to_string lay = + match get lay with Const c -> string_of_const c | Var v -> Sort.var_name v let format ppf t = Format.fprintf ppf "%s" (to_string t) @@ -553,6 +591,7 @@ let format ppf t = Format.fprintf ppf "%s" (to_string t) (* jkind histories *) let printtyp_path = ref (fun _ _ -> assert false) + let set_printtyp_path f = printtyp_path := f module Report_missing_cmi : sig @@ -574,15 +613,13 @@ end = struct with a missing .cmi file; definitely less likely to be right outside of Jane Street. *) let guess_library_name : Path.t -> string option = function - | Pdot _ as p -> Some begin - match root_module_name p with + | Pdot _ as p -> + Some + (match root_module_name p with | "Location" | "Longident" -> "ocamlcommon" - | mn -> mn - |> String.lowercase_ascii - |> delete_trailing_double_underscore - end - | Pident _ | Papply _ -> - None + | mn -> + mn |> String.lowercase_ascii |> delete_trailing_double_underscore) + | Pident _ | Papply _ -> None in Option.iter (fprintf ppf "@,Hint: Adding \"%s\" to your dependencies might help.") @@ -621,8 +658,7 @@ end = struct let format_concrete_jkind_reason ppf : concrete_jkind_reason -> unit = function - | Match -> - fprintf ppf "matched on" + | Match -> fprintf ppf "matched on" | Constructor_declaration idx -> fprintf ppf "used as constructor field %d" idx | Label_declaration lbl -> @@ -630,92 +666,73 @@ end = struct Ident.print lbl | Unannotated_type_parameter -> fprintf ppf "appears as an unannotated type parameter" - | Record_projection -> - fprintf ppf "used as the record in a projection" - | Record_assignment -> - fprintf ppf "used as the record in an assignment" - | Let_binding -> - fprintf ppf "bound by a `let`" - | Function_argument -> - fprintf ppf "used as a function argument" - | Function_result -> - fprintf ppf "used as a function result" + | Record_projection -> fprintf ppf "used as the record in a projection" + | Record_assignment -> fprintf ppf "used as the record in an assignment" + | Let_binding -> fprintf ppf "bound by a `let`" + | Function_argument -> fprintf ppf "used as a function argument" + | Function_result -> fprintf ppf "used as a function result" | Structure_item_expression -> fprintf ppf "used in an expression in a structure" - | V1_safety_check -> - fprintf ppf "part of the v1 safety check" + | V1_safety_check -> fprintf ppf "part of the v1 safety check" | External_argument -> fprintf ppf "used as an argument in an external declaration" | External_result -> fprintf ppf "used as the result of an external declaration" - | Statement -> - fprintf ppf "used as a statement" + | Statement -> fprintf ppf "used as a statement" let format_annotation_context ppf : annotation_context -> unit = function | Type_declaration p -> - fprintf ppf "the declaration of the type %a" - !printtyp_path p + fprintf ppf "the declaration of the type %a" !printtyp_path p | Type_parameter (path, var) -> - let var_string = match var with None -> "_" | Some v -> "'" ^ v in - fprintf ppf "@[%s@ in the declaration of the type@ %a@]" - var_string - !printtyp_path path - | With_constraint s -> - fprintf ppf "the `with` constraint for %s" s + let var_string = match var with None -> "_" | Some v -> "'" ^ v in + fprintf ppf "@[%s@ in the declaration of the type@ %a@]" var_string + !printtyp_path path + | With_constraint s -> fprintf ppf "the `with` constraint for %s" s | Newtype_declaration name -> - fprintf ppf "the abstract type declaration for %s" - name + fprintf ppf "the abstract type declaration for %s" name | Constructor_type_parameter (cstr, name) -> - fprintf ppf "@[%s@ in the declaration of constructor@ %a@]" - name - !printtyp_path cstr - | Univar name -> - fprintf ppf "the universal variable %s" - name - | Type_variable name -> - fprintf ppf "the type variable %s" name + fprintf ppf "@[%s@ in the declaration of constructor@ %a@]" name + !printtyp_path cstr + | Univar name -> fprintf ppf "the universal variable %s" name + | Type_variable name -> fprintf ppf "the type variable %s" name | Type_wildcard loc -> - fprintf ppf "the wildcard _ at %a" Location.print_loc loc + fprintf ppf "the wildcard _ at %a" Location.print_loc loc let format_any_creation_reason ppf : any_creation_reason -> unit = function - | Missing_cmi p -> - fprintf ppf "a missing .cmi file for %a" !printtyp_path p - | Wildcard -> - fprintf ppf "a _ in a type" - | Unification_var -> - fprintf ppf "a fresh unification variable" + | Missing_cmi p -> fprintf ppf "a missing .cmi file for %a" !printtyp_path p + | Wildcard -> fprintf ppf "a _ in a type" + | Unification_var -> fprintf ppf "a fresh unification variable" | Initial_typedecl_env -> - fprintf ppf "a dummy layout used in checking mutually recursive datatypes" + fprintf ppf "a dummy layout used in checking mutually recursive datatypes" | Dummy_jkind -> - fprintf ppf "@[a dummy layout that should have been overwritten;@ \ - Please notify the Jane Street compilers group if you see this output." + fprintf ppf + "@[a dummy layout that should have been overwritten;@ Please notify \ + the Jane Street compilers group if you see this output." (* CR layouts: Improve output or remove this constructor ^^ *) | Type_expression_call -> - fprintf ppf "a call to [type_expression] via the ocaml API" + fprintf ppf "a call to [type_expression] via the ocaml API" let format_immediate_creation_reason ppf : immediate_creation_reason -> _ = function - | Empty_record -> - fprintf ppf "a record containing all void elements" + | Empty_record -> fprintf ppf "a record containing all void elements" | Enumeration -> - fprintf ppf "an enumeration variant (all constructors are constant)" + fprintf ppf "an enumeration variant (all constructors are constant)" | Primitive id -> - fprintf ppf "it equals the primitive immediate type %s" (Ident.name id) + fprintf ppf "it equals the primitive immediate type %s" (Ident.name id) | Immediate_polymorphic_variant -> - fprintf ppf "an immediate polymorphic variant" + fprintf ppf "an immediate polymorphic variant" | Gc_ignorable_check -> - fprintf ppf "the check to see whether a value can be ignored by GC" + fprintf ppf "the check to see whether a value can be ignored by GC" | Value_kind -> - fprintf ppf - "the check to see whether a polymorphic variant is immediate" + fprintf ppf "the check to see whether a polymorphic variant is immediate" let format_immediate64_creation_reason ppf = function | Local_mode_cross_check -> - fprintf ppf "the check for whether a local value can safely escape" + fprintf ppf "the check for whether a local value can safely escape" | Gc_ignorable_check -> - fprintf ppf "the check to see whether a value can be ignored by GC" + fprintf ppf "the check to see whether a value can be ignored by GC" | Separability_check -> - fprintf ppf "the check that a type is definitely not `float`" + fprintf ppf "the check that a type is definitely not `float`" let format_value_creation_reason ppf : value_creation_reason -> _ = function | Class_let_binding -> fprintf ppf "let-bound in a class expression" @@ -731,7 +748,8 @@ end = struct | Extensible_variant -> fprintf ppf "an extensible variant" | Primitive id -> fprintf ppf "it equals the primitive value type %s" (Ident.name id) - | Type_argument -> fprintf ppf "a type argument defaulted to have layout value" + | Type_argument -> + fprintf ppf "a type argument defaulted to have layout value" | Tuple -> fprintf ppf "a tuple type" | Row_variable -> fprintf ppf "a row variable" | Polymorphic_variant -> fprintf ppf "a polymorphic variant" @@ -742,65 +760,55 @@ end = struct | Separability_check -> fprintf ppf "the check that a type is definitely not `float`" | Univar -> fprintf ppf "an unannotated universal variable" - | Polymorphic_variant_field -> fprintf ppf "a field of a polymorphic variant" + | Polymorphic_variant_field -> + fprintf ppf "a field of a polymorphic variant" | Default_type_jkind -> fprintf ppf "the default layout for an abstract type" - | Float_record_field -> - fprintf ppf "a field of a float record" + | Float_record_field -> fprintf ppf "a field of a float record" | Existential_type_variable -> fprintf ppf "an unannotated existential type variable" - | Array_element -> - fprintf ppf "an array element" - | Lazy_expression -> - fprintf ppf "a lazy expression" + | Array_element -> fprintf ppf "an array element" + | Lazy_expression -> fprintf ppf "a lazy expression" | Class_argument -> fprintf ppf "a term-level argument to a class constructor" - | Structure_element -> - fprintf ppf "stored in a module structure" + | Structure_element -> fprintf ppf "stored in a module structure" | Debug_printer_argument -> - fprintf ppf "used as the argument to a debugger printer function" - | V1_safety_check -> - fprintf ppf "to be value for the V1 safety check" + fprintf ppf "used as the argument to a debugger printer function" + | V1_safety_check -> fprintf ppf "to be value for the V1 safety check" | Captured_in_object -> fprintf ppf "captured in an object" - | Unknown s -> fprintf ppf "unknown @[(please alert the Jane Street@;\ - compilers team with this message: %s)@]" s - + | Unknown s -> + fprintf ppf + "unknown @[(please alert the Jane Street@;\ + compilers team with this message: %s)@]" s let format_void_creation_reason ppf : void_creation_reason -> _ = function | V1_safety_check -> fprintf ppf "check to make sure there are no voids" - (* CR layouts: remove this when we remove its uses *) + (* CR layouts: remove this when we remove its uses *) - let format_float64_creation_reason ppf : float64_creation_reason -> _ = function + let format_float64_creation_reason ppf : float64_creation_reason -> _ = + function | Primitive id -> fprintf ppf "it equals the primitive value type %s" (Ident.name id) let format_creation_reason ppf : creation_reason -> unit = function | Annotated (ctx, _) -> - fprintf ppf "of the annotation on %a" format_annotation_context ctx - | Any_creation any -> - format_any_creation_reason ppf any + fprintf ppf "of the annotation on %a" format_annotation_context ctx + | Any_creation any -> format_any_creation_reason ppf any | Immediate_creation immediate -> - format_immediate_creation_reason ppf immediate + format_immediate_creation_reason ppf immediate | Immediate64_creation immediate64 -> - format_immediate64_creation_reason ppf immediate64 - | Void_creation void -> - format_void_creation_reason ppf void - | Value_creation value -> - format_value_creation_reason ppf value - | Float64_creation float -> - format_float64_creation_reason ppf float - | Concrete_creation concrete -> - format_concrete_jkind_reason ppf concrete - | Imported -> - fprintf ppf "imported from another compilation unit" + format_immediate64_creation_reason ppf immediate64 + | Void_creation void -> format_void_creation_reason ppf void + | Value_creation value -> format_value_creation_reason ppf value + | Float64_creation float -> format_float64_creation_reason ppf float + | Concrete_creation concrete -> format_concrete_jkind_reason ppf concrete + | Imported -> fprintf ppf "imported from another compilation unit" let format_interact_reason ppf = function | Gadt_equation name -> fprintf ppf "a GADT match on the constructor %a" !printtyp_path name - | Tyvar_refinement_intersection -> - fprintf ppf "updating a type variable" - | Subjkind -> - fprintf ppf "sublayout check" + | Tyvar_refinement_intersection -> fprintf ppf "updating a type variable" + | Subjkind -> fprintf ppf "sublayout check" (* a flattened_history describes the history of a jkind L. That jkind has been constrained to be a subjkind of jkinds L1..Ln. @@ -826,6 +834,7 @@ end = struct This type could be more efficient in several ways, but there is little incentive to do so. *) type flattened_row = desc * creation_reason list + type flattened_history = flattened_row list (* first arg is the jkind L whose history we are flattening *) @@ -833,70 +842,62 @@ end = struct let add jkind reason = let jkind_desc = get_internal jkind in let rec go acc = function - | ((key, value) as row) :: rest -> - begin match sub_desc jkind_desc key with + | ((key, value) as row) :: rest -> ( + match sub_desc jkind_desc key with | Sub -> go acc rest - | Equal -> (key, reason :: value) :: acc @ rest - | Not_sub -> go (row :: acc) rest - end + | Equal -> ((key, reason :: value) :: acc) @ rest + | Not_sub -> go (row :: acc) rest) | [] -> (jkind_desc, [reason]) :: acc in go [] in let rec history acc internal = function - | Interact { reason = _ - ; lhs_jkind - ; lhs_history - ; rhs_jkind - ; rhs_history } -> + | Interact { reason = _; lhs_jkind; lhs_history; rhs_jkind; rhs_history } + -> let fh1 = history acc lhs_jkind lhs_history in let fh2 = history fh1 rhs_jkind rhs_history in fh2 - | Creation reason -> - add internal reason acc + | Creation reason -> add internal reason acc in - fun internal hist -> - history [] internal hist + fun internal hist -> history [] internal hist let format_flattened_row ppf (lay, reasons) = fprintf ppf "%a, because" format_desc lay; match reasons with | [reason] -> fprintf ppf "@ %a." format_creation_reason reason | _ -> - fprintf ppf " all of the following:@ @[ %a@]" - (pp_print_list format_creation_reason) reasons + fprintf ppf " all of the following:@ @[ %a@]" + (pp_print_list format_creation_reason) + reasons let format_flattened_history ~intro ppf t = let fh = flatten_history t.jkind t.history in fprintf ppf "@[%t " intro; - begin match fh with + (match fh with | [row] -> format_flattened_row ppf row - | _ -> fprintf ppf "a sublayout of all of the following:@ @[ %a@]" - (pp_print_list format_flattened_row) fh - end; + | _ -> + fprintf ppf "a sublayout of all of the following:@ @[ %a@]" + (pp_print_list format_flattened_row) + fh); fprintf ppf "@]@;" (* this isn't really formatted for user consumption *) let format_history_tree ~intro ppf t = let rec in_order ppf = function | Interact { reason; lhs_history; rhs_history } -> - fprintf ppf "@[ %a@]@;%a@ @[ %a@]" - in_order lhs_history - format_interact_reason reason - in_order rhs_history - | Creation c -> - format_creation_reason ppf c + fprintf ppf "@[ %a@]@;%a@ @[ %a@]" in_order lhs_history + format_interact_reason reason in_order rhs_history + | Creation c -> format_creation_reason ppf c in - fprintf ppf "@;%t has this layout history:@;@[ %a@]" - intro - in_order t.history + fprintf ppf "@;%t has this layout history:@;@[ %a@]" intro in_order + t.history let format_history ~intro ppf t = - if display_histories then begin + if display_histories + then if flattened_histories then format_flattened_history ~intro ppf t else format_history_tree ~intro ppf t - end end include Format_history @@ -911,71 +912,81 @@ module Violation = struct | Not_a_subjkind of t * t | No_intersection of t * t - type nonrec t = { violation : violation - ; missing_cmi : Path.t option } - (* [missing_cmi]: is this error a result of a missing cmi file? - This is stored separately from the [violation] because it's - used to change the behavior of [value_kind], and we don't - want that function to inspect something that is purely about - the choice of error message. (Though the [Path.t] payload *is* - indeed just about the payload.) *) + type nonrec t = + { violation : violation; + missing_cmi : Path.t option + } + (* [missing_cmi]: is this error a result of a missing cmi file? + This is stored separately from the [violation] because it's + used to change the behavior of [value_kind], and we don't + want that function to inspect something that is purely about + the choice of error message. (Though the [Path.t] payload *is* + indeed just about the payload.) *) let of_ violation = { violation; missing_cmi = None } - let record_missing_cmi ~missing_cmi_for t = { t with missing_cmi = Some missing_cmi_for } + let record_missing_cmi ~missing_cmi_for t = + { t with missing_cmi = Some missing_cmi_for } let is_missing_cmi { missing_cmi } = Option.is_some missing_cmi let report_general preamble pp_former former ppf t = - let subjkind_format verb l2 = match get l2 with + let subjkind_format verb l2 = + match get l2 with | Var _ -> dprintf "%s representable" verb | Const _ -> dprintf "%s a sublayout of %a" verb format l2 in - let l1, l2, fmt_l1, fmt_l2, missing_cmi_option = match t with - | { violation = Not_a_subjkind(l1, l2); missing_cmi } -> - begin match missing_cmi with + let l1, l2, fmt_l1, fmt_l2, missing_cmi_option = + match t with + | { violation = Not_a_subjkind (l1, l2); missing_cmi } -> ( + match missing_cmi with | None -> - l1, l2, - dprintf "layout %a" format l1, - subjkind_format "is not" l2, None + ( l1, + l2, + dprintf "layout %a" format l1, + subjkind_format "is not" l2, + None ) | Some p -> - l1, l2, - dprintf "an unknown layout", - subjkind_format "might not be" l2, Some p - end - | { violation = No_intersection(l1, l2); missing_cmi } -> + ( l1, + l2, + dprintf "an unknown layout", + subjkind_format "might not be" l2, + Some p )) + | { violation = No_intersection (l1, l2); missing_cmi } -> assert (Option.is_none missing_cmi); - l1, l2, - dprintf "layout %a" format l1, - dprintf "does not overlap with %a" format l2, None + ( l1, + l2, + dprintf "layout %a" format l1, + dprintf "does not overlap with %a" format l2, + None ) in - if display_histories then begin - let connective = match t.violation with + if display_histories + then + let connective = + match t.violation with | Not_a_subjkind _ -> "be a sublayout of" | No_intersection _ -> "overlap with" in fprintf ppf "%a%a" - (format_history ~intro:(dprintf "The layout of %a is" pp_former former)) l1 - (format_history ~intro:(dprintf "But the layout of %a must %s" pp_former former connective)) l2; - end else begin - fprintf ppf "@[%s%a has %t,@ which %t.@]" - preamble - pp_former former - fmt_l1 - fmt_l2 - end; + (format_history ~intro:(dprintf "The layout of %a is" pp_former former)) + l1 + (format_history + ~intro: + (dprintf "But the layout of %a must %s" pp_former former connective)) + l2 + else + fprintf ppf "@[%s%a has %t,@ which %t.@]" preamble pp_former former + fmt_l1 fmt_l2; report_missing_cmi ppf missing_cmi_option let pp_t ppf x = fprintf ppf "%t" x - let report_with_offender ~offender = - report_general "" pp_t offender + let report_with_offender ~offender = report_general "" pp_t offender let report_with_offender_sort ~offender = report_general "A representable layout was expected, but " pp_t offender - let report_with_name ~name = - report_general "" pp_print_string name + let report_with_name ~name = report_general "" pp_print_string name end (******************************) @@ -986,15 +997,12 @@ let equate_or_equal ~allow_mutation (l1 : t) (l2 : t) = | Any, Any -> true | Immediate64, Immediate64 -> true | Immediate, Immediate -> true - | Sort s1, Sort s2 -> begin - match Sort.equate_tracking_mutation s1 s2 with - | (Equal_mutated_first | Equal_mutated_second) - when not allow_mutation -> - Misc.fatal_errorf - "Jkind.equal: Performed unexpected mutation" - | Unequal -> false - | Equal_no_mutation | Equal_mutated_first | Equal_mutated_second -> true - end + | Sort s1, Sort s2 -> ( + match Sort.equate_tracking_mutation s1 s2 with + | (Equal_mutated_first | Equal_mutated_second) when not allow_mutation -> + Misc.fatal_errorf "Jkind.equal: Performed unexpected mutation" + | Unequal -> false + | Equal_no_mutation | Equal_mutated_first | Equal_mutated_second -> true) | (Any | Immediate64 | Immediate | Sort _), _ -> false (* CR layouts v2.8: Switch this back to ~allow_mutation:false *) @@ -1003,8 +1011,13 @@ let equal = equate_or_equal ~allow_mutation:true let equate = equate_or_equal ~allow_mutation:true let combine_histories reason lhs rhs = - Interact { reason; lhs_jkind = lhs.jkind; lhs_history = lhs.history; - rhs_jkind = rhs.jkind; rhs_history = rhs.history } + Interact + { reason; + lhs_jkind = lhs.jkind; + lhs_history = lhs.history; + rhs_jkind = rhs.jkind; + rhs_history = rhs.history + } let intersection ~reason l1 l2 = match l1.jkind, l2.jkind with @@ -1013,7 +1026,7 @@ let intersection ~reason l1 l2 = is not interesting *) | _, Any -> Ok l1 | Any, _ -> Ok l2 - | (Immediate, Immediate) | (Immediate64, Immediate64) -> + | Immediate, Immediate | Immediate64, Immediate64 -> Ok { l1 with history = combine_histories reason l1 l2 } | Immediate, Immediate64 -> Ok l1 | Immediate64, Immediate -> Ok l2 @@ -1033,7 +1046,7 @@ let intersection ~reason l1 l2 = (* this is hammered on; it must be fast! *) let check_sub sub super : sub_result = match sub.jkind, super.jkind with - (* don't use [get], because that allocates *) + (* don't use [get], because that allocates *) | Any, Any -> Equal | _, Any -> Sub | Immediate, Immediate -> Equal @@ -1042,16 +1055,17 @@ let check_sub sub super : sub_result = | Immediate64, Immediate -> Not_sub | (Immediate | Immediate64), Sort s -> if Sort.equate s Sort.value then Sub else Not_sub - | Sort s1, Sort s2 -> - if Sort.equate s1 s2 then Equal else Not_sub + | Sort s1, Sort s2 -> if Sort.equate s1 s2 then Equal else Not_sub | Any, _ -> Not_sub | Sort _, (Immediate | Immediate64) -> Not_sub -let sub sub super = match check_sub sub super with +let sub sub super = + match check_sub sub super with | Sub | Equal -> Ok () | Not_sub -> Error (Violation.of_ (Not_a_subjkind (sub, super))) -let sub_with_history sub super = match check_sub sub super with +let sub_with_history sub super = + match check_sub sub super with | Sub | Equal -> Ok { sub with history = combine_histories Subjkind sub super } | Not_sub -> Error (Violation.of_ (Not_a_subjkind (sub, super))) @@ -1060,9 +1074,7 @@ let is_void_defaulting = function | { jkind = Sort s } -> Sort.is_void_defaulting s | _ -> false -let is_any = function - | { jkind = Any } -> true - | _ -> false +let is_any = function { jkind = Any } -> true | _ -> false (*********************************) (* debugging *) @@ -1077,54 +1089,37 @@ module Debug_printers = struct | Immediate -> fprintf ppf "Immediate" let concrete_jkind_reason ppf : concrete_jkind_reason -> unit = function - | Match -> - fprintf ppf "Match" + | Match -> fprintf ppf "Match" | Constructor_declaration idx -> - fprintf ppf "Constructor_declaration %d" idx + fprintf ppf "Constructor_declaration %d" idx | Label_declaration lbl -> - fprintf ppf "Label_declaration %a" Ident.print lbl - | Unannotated_type_parameter -> - fprintf ppf "Unannotated_type_parameter" - | Record_projection -> - fprintf ppf "Record_projection" - | Record_assignment -> - fprintf ppf "Record_assignment" - | Let_binding -> - fprintf ppf "Let_binding" - | Function_argument -> - fprintf ppf "Function_argument" - | Function_result -> - fprintf ppf "Function_result" - | Structure_item_expression -> - fprintf ppf "Structure_item_expression" - | V1_safety_check -> - fprintf ppf "V1_safety_check" - | External_argument -> - fprintf ppf "External_argument" - | External_result -> - fprintf ppf "External_result" - | Statement -> - fprintf ppf "Statement" + fprintf ppf "Label_declaration %a" Ident.print lbl + | Unannotated_type_parameter -> fprintf ppf "Unannotated_type_parameter" + | Record_projection -> fprintf ppf "Record_projection" + | Record_assignment -> fprintf ppf "Record_assignment" + | Let_binding -> fprintf ppf "Let_binding" + | Function_argument -> fprintf ppf "Function_argument" + | Function_result -> fprintf ppf "Function_result" + | Structure_item_expression -> fprintf ppf "Structure_item_expression" + | V1_safety_check -> fprintf ppf "V1_safety_check" + | External_argument -> fprintf ppf "External_argument" + | External_result -> fprintf ppf "External_result" + | Statement -> fprintf ppf "Statement" let annotation_context ppf : annotation_context -> unit = function - | Type_declaration p -> - fprintf ppf "Type_declaration %a" Path.print p + | Type_declaration p -> fprintf ppf "Type_declaration %a" Path.print p | Type_parameter (p, var) -> - fprintf ppf "Type_parameter (%a, %a)" - Path.print p - (Misc.Stdlib.Option.print Misc.Stdlib.String.print) var - | With_constraint s -> - fprintf ppf "With_constraint %S" s - | Newtype_declaration name -> - fprintf ppf "Newtype_declaration %s" name + fprintf ppf "Type_parameter (%a, %a)" Path.print p + (Misc.Stdlib.Option.print Misc.Stdlib.String.print) + var + | With_constraint s -> fprintf ppf "With_constraint %S" s + | Newtype_declaration name -> fprintf ppf "Newtype_declaration %s" name | Constructor_type_parameter (cstr, name) -> - fprintf ppf "Constructor_type_parameter (%a, %S)" Path.print cstr name - | Univar name -> - fprintf ppf "Univar %S" name - | Type_variable name -> - fprintf ppf "Type_variable %S" name + fprintf ppf "Constructor_type_parameter (%a, %S)" Path.print cstr name + | Univar name -> fprintf ppf "Univar %S" name + | Type_variable name -> fprintf ppf "Type_variable %S" name | Type_wildcard loc -> - fprintf ppf "Type_wildcard (%a)" Location.print_loc loc + fprintf ppf "Type_wildcard (%a)" Location.print_loc loc let any_creation_reason ppf : any_creation_reason -> unit = function | Missing_cmi p -> fprintf ppf "Missing_cmi %a" Path.print p @@ -1134,8 +1129,7 @@ module Debug_printers = struct | Dummy_jkind -> fprintf ppf "Dummy_jkind" | Type_expression_call -> fprintf ppf "Type_expression_call" - let immediate_creation_reason ppf : immediate_creation_reason -> _ = - function + let immediate_creation_reason ppf : immediate_creation_reason -> _ = function | Empty_record -> fprintf ppf "Empty_record" | Enumeration -> fprintf ppf "Enumeration" | Primitive id -> fprintf ppf "Primitive %s" (Ident.unique_name id) @@ -1193,86 +1187,67 @@ module Debug_printers = struct let creation_reason ppf : creation_reason -> unit = function | Annotated (ctx, loc) -> - fprintf ppf "Annotated (%a,%a)" - annotation_context ctx - Location.print_loc loc - | Any_creation any -> - fprintf ppf "Any_creation %a" any_creation_reason any + fprintf ppf "Annotated (%a,%a)" annotation_context ctx Location.print_loc + loc + | Any_creation any -> fprintf ppf "Any_creation %a" any_creation_reason any | Immediate_creation immediate -> - fprintf ppf "Immediate_creation %a" immediate_creation_reason immediate + fprintf ppf "Immediate_creation %a" immediate_creation_reason immediate | Immediate64_creation immediate64 -> - fprintf ppf "Immediate64_creation %a" immediate64_creation_reason immediate64 + fprintf ppf "Immediate64_creation %a" immediate64_creation_reason + immediate64 | Value_creation value -> - fprintf ppf "Value_creation %a" value_creation_reason value + fprintf ppf "Value_creation %a" value_creation_reason value | Void_creation void -> - fprintf ppf "Void_creation %a" void_creation_reason void + fprintf ppf "Void_creation %a" void_creation_reason void | Float64_creation float -> - fprintf ppf "Float64_creation %a" float64_creation_reason float + fprintf ppf "Float64_creation %a" float64_creation_reason float | Concrete_creation concrete -> - fprintf ppf "Concrete_creation %a" concrete_jkind_reason concrete - | Imported -> - fprintf ppf "Imported" + fprintf ppf "Concrete_creation %a" concrete_jkind_reason concrete + | Imported -> fprintf ppf "Imported" let interact_reason ppf = function - | Gadt_equation p -> - fprintf ppf "Gadt_equation %a" - Path.print p + | Gadt_equation p -> fprintf ppf "Gadt_equation %a" Path.print p | Tyvar_refinement_intersection -> fprintf ppf "Tyvar_refinement_intersection" - | Subjkind -> - fprintf ppf "Subjkind" + | Subjkind -> fprintf ppf "Subjkind" let rec history ppf = function - | Interact - { reason; lhs_jkind; lhs_history; rhs_jkind; rhs_history } -> - fprintf ppf "Interact {@[reason = %a;@ \ - lhs_jkind = %a;@ \ - lhs_history = %a;@ \ - rhs_jkind = %a;@ \ - rhs_history = %a}@]" - interact_reason reason - internal lhs_jkind - history lhs_history - internal rhs_jkind - history rhs_history - | Creation c -> - fprintf ppf "Creation (%a)" - creation_reason c - - let t ppf ({ jkind; history=h } : t) : unit = - fprintf ppf "@[{ jkind = %a@,; history = %a }@]" - internal jkind - history h + | Interact { reason; lhs_jkind; lhs_history; rhs_jkind; rhs_history } -> + fprintf ppf + "Interact {@[reason = %a;@ lhs_jkind = %a;@ lhs_history = %a;@ \ + rhs_jkind = %a;@ rhs_history = %a}@]" + interact_reason reason internal lhs_jkind history lhs_history internal + rhs_jkind history rhs_history + | Creation c -> fprintf ppf "Creation (%a)" creation_reason c + + let t ppf ({ jkind; history = h } : t) : unit = + fprintf ppf "@[{ jkind = %a@,; history = %a }@]" internal jkind history + h end (*** formatting user errors ***) let report_error ~loc = function -| Insufficient_level (context, jkind) -> - let required_layouts_level = get_required_layouts_level context jkind in - let hint ppf = - Format.fprintf ppf "You must enable -extension %s to use this feature." - (Language_extension.to_command_line_string - Layouts required_layouts_level) - in - match Language_extension.get_command_line_string_if_enabled Layouts with - | None -> - Location.errorf ~loc - "@[The appropriate layouts extension is not enabled.@;%t@]" - hint - | Some cmd_line_string -> - Location.errorf ~loc - (* CR layouts errors: use the context to produce a better error message. - When RAE tried this, some types got printed like [t/2], but the - [/2] shouldn't be there. Investigate and fix. *) - "@[Layout %s is more experimental than allowed by -extension %s.@;%t@]" - (string_of_const jkind) - cmd_line_string - hint + | Insufficient_level (context, jkind) -> ( + let required_layouts_level = get_required_layouts_level context jkind in + let hint ppf = + Format.fprintf ppf "You must enable -extension %s to use this feature." + (Language_extension.to_command_line_string Layouts + required_layouts_level) + in + match Language_extension.get_command_line_string_if_enabled Layouts with + | None -> + Location.errorf ~loc + "@[The appropriate layouts extension is not enabled.@;%t@]" hint + | Some cmd_line_string -> + Location.errorf ~loc + (* CR layouts errors: use the context to produce a better error message. + When RAE tried this, some types got printed like [t/2], but the + [/2] shouldn't be there. Investigate and fix. *) + "@[Layout %s is more experimental than allowed by -extension %s.@;\ + %t@]" + (string_of_const jkind) cmd_line_string hint) let () = - Location.register_error_of_exn - (function - | User_error(loc, err) -> - Some (report_error ~loc err) - | _ -> None) - + Location.register_error_of_exn (function + | User_error (loc, err) -> Some (report_error ~loc err) + | _ -> None) diff --git a/typing/jkind.mli b/typing/jkind.mli index 48f5006d777..b15fc1bedc7 100644 --- a/typing/jkind.mli +++ b/typing/jkind.mli @@ -39,13 +39,9 @@ module Sort : sig (** These are the constant sorts -- fully determined and without variables *) type const = - | Void - (** No run time representation at all *) - | Value - (** Standard ocaml value representation *) - | Float64 - (** Unboxed 64-bit floats *) - + | Void (** No run time representation at all *) + | Value (** Standard ocaml value representation *) + | Float64 (** Unboxed 64-bit floats *) (** A sort variable that can be unified during type-checking. *) type var @@ -54,10 +50,13 @@ module Sort : sig val new_var : unit -> t val of_const : const -> t + val of_var : var -> t val void : t + val value : t + val float64 : t (** These names are generated lazily and only when this function is called, @@ -85,6 +84,7 @@ module Sort : sig module Debug_printers : sig val t : Format.formatter -> t -> unit + val var : Format.formatter -> var -> unit end @@ -96,27 +96,44 @@ module Sort : sig just the translation to lambda) rather than writing specific jkinds and sorts in the code. *) val for_class_arg : t + val for_instance_var : t + val for_lazy_body : t + val for_tuple_element : t + val for_record : t + val for_constructor_arg : t + val for_block_element : t + val for_array_get_result : t + val for_array_element : t + val for_list_element : t (** These are sorts for the types of ocaml expressions that we expect will always be "value". These names are used in the translation to lambda to make the code clearer. *) val for_function : t + val for_probe_body : t + val for_poly_variant : t + val for_object : t + val for_initializer : t + val for_method : t + val for_module : t + val for_predef_value : t (* Predefined value types, e.g. int and string *) + val for_tuple : t end @@ -170,7 +187,7 @@ type annotation_context = | Type_variable of string | Type_wildcard of Location.t - type value_creation_reason = +type value_creation_reason = | Class_let_binding | Tuple_element | Probe @@ -204,7 +221,7 @@ type annotation_context = | Debug_printer_argument | V1_safety_check | Captured_in_object - | Unknown of string (* CR layouts: get rid of these *) + | Unknown of string (* CR layouts: get rid of these *) type immediate_creation_reason = | Empty_record @@ -219,8 +236,7 @@ type immediate64_creation_reason = | Gc_ignorable_check | Separability_check -type void_creation_reason = - | V1_safety_check +type void_creation_reason = V1_safety_check type any_creation_reason = | Missing_cmi of Path.t @@ -233,8 +249,7 @@ type any_creation_reason = unified to correct levels *) | Type_expression_call -type float64_creation_reason = - | Primitive of Ident.t +type float64_creation_reason = Primitive of Ident.t type creation_reason = | Annotated of annotation_context * Location.t @@ -276,17 +291,16 @@ module Violation : sig (* CR layouts: Having these options for printing a violation was a choice made based on the needs of expedient debugging during development, but probably should be rethought at some point. *) + (** Prints a violation and the thing that had an unexpected jkind ([offender], which you supply an arbitrary printer for). *) val report_with_offender : - offender:(Format.formatter -> unit) -> - Format.formatter -> t -> unit + offender:(Format.formatter -> unit) -> Format.formatter -> t -> unit (** Like [report_with_offender], but additionally prints that the issue is that a representable jkind was expected. *) val report_with_offender_sort : - offender:(Format.formatter -> unit) -> - Format.formatter -> t -> unit + offender:(Format.formatter -> unit) -> Format.formatter -> t -> unit (** Simpler version of [report_with_offender] for when the thing that had an unexpected jkind is available as a string. *) @@ -305,7 +319,9 @@ type const = Jane_asttypes.const_jkind = | Immediate64 | Immediate | Float64 + val string_of_const : const -> string + val equal_const : const -> const -> bool (** This jkind is the top of the jkind lattice. All types have jkind [any]. @@ -336,6 +352,7 @@ val float64 : why:float64_creation_reason -> t val of_new_sort_var : why:concrete_jkind_reason -> t val of_sort : why:concrete_jkind_reason -> sort -> t + val of_const : why:creation_reason -> const -> t (* CR layouts v1.5: remove legacy_immediate when the old attributes mechanism @@ -348,22 +365,28 @@ val of_annotation : val of_annotation_option_default : ?legacy_immediate:bool -> - default:t -> context:annotation_context -> - Jane_asttypes.jkind_annotation option -> t + default:t -> + context:annotation_context -> + Jane_asttypes.jkind_annotation option -> + t (** Find a jkind in attributes. Returns error if a disallowed jkind is present, but always allows immediate attributes if ~legacy_immediate is true. See comment on [Builtin_attributes.jkind]. *) val of_attributes : - legacy_immediate:bool -> context:annotation_context -> Parsetree.attributes -> + legacy_immediate:bool -> + context:annotation_context -> + Parsetree.attributes -> (t option, Jane_asttypes.jkind_annotation) result (** Find a jkind in attributes, defaulting to ~default. Returns error if a disallowed jkind is present, but always allows immediate if ~legacy_immediate is true. See comment on [Builtin_attributes.jkind]. *) val of_attributes_default : - legacy_immediate:bool -> context:annotation_context -> - default:t -> Parsetree.attributes -> + legacy_immediate:bool -> + context:annotation_context -> + default:t -> + Parsetree.attributes -> (t, Jane_asttypes.jkind_annotation) result (** Choose an appropriate jkind for a boxed record type, given whether @@ -409,6 +432,7 @@ val sort_of_jkind : t -> sort (* pretty printing *) val to_string : t -> string + val format : Format.formatter -> t -> unit (** Format the history of this jkind: what interactions it has had and why @@ -417,8 +441,7 @@ val format : Format.formatter -> t -> unit The [intro] is something like "The jkind of t is". *) val format_history : - intro:(Format.formatter -> unit) -> - Format.formatter -> t -> unit + intro:(Format.formatter -> unit) -> Format.formatter -> t -> unit (** Provides the [Printtyp.path] formatter back up the dependency chain to this module. *) @@ -446,8 +469,7 @@ val equal : t -> t -> bool jkind argument. That is, due to histories, this function is asymmetric; it should be thought of as modifying the first jkind to be the intersection of the two, not something that modifies the second jkind. *) -val intersection : - reason:interact_reason -> t -> t -> (t, Violation.t) Result.t +val intersection : reason:interact_reason -> t -> t -> (t, Violation.t) Result.t (** [sub t1 t2] returns [Ok ()] iff [t1] is a subjkind of of [t2]. The current hierarchy is: diff --git a/typing/mode.ml b/typing/mode.ml index f56ad750c17..11caee5e52b 100644 --- a/typing/mode.ml +++ b/typing/mode.ml @@ -13,13 +13,13 @@ (* *) (**************************************************************************) -type 'a var = { - mutable upper : 'a; - mutable lower : 'a; - mutable vlower : 'a var list; - mutable mark : bool; - mvid : int; -} +type 'a var = + { mutable upper : 'a; + mutable lower : 'a; + mutable vlower : 'a var list; + mutable mark : bool; + mvid : int + } type changes = | Cnil : changes @@ -42,14 +42,14 @@ let set_vlower ~log v vlower = let rec undo_changes = function | Cnil -> () | Cupper (v, upper, rest) -> - v.upper <- upper; - undo_changes rest + v.upper <- upper; + undo_changes rest | Clower (v, lower, rest) -> - v.lower <- lower; - undo_changes rest + v.lower <- lower; + undo_changes rest | Cvlower (v, vlower, rest) -> - v.vlower <- vlower; - undo_changes rest + v.vlower <- vlower; + undo_changes rest let change_log : (changes -> unit) ref = ref (fun _ -> ()) @@ -59,55 +59,86 @@ let is_not_nil = function let log_changes changes = if is_not_nil changes then !change_log changes -type ('a, 'b) const_or_var = Const of 'a | Var of 'b +type ('a, 'b) const_or_var = + | Const of 'a + | Var of 'b -type ('loc, 'u, 'lin) modes = { - locality : 'loc; - uniqueness : 'u; - linearity : 'lin; -} +type ('loc, 'u, 'lin) modes = + { locality : 'loc; + uniqueness : 'u; + linearity : 'lin + } module type Lattice = sig type t val min : t + val max : t + val eq : t -> t -> bool + val le : t -> t -> bool + val join : t -> t -> t + val meet : t -> t -> t + val print : Format.formatter -> t -> unit end module type Solver = sig type const + type t + type var val of_const : const -> t + val min_mode : t + val max_mode : t + val is_const : t -> bool + val submode : t -> t -> (unit, unit) Result.t + val submode_exn : t -> t -> unit + val equate : t -> t -> (unit, unit) Result.t + val constrain_upper : t -> const + val newvar : unit -> t + val newvar_below : t -> t * bool + val newvar_above : t -> t * bool + val join : t list -> t + val meet : t list -> t + val constrain_lower : t -> const + val const_or_var : t -> (const, var) const_or_var + val check_const : t -> const option + val print_var : Format.formatter -> var -> unit + val print : Format.formatter -> t -> unit + val print' : ?verbose:bool -> ?label:string -> Format.formatter -> t -> unit end module Solver (L : Lattice) : Solver with type const := L.t = struct type nonrec var = L.t var - type t = Amode of L.t | Amodevar of var + + type t = + | Amode of L.t + | Amodevar of var let next_id = ref (-1) @@ -118,21 +149,28 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct exception NotSubmode let of_const c = Amode c + let min_mode = Amode L.min + let max_mode = Amode L.max + let is_const = function Amode _ -> true | Amodevar _ -> false let submode_cv ~log m v = - if L.le m v.lower then () - else if not (L.le m v.upper) then raise NotSubmode + if L.le m v.lower + then () + else if not (L.le m v.upper) + then raise NotSubmode else let m = L.join v.lower m in set_lower ~log v m; if L.eq m v.upper then set_vlower ~log v [] let rec submode_vc ~log v m = - if L.le v.upper m then () - else if not (L.le v.lower m) then raise NotSubmode + if L.le v.upper m + then () + else if not (L.le v.lower m) + then raise NotSubmode else let m = L.meet v.upper m in set_upper ~log v m; @@ -145,8 +183,10 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct let submode_vv ~log a b = (* Printf.printf " %a <= %a\n" pp_v a pp_v b; *) - if L.le a.upper b.lower then () - else if a == b || List.memq a b.vlower then () + if L.le a.upper b.lower + then () + else if a == b || List.memq a b.vlower + then () else ( submode_vc ~log a b.upper; set_vlower ~log b (a :: b.vlower); @@ -157,8 +197,10 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct | v' :: rest -> if v == v' then all_equal v rest else false let join_vc v m = - if L.le v.upper m then Amode m - else if L.le m v.lower then Amodevar v + if L.le v.upper m + then Amode m + else if L.le m v.lower + then Amodevar v else let log = ref Cnil in let v' = fresh () in @@ -171,18 +213,21 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct match vs with | [] -> Amode m | v :: rest -> - if all_equal v rest then join_vc v m - else - let log = ref Cnil in - let v = fresh () in - submode_cv ~log m v; - List.iter (fun v' -> submode_vv ~log v' v) vs; - log_changes !log; - Amodevar v + if all_equal v rest + then join_vc v m + else + let log = ref Cnil in + let v = fresh () in + submode_cv ~log m v; + List.iter (fun v' -> submode_vv ~log v' v) vs; + log_changes !log; + Amodevar v let meet_vc v m = - if L.le m v.lower then Amode m - else if L.le v.upper m then Amodevar v + if L.le m v.lower + then Amode m + else if L.le v.upper m + then Amodevar v else let log = ref Cnil in let v' = fresh () in @@ -195,30 +240,31 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct match vs with | [] -> Amode m | v :: rest -> - if all_equal v rest then meet_vc v m - else - let log = ref Cnil in - let v = fresh () in - submode_vc ~log v m; - List.iter (fun v' -> submode_vv ~log v v') vs; - log_changes !log; - Amodevar v + if all_equal v rest + then meet_vc v m + else + let log = ref Cnil in + let v = fresh () in + submode_vc ~log v m; + List.iter (fun v' -> submode_vv ~log v v') vs; + log_changes !log; + Amodevar v let submode a b = let log = ref Cnil in match - match (a, b) with + match a, b with | Amode a, Amode b -> if not (L.le a b) then raise NotSubmode | Amodevar v, Amode c -> submode_vc ~log v c | Amode c, Amodevar v -> submode_cv ~log c v | Amodevar a, Amodevar b -> submode_vv ~log a b with | () -> - log_changes !log; - Ok () + log_changes !log; + Ok () | exception NotSubmode -> - undo_changes !log; - Error () + undo_changes !log; + Error () let submode_exn t1 t2 = match submode t1 t2 with @@ -226,31 +272,31 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct | Error () -> invalid_arg "submode_exn" let equate a b = - match (submode a b, submode b a) with + match submode a b, submode b a with | Ok (), Ok () -> Ok () | Error (), _ | _, Error () -> Error () let constrain_upper = function | Amode m -> m | Amodevar v -> - submode_exn (Amode v.upper) (Amodevar v); - v.upper + submode_exn (Amode v.upper) (Amodevar v); + v.upper let newvar () = Amodevar (fresh ()) let newvar_below = function - | Amode c when L.eq c L.min -> (min_mode, false) + | Amode c when L.eq c L.min -> min_mode, false | m -> - let v = newvar () in - submode_exn v m; - (v, true) + let v = newvar () in + submode_exn v m; + v, true let newvar_above = function - | Amode c when L.eq c L.max -> (max_mode, false) + | Amode c when L.eq c L.max -> max_mode, false | m -> - let v = newvar () in - submode_exn m v; - (v, true) + let v = newvar () in + submode_exn m v; + v, true let join ms = let rec aux vars const = function @@ -289,19 +335,23 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct (* Ensure that each transitive lower bound of v is a direct lower bound of v *) let rec trans v' = - if L.le v'.upper !new_lower then () - else if v'.mark then () + if L.le v'.upper !new_lower + then () + else if v'.mark + then () else ( mark v'; new_vlower := v' :: !new_vlower; trans_low v') and trans_low v' = assert (v != v'); - if not (L.le v'.lower v.upper) then - Misc.fatal_error "compress_vlower: invalid bounds"; - if not (L.le v'.lower !new_lower) then ( + if not (L.le v'.lower v.upper) + then Misc.fatal_error "compress_vlower: invalid bounds"; + if not (L.le v'.lower !new_lower) + then ( new_lower := L.join !new_lower v'.lower; - if !new_lower = v.upper then + if !new_lower = v.upper + then (* v is now a constant, no need to keep computing bounds *) raise Became_constant); List.iter trans v'.vlower @@ -317,7 +367,8 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct unmark v; assert (!nmarked = 0); if became_constant then new_vlower := []; - if !new_lower != v.lower || !new_vlower != v.vlower then ( + if !new_lower != v.lower || !new_vlower != v.vlower + then ( let log = ref Cnil in set_lower ~log v !new_lower; set_vlower ~log v !new_vlower; @@ -326,15 +377,15 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct let constrain_lower = function | Amode m -> m | Amodevar v -> - compress_vlower v; - submode_exn (Amodevar v) (Amode v.lower); - v.lower + compress_vlower v; + submode_exn (Amodevar v) (Amode v.lower); + v.lower let const_or_var = function | Amode m -> Const m | Amodevar v -> - compress_vlower v; - if L.eq v.lower v.upper then Const v.lower else Var v + compress_vlower v; + if L.eq v.lower v.upper then Const v.lower else Var v let check_const a = match const_or_var a with Const m -> Some m | Var _ -> None @@ -342,7 +393,8 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct let print_var_id ppf v = Format.fprintf ppf "?%i" v.mvid let print_var ppf v = - if v.vlower = [] then print_var_id ppf v + if v.vlower = [] + then print_var_id ppf v else Format.fprintf ppf "%a[> %a]" print_var_id v (Format.pp_print_list print_var_id) @@ -352,8 +404,8 @@ module Solver (L : Lattice) : Solver with type const := L.t = struct match const_or_var a with | Const m -> L.print ppf m | Var v -> - (match label with None -> () | Some s -> Format.fprintf ppf "%s:" s); - if verbose then print_var ppf v else Format.fprintf ppf "?" + (match label with None -> () | Some s -> Format.fprintf ppf "%s:" s); + if verbose then print_var ppf v else Format.fprintf ppf "?" let print ppf a = print' ~verbose:true ?label:None ppf a end @@ -364,6 +416,7 @@ module type DualLattice = sig type dual val to_dual : t -> dual + val of_dual : dual -> t end @@ -373,6 +426,7 @@ module type DualSolver = sig type dual val to_dual : t -> dual + val of_dual : dual -> t end @@ -382,30 +436,43 @@ module DualSolver (L : DualLattice with type dual := Dual.t) : DualSolver with type const := L.t and type dual := Solver.t = struct type var = Solver.var + type t = Solver.t let of_const c = Solver.of_const (L.to_dual c) + let is_const a = Solver.is_const a + let submode a b = Solver.submode b a + let submode_exn a b = Solver.submode_exn b a + let equate a b = Solver.equate b a + let constrain_upper a = L.of_dual (Solver.constrain_lower a) + let constrain_lower a = L.of_dual (Solver.constrain_upper a) + let to_dual a = a + let of_dual a = a + let min_mode = of_dual Solver.max_mode + let max_mode = of_dual Solver.min_mode + let newvar () = Solver.newvar () let newvar_below a = let a', changed = Solver.newvar_above a in - (a', changed) + a', changed let newvar_above a = let a', changed = Solver.newvar_below a in - (a', changed) + a', changed let join ts = Solver.meet ts + let meet ts = Solver.join ts let const_or_var a = @@ -424,40 +491,40 @@ module DualSolver match Solver.const_or_var a with | Const m -> L.print ppf (L.of_dual m) | Var v -> - (match label with None -> () | Some s -> Format.fprintf ppf "%s:" s); - if verbose then - (* caret stands for dual *) - Format.fprintf ppf "^%a" print_var v - else Format.fprintf ppf "?" + (match label with None -> () | Some s -> Format.fprintf ppf "%s:" s); + if verbose + then (* caret stands for dual *) + Format.fprintf ppf "^%a" print_var v + else Format.fprintf ppf "?" let print ppf m = print' ~verbose:true ?label:None ppf m end module Locality = struct module Const = struct - type t = Global | Local + type t = + | Global + | Local let min = Global + let max = Local + let legacy = Global let le a b = - match (a, b) with Global, _ | _, Local -> true | Local, Global -> false + match a, b with Global, _ | _, Local -> true | Local, Global -> false let eq a b = - match (a, b) with + match a, b with | Global, Global | Local, Local -> true | Local, Global | Global, Local -> false let join a b = - match (a, b) with - | Local, _ | _, Local -> Local - | Global, Global -> Global + match a, b with Local, _ | _, Local -> Local | Global, Global -> Global let meet a b = - match (a, b) with - | Global, _ | _, Global -> Global - | Local, Local -> Local + match a, b with Global, _ | _, Global -> Global | Local, Local -> Local let print ppf = function | Global -> Format.fprintf ppf "Global" @@ -467,14 +534,20 @@ module Locality = struct include Solver (Const) let global = of_const Const.Global + let local = of_const Const.Local + let legacy = global + let constrain_legacy = constrain_lower end module Regionality = struct module Const = struct - type t = Global | Regional | Local + type t = + | Global + | Regional + | Local let r_as_l : t -> Locality.Const.t = function | Local | Regional -> Local @@ -486,7 +559,7 @@ module Regionality = struct let of_localities ~(r_as_l : Locality.Const.t) ~(r_as_g : Locality.Const.t) = - match (r_as_l, r_as_g) with + match r_as_l, r_as_g with | Global, Global -> Global | Global, Local -> assert false | Local, Global -> Regional @@ -502,22 +575,28 @@ module Regionality = struct Format.fprintf ppf "%s" s end - type t = { r_as_l : Locality.t; r_as_g : Locality.t } + type t = + { r_as_l : Locality.t; + r_as_g : Locality.t + } let of_locality l = { r_as_l = l; r_as_g = l } let of_const c = let r_as_l, r_as_g = match c with - | Const.Global -> (Locality.global, Locality.global) - | Const.Regional -> (Locality.local, Locality.global) - | Const.Local -> (Locality.local, Locality.local) + | Const.Global -> Locality.global, Locality.global + | Const.Regional -> Locality.local, Locality.global + | Const.Local -> Locality.local, Locality.local in { r_as_l; r_as_g } let local = of_const Local + let regional = of_const Regional + let global = of_const Global + let legacy = global let max_mode = @@ -531,24 +610,31 @@ module Regionality = struct { r_as_l; r_as_g } let local_to_regional t = { t with r_as_g = Locality.global } + let regional_to_global t = { t with r_as_l = t.r_as_g } + let regional_to_local t = { t with r_as_g = t.r_as_l } + let global_to_regional t = { t with r_as_l = Locality.local } + let regional_to_global_locality t = t.r_as_g + let regional_to_local_locality t = t.r_as_l - type error = [ `Regionality | `Locality ] + type error = + [ `Regionality + | `Locality ] let submode t1 t2 = match Locality.submode t1.r_as_l t2.r_as_l with | Error () -> Error `Regionality | Ok () -> ( - match Locality.submode t1.r_as_g t2.r_as_g with - | Error () -> Error `Locality - | Ok () as ok -> ok) + match Locality.submode t1.r_as_g t2.r_as_g with + | Error () -> Error `Locality + | Ok () as ok -> ok) let equate a b = - match (submode a b, submode b a) with + match submode a b, submode b a with | Ok (), Ok () -> Ok () | Error e, _ | _, Error e -> Error e @@ -576,64 +662,66 @@ module Regionality = struct let r_as_l, changed1 = Locality.newvar_below t.r_as_l in let r_as_g, changed2 = Locality.newvar_below t.r_as_g in Locality.submode_exn r_as_g r_as_l; - ({ r_as_l; r_as_g }, changed1 || changed2) + { r_as_l; r_as_g }, changed1 || changed2 let newvar_above t = let r_as_l, changed1 = Locality.newvar_above t.r_as_l in let r_as_g, changed2 = Locality.newvar_above t.r_as_g in Locality.submode_exn r_as_g r_as_l; - ({ r_as_l; r_as_g }, changed1 || changed2) + { r_as_l; r_as_g }, changed1 || changed2 let check_const t = match Locality.check_const t.r_as_l with | None -> None | Some r_as_l -> ( - match Locality.check_const t.r_as_g with - | None -> None - | Some r_as_g -> Some (Const.of_localities ~r_as_l ~r_as_g)) + match Locality.check_const t.r_as_g with + | None -> None + | Some r_as_g -> Some (Const.of_localities ~r_as_l ~r_as_g)) let print' ?(verbose = true) ?label ppf t = match check_const t with | Some l -> Const.print ppf l | None -> ( - match label with - | None -> () - | Some l -> - Format.fprintf ppf "%s: " l; - Format.fprintf ppf "r_as_l=%a r_as_g=%a" - (Locality.print' ~verbose ?label:None) - t.r_as_l - (Locality.print' ~verbose ?label:None) - t.r_as_g) + match label with + | None -> () + | Some l -> + Format.fprintf ppf "%s: " l; + Format.fprintf ppf "r_as_l=%a r_as_g=%a" + (Locality.print' ~verbose ?label:None) + t.r_as_l + (Locality.print' ~verbose ?label:None) + t.r_as_g) let print ppf m = print' ~verbose:true ?label:None ppf m end module Uniqueness = struct module Const = struct - type t = Unique | Shared + type t = + | Unique + | Shared let legacy = Shared + let min = Unique + let max = Shared let le a b = - match (a, b) with - | Unique, _ | _, Shared -> true - | Shared, Unique -> false + match a, b with Unique, _ | _, Shared -> true | Shared, Unique -> false let eq a b = - match (a, b) with + match a, b with | Unique, Unique | Shared, Shared -> true | Shared, Unique | Unique, Shared -> false let join a b = - match (a, b) with + match a, b with | Shared, _ | _, Shared -> Shared | Unique, Unique -> Unique let meet a b = - match (a, b) with + match a, b with | Unique, _ | _, Unique -> Unique | Shared, Shared -> Shared @@ -645,32 +733,39 @@ module Uniqueness = struct include Solver (Const) let constrain_legacy = constrain_upper + let unique = of_const Const.Unique + let shared = of_const Const.Shared + let legacy = shared end module Linearity = struct module Const = struct - type t = Many | Once + type t = + | Many + | Once let legacy = Many + let min = Many + let max = Once let le a b = - match (a, b) with Many, _ | _, Once -> true | Once, Many -> false + match a, b with Many, _ | _, Once -> true | Once, Many -> false let eq a b = - match (a, b) with + match a, b with | Many, Many | Once, Once -> true | Once, Many | Many, Once -> false let join a b = - match (a, b) with Once, _ | _, Once -> Once | Many, Many -> Many + match a, b with Once, _ | _, Once -> Once | Many, Many -> Many let meet a b = - match (a, b) with Many, _ | _, Many -> Many | Once, Once -> Once + match a, b with Many, _ | _, Many -> Many | Once, Once -> Once let print ppf = function | Once -> Format.fprintf ppf "Once" @@ -688,8 +783,11 @@ module Linearity = struct include DualSolver (Uniqueness.Const) (Uniqueness) (Const) let once = of_const Once + let many = of_const Many + let legacy = many + let constrain_legacy = constrain_lower end @@ -698,18 +796,16 @@ module Alloc = struct type t = (Locality.Const.t, Uniqueness.Const.t, Linearity.Const.t) modes let legacy = - { - locality = Locality.Const.legacy; + { locality = Locality.Const.legacy; uniqueness = Uniqueness.Const.legacy; - linearity = Linearity.Const.legacy; + linearity = Linearity.Const.legacy } let join { locality = loc1; uniqueness = u1; linearity = lin1 } { locality = loc2; uniqueness = u2; linearity = lin2 } = - { - locality = Locality.Const.join loc1 loc2; + { locality = Locality.Const.join loc1 loc2; uniqueness = Uniqueness.Const.join u1 u2; - linearity = Linearity.Const.join lin1 lin2; + linearity = Linearity.Const.join lin1 lin2 } (** constrain uncurried function ret_mode from arg_mode *) @@ -735,10 +831,9 @@ module Alloc = struct { locality; uniqueness; linearity } let min = - { - locality = Locality.Const.min; + { locality = Locality.Const.min; uniqueness = Uniqueness.Const.min; - linearity = Linearity.Const.min; + linearity = Linearity.Const.min } let min_with_uniqueness uniqueness = { min with uniqueness } @@ -747,23 +842,23 @@ module Alloc = struct type t = (Locality.t, Uniqueness.t, Linearity.t) modes let of_const { locality; uniqueness; linearity } : t = - { - locality = Locality.of_const locality; + { locality = Locality.of_const locality; uniqueness = Uniqueness.of_const uniqueness; - linearity = Linearity.of_const linearity; + linearity = Linearity.of_const linearity } let prod locality uniqueness linearity = { locality; uniqueness; linearity } let legacy = - { - locality = Locality.legacy; + { locality = Locality.legacy; uniqueness = Uniqueness.legacy; - linearity = Linearity.legacy; + linearity = Linearity.legacy } let local = { legacy with locality = Locality.local } + let unique = { legacy with uniqueness = Uniqueness.unique } + let local_unique = { local with uniqueness = Uniqueness.unique } let is_const { locality; uniqueness; linearity } = @@ -772,35 +867,38 @@ module Alloc = struct && Linearity.is_const linearity let min_mode : t = - { - locality = Locality.min_mode; + { locality = Locality.min_mode; uniqueness = Uniqueness.min_mode; - linearity = Linearity.min_mode; + linearity = Linearity.min_mode } let max_mode : t = - { - locality = Locality.max_mode; + { locality = Locality.max_mode; uniqueness = Uniqueness.max_mode; - linearity = Linearity.max_mode; + linearity = Linearity.max_mode } let locality t = t.locality + let uniqueness t = t.uniqueness + let linearity t = t.linearity - type error = [ `Locality | `Uniqueness | `Linearity ] + type error = + [ `Locality + | `Uniqueness + | `Linearity ] let submode { locality = loc1; uniqueness = u1; linearity = lin1 } { locality = loc2; uniqueness = u2; linearity = lin2 } = match Locality.submode loc1 loc2 with | Ok () -> ( - match Uniqueness.submode u1 u2 with - | Ok () -> ( - match Linearity.submode lin1 lin2 with - | Ok () -> Ok () - | Error () -> Error `Linearity) - | Error () -> Error `Uniqueness) + match Uniqueness.submode u1 u2 with + | Ok () -> ( + match Linearity.submode lin1 lin2 with + | Ok () -> Ok () + | Error () -> Error `Linearity) + | Error () -> Error `Uniqueness) | Error () -> Error `Locality let submode_exn ({ locality = loc1; uniqueness = u1; linearity = lin1 } : t) @@ -813,97 +911,90 @@ module Alloc = struct ({ locality = loc2; uniqueness = u2; linearity = lin2 } : t) = match Locality.equate loc1 loc2 with | Ok () -> ( - match Uniqueness.equate u1 u2 with - | Ok () -> ( - match Linearity.equate lin1 lin2 with - | Ok () -> Ok () - | Error () -> Error `Linearity) - | Error () -> Error `Uniqueness) + match Uniqueness.equate u1 u2 with + | Ok () -> ( + match Linearity.equate lin1 lin2 with + | Ok () -> Ok () + | Error () -> Error `Linearity) + | Error () -> Error `Uniqueness) | Error () -> Error `Locality let join ms : t = - { - locality = Locality.join (List.map (fun (t : t) -> t.locality) ms); + { locality = Locality.join (List.map (fun (t : t) -> t.locality) ms); uniqueness = Uniqueness.join (List.map (fun (t : t) -> t.uniqueness) ms); - linearity = Linearity.join (List.map (fun (t : t) -> t.linearity) ms); + linearity = Linearity.join (List.map (fun (t : t) -> t.linearity) ms) } let constrain_upper { locality; uniqueness; linearity } = - { - locality = Locality.constrain_upper locality; + { locality = Locality.constrain_upper locality; uniqueness = Uniqueness.constrain_upper uniqueness; - linearity = Linearity.constrain_upper linearity; + linearity = Linearity.constrain_upper linearity } let constrain_lower { locality; uniqueness; linearity } = - { - locality = Locality.constrain_lower locality; + { locality = Locality.constrain_lower locality; uniqueness = Uniqueness.constrain_lower uniqueness; - linearity = Linearity.constrain_lower linearity; + linearity = Linearity.constrain_lower linearity } (* constrain to the legacy modes*) let constrain_legacy { locality; uniqueness; linearity } = - { - locality = Locality.constrain_legacy locality; + { locality = Locality.constrain_legacy locality; uniqueness = Uniqueness.constrain_legacy uniqueness; - linearity = Linearity.constrain_legacy linearity; + linearity = Linearity.constrain_legacy linearity } let newvar () = - { - locality = Locality.newvar (); + { locality = Locality.newvar (); uniqueness = Uniqueness.newvar (); - linearity = Linearity.newvar (); + linearity = Linearity.newvar () } let newvar_below { locality; uniqueness; linearity } = let locality, changed1 = Locality.newvar_below locality in let uniqueness, changed2 = Uniqueness.newvar_below uniqueness in let linearity, changed3 = Linearity.newvar_below linearity in - ({ locality; uniqueness; linearity }, changed1 || changed2 || changed3) + { locality; uniqueness; linearity }, changed1 || changed2 || changed3 - let newvar_below_comonadic {locality; uniqueness; linearity} = + let newvar_below_comonadic { locality; uniqueness; linearity } = let locality, changed1 = Locality.newvar_below locality in let linearity, changed2 = Linearity.newvar_below linearity in - ({ locality; uniqueness; linearity }, changed1 || changed2) + { locality; uniqueness; linearity }, changed1 || changed2 let newvar_above { locality; uniqueness; linearity } = let locality, changed1 = Locality.newvar_above locality in let uniqueness, changed2 = Uniqueness.newvar_above uniqueness in let linearity, changed3 = Linearity.newvar_above linearity in - ({ locality; uniqueness; linearity }, changed1 || changed2 || changed3) + { locality; uniqueness; linearity }, changed1 || changed2 || changed3 let of_uniqueness uniqueness = - { - locality = Locality.newvar (); + { locality = Locality.newvar (); uniqueness; - linearity = Linearity.newvar (); + linearity = Linearity.newvar () } let of_locality locality = - { - locality; + { locality; uniqueness = Uniqueness.newvar (); - linearity = Linearity.newvar (); + linearity = Linearity.newvar () } let of_linearity linearity = - { - locality = Locality.newvar (); + { locality = Locality.newvar (); uniqueness = Uniqueness.newvar (); - linearity; + linearity } let with_locality locality t = { t with locality } + let with_uniqueness uniqueness t = { t with uniqueness } + let with_linearity linearity t = { t with linearity } let check_const { locality; uniqueness; linearity } = - { - locality = Locality.check_const locality; + { locality = Locality.check_const locality; uniqueness = Uniqueness.check_const uniqueness; - linearity = Linearity.check_const linearity; + linearity = Linearity.check_const linearity } let print' ?(verbose = true) ppf { locality; uniqueness; linearity } = @@ -924,13 +1015,11 @@ module Alloc = struct let uniqueness = Uniqueness.of_const Uniqueness.Const.min in let linearity = Linearity.join - [ - arg_mode.linearity; + [ arg_mode.linearity; (* In addition, unique argument make the returning function once. In other words, if argument <= unique, returning function >= once. That is, returning function >= (dual of argument) *) - Linearity.of_dual arg_mode.uniqueness; - ] + Linearity.of_dual arg_mode.uniqueness ] in { locality; uniqueness; linearity } @@ -949,37 +1038,39 @@ module Value = struct let r_as_l : t -> Alloc.Const.t = function | { locality; uniqueness; linearity } -> - let locality = Regionality.Const.r_as_l locality in - { locality; uniqueness; linearity } + let locality = Regionality.Const.r_as_l locality in + { locality; uniqueness; linearity } [@@warning "-unused-value-declaration"] let r_as_g : t -> Alloc.Const.t = function | { locality; uniqueness; linearity } -> - let locality = Regionality.Const.r_as_g locality in - { locality; uniqueness; linearity } + let locality = Regionality.Const.r_as_g locality in + { locality; uniqueness; linearity } [@@warning "-unused-value-declaration"] end type t = (Regionality.t, Uniqueness.t, Linearity.t) modes let legacy = - { - locality = Regionality.legacy; + { locality = Regionality.legacy; uniqueness = Uniqueness.legacy; - linearity = Linearity.legacy; + linearity = Linearity.legacy } let regional = { legacy with locality = Regionality.regional } + let local = { legacy with locality = Regionality.local } + let unique = { legacy with uniqueness = Uniqueness.unique } + let regional_unique = { regional with uniqueness = Uniqueness.unique } + let local_unique = { local with uniqueness = Uniqueness.unique } let of_const { locality; uniqueness; linearity } = - { - locality = Regionality.of_const locality; + { locality = Regionality.of_const locality; uniqueness = Uniqueness.of_const uniqueness; - linearity = Linearity.of_const linearity; + linearity = Linearity.of_const linearity } let max_mode = @@ -995,28 +1086,37 @@ module Value = struct { locality; uniqueness; linearity } let locality t = t.locality + let uniqueness t = t.uniqueness + let linearity t = t.linearity + let min_with_uniqueness u = { min_mode with uniqueness = u } + let max_with_uniqueness u = { max_mode with uniqueness = u } - let min_with_locality locality = - { min_mode with locality } + let min_with_locality locality = { min_mode with locality } - let max_with_locality locality = - { max_mode with locality } + let max_with_locality locality = { max_mode with locality } - let min_with_linearity linearity = - { min_mode with linearity } + let min_with_linearity linearity = { min_mode with linearity } let with_locality locality t = { t with locality } + let with_uniqueness uniqueness t = { t with uniqueness } + let with_linearity linearity t = { t with linearity } + let to_local t = { t with locality = Regionality.local } + let to_global t = { t with locality = Regionality.global } + let to_unique t = { t with uniqueness = Uniqueness.unique } + let to_shared t = { t with uniqueness = Uniqueness.shared } + let to_once t = { t with linearity = Linearity.once } + let to_many t = { t with linearity = Linearity.many } let of_alloc { locality; uniqueness; linearity } = @@ -1047,18 +1147,22 @@ module Value = struct let regional_to_local_locality t = Regionality.regional_to_local_locality t.locality - type error = [ `Regionality | `Locality | `Uniqueness | `Linearity ] + type error = + [ `Regionality + | `Locality + | `Uniqueness + | `Linearity ] let submode t1 t2 = match Regionality.submode t1.locality t2.locality with | Error _ as e -> e | Ok () -> ( - match Uniqueness.submode t1.uniqueness t2.uniqueness with - | Error () -> Error `Uniqueness - | Ok () -> ( - match Linearity.submode t1.linearity t2.linearity with - | Error () -> Error `Linearity - | Ok () as ok -> ok)) + match Uniqueness.submode t1.uniqueness t2.uniqueness with + | Error () -> Error `Uniqueness + | Ok () -> ( + match Linearity.submode t1.linearity t2.linearity with + | Error () -> Error `Linearity + | Ok () as ok -> ok)) let submode_exn t1 t2 = match submode t1 t2 with @@ -1069,20 +1173,20 @@ module Value = struct ({ locality = loc2; uniqueness = u2; linearity = lin2 } : t) = match Regionality.equate loc1 loc2 with | Ok () -> ( - match Uniqueness.equate u1 u2 with - | Ok () -> ( - match Linearity.equate lin1 lin2 with - | Ok () -> Ok () - | Error () -> Error `Linearity) - | Error () -> Error `Uniqueness) + match Uniqueness.equate u1 u2 with + | Ok () -> ( + match Linearity.equate lin1 lin2 with + | Ok () -> Ok () + | Error () -> Error `Linearity) + | Error () -> Error `Uniqueness) | Error e -> Error e let rec submode_meet t = function | [] -> Ok () | t' :: rest -> ( - match submode t t' with - | Ok () -> submode_meet t rest - | Error _ as err -> err) + match submode t t' with + | Ok () -> submode_meet t rest + | Error _ as err -> err) let join ts = let locality = Regionality.join (List.map (fun t -> t.locality) ts) in @@ -1112,13 +1216,13 @@ module Value = struct let locality, changed1 = Regionality.newvar_below locality in let uniqueness, changed2 = Uniqueness.newvar_below uniqueness in let linearity, changed3 = Linearity.newvar_below linearity in - ({ locality; uniqueness; linearity }, changed1 || changed2 || changed3) + { locality; uniqueness; linearity }, changed1 || changed2 || changed3 let newvar_above { locality; uniqueness; linearity } = let locality, changed1 = Regionality.newvar_above locality in let uniqueness, changed2 = Uniqueness.newvar_above uniqueness in let linearity, changed3 = Linearity.newvar_above linearity in - ({ locality; uniqueness; linearity }, changed1 || changed2 || changed3) + { locality; uniqueness; linearity }, changed1 || changed2 || changed3 let check_const t = let locality = Regionality.check_const t.locality in diff --git a/typing/mode.mli b/typing/mode.mli index d35ca486932..76ffa16cf57 100644 --- a/typing/mode.mli +++ b/typing/mode.mli @@ -16,170 +16,284 @@ type changes val undo_changes : changes -> unit + val change_log : (changes -> unit) ref module Locality : sig module Const : sig - type t = Global | Local + type t = + | Global + | Local val legacy : t + val min : t + val max : t + val le : t -> t -> bool + val join : t -> t -> t + val meet : t -> t -> t + val print : Format.formatter -> t -> unit end type t val legacy : t + val of_const : Const.t -> t + val global : t + val local : t + val submode : t -> t -> (unit, unit) result + val submode_exn : t -> t -> unit + val equate : t -> t -> (unit, unit) result + val join : t list -> t + val constrain_upper : t -> Const.t + val constrain_lower : t -> Const.t + val newvar : unit -> t + val newvar_below : t -> t * bool + val newvar_above : t -> t * bool + val check_const : t -> Const.t option + val print' : ?verbose:bool -> ?label:string -> Format.formatter -> t -> unit + val print : Format.formatter -> t -> unit end module Regionality : sig module Const : sig - type t = Global | Regional | Local + type t = + | Global + | Regional + | Local end type t - type error = [ `Regionality | `Locality ] + + type error = + [ `Regionality + | `Locality ] val global : t + val regional : t + val local : t + val submode : t -> t -> (unit, error) result + val of_locality : Locality.t -> t + val regional_to_local : t -> t + val global_to_regional : t -> t + val local_to_regional : t -> t + val regional_to_global : t -> t + val regional_to_global_locality : t -> Locality.t + val print : Format.formatter -> t -> unit end module Uniqueness : sig module Const : sig - type t = Unique | Shared + type t = + | Unique + | Shared val legacy : t + val min : t + val max : t + val le : t -> t -> bool + val join : t -> t -> t + val meet : t -> t -> t + val print : Format.formatter -> t -> unit end type t val legacy : t + val of_const : Const.t -> t + val unique : t + val shared : t + val submode : t -> t -> (unit, unit) result + val submode_exn : t -> t -> unit + val equate : t -> t -> (unit, unit) result + val join : t list -> t + val meet : t list -> t + val constrain_upper : t -> Const.t + val constrain_lower : t -> Const.t + val newvar : unit -> t + val newvar_below : t -> t * bool + val newvar_above : t -> t * bool + val check_const : t -> Const.t option + val print' : ?verbose:bool -> ?label:string -> Format.formatter -> t -> unit + val print : Format.formatter -> t -> unit end module Linearity : sig module Const : sig - type t = Many | Once + type t = + | Many + | Once val legacy : t + val min : t + val max : t + val le : t -> t -> bool + val join : t -> t -> t + val meet : t -> t -> t + val print : Format.formatter -> t -> unit + val to_dual : t -> Uniqueness.Const.t + val of_dual : Uniqueness.Const.t -> t end type t val legacy : t + val of_const : Const.t -> t + val to_dual : t -> Uniqueness.t + val of_dual : Uniqueness.t -> t + val once : t + val many : t + val submode : t -> t -> (unit, unit) result + val submode_exn : t -> t -> unit + val equate : t -> t -> (unit, unit) result + val join : t list -> t + val constrain_upper : t -> Const.t + val constrain_lower : t -> Const.t + val newvar : unit -> t + val newvar_below : t -> t * bool + val newvar_above : t -> t * bool + val check_const : t -> Const.t option + val print' : ?verbose:bool -> ?label:string -> Format.formatter -> t -> unit + val print : Format.formatter -> t -> unit end -type ('a, 'b, 'c) modes = { locality : 'a; uniqueness : 'b; linearity : 'c } +type ('a, 'b, 'c) modes = + { locality : 'a; + uniqueness : 'b; + linearity : 'c + } module Alloc : sig module Const : sig type t = (Locality.Const.t, Uniqueness.Const.t, Linearity.Const.t) modes val legacy : t + val join : t -> t -> t + val close_over : t -> t + val partial_apply : t -> t + val min_with_uniqueness : Uniqueness.Const.t -> t end type t val legacy : t + val local : t + val unique : t + val local_unique : t + val prod : Locality.t -> Uniqueness.t -> Linearity.t -> t val of_const : Const.t -> t + val is_const : t -> bool + val min_mode : t + val max_mode : t (** Projections to Locality, Uniqueness and Linearity *) val locality : t -> Locality.t + val uniqueness : t -> Uniqueness.t + val linearity : t -> Linearity.t - type error = [ `Locality | `Uniqueness | `Linearity ] + type error = + [ `Locality + | `Uniqueness + | `Linearity ] val submode : t -> t -> (unit, error) result + val submode_exn : t -> t -> unit + val equate : t -> t -> (unit, error) result + val join : t list -> t (* Force a mode variable to its upper bound *) @@ -190,18 +304,26 @@ module Alloc : sig (* Force a mode variable to legacys *) val constrain_legacy : t -> Const.t + val newvar : unit -> t + val newvar_below : t -> t * bool (* Same as [newvar_below] but only on the comonadic axes *) val newvar_below_comonadic : t -> t * bool val newvar_above : t -> t * bool + val with_locality : Locality.t -> t -> t + val with_uniqueness : Uniqueness.t -> t -> t + val with_linearity : Linearity.t -> t -> t + val of_uniqueness : Uniqueness.t -> t + val of_locality : Locality.t -> t + val of_linearity : Linearity.t -> t val check_const : @@ -212,8 +334,11 @@ module Alloc : sig modes val print' : ?verbose:bool -> Format.formatter -> t -> unit + val print : Format.formatter -> t -> unit + val close_over : t -> t + val partial_apply : t -> t end @@ -225,13 +350,21 @@ module Value : sig type t val legacy : t + val regional : t + val local : t + val unique : t + val regional_unique : t + val local_unique : t + val of_const : Const.t -> t + val max_mode : t + val min_mode : t (** Injections from Locality and Uniqueness into [Value_mode.t] *) @@ -239,53 +372,66 @@ module Value : sig (* The 'min_with_*' functions extend the min_mode, the 'max_with_' functions extend the max_mode, the 'with_*' functions extend given mode. - *) + *) val min_with_uniqueness : Uniqueness.t -> t + val max_with_uniqueness : Uniqueness.t -> t + val min_with_locality : Regionality.t -> t + val max_with_locality : Regionality.t -> t + val min_with_linearity : Linearity.t -> t + val with_locality : Regionality.t -> t -> t + val with_uniqueness : Uniqueness.t -> t -> t + val with_linearity : Linearity.t -> t -> t (** Projections to Locality, Uniqueness and Linearity *) val locality : t -> Regionality.t + val uniqueness : t -> Uniqueness.t + val linearity : t -> Linearity.t (** Injections from [Alloc.t] into [Value_mode.t] *) - val of_alloc : Alloc.t -> t (** [of_alloc] maps [Global] to [Global] and [Local] to [Local] *) + val of_alloc : Alloc.t -> t (** Kernel operators *) - val local_to_regional : t -> t (** The kernel operator [local_to_regional] maps [Local] to [Regional] and leaves the others unchanged. *) + val local_to_regional : t -> t - val regional_to_global : t -> t (** The kernel operator [regional_to_global] maps [Regional] to [Global] and leaves the others unchanged. *) + val regional_to_global : t -> t val to_global : t -> t + val to_unique : t -> t + val to_many : t -> t (** Closure operators *) - val regional_to_local : t -> t (** The closure operator [regional_to_local] maps [Regional] to [Local] and leaves the others unchanged. *) + val regional_to_local : t -> t - val global_to_regional : t -> t (** The closure operator [global_to_regional] maps [Global] to [Regional] and leaves the others unchanged. *) + val global_to_regional : t -> t val to_local : t -> t + val to_shared : t -> t + val to_once : t -> t (** Note that the kernal and closure operators are in the following @@ -313,29 +459,42 @@ module Value : sig (** Versions of the operators that return [Alloc.t] *) - val regional_to_global_alloc : t -> Alloc.t (** Maps [Regional] to [Global] and leaves the others unchanged. *) + val regional_to_global_alloc : t -> Alloc.t - val regional_to_local_alloc : t -> Alloc.t (** Maps [Regional] to [Local] and leaves the others unchanged. *) + val regional_to_local_alloc : t -> Alloc.t - val regional_to_global_locality : t -> Locality.t (** Maps [Regional] to [Global] *) + val regional_to_global_locality : t -> Locality.t - val regional_to_local_locality : t -> Locality.t (** Maps [Regional] to [Local] *) + val regional_to_local_locality : t -> Locality.t - type error = [ `Regionality | `Locality | `Uniqueness | `Linearity ] + type error = + [ `Regionality + | `Locality + | `Uniqueness + | `Linearity ] val submode : t -> t -> (unit, error) result + val submode_exn : t -> t -> unit + val equate : t -> t -> (unit, error) result + val submode_meet : t -> t list -> (unit, error) result + val join : t list -> t + val constrain_upper : t -> Const.t + val constrain_lower : t -> Const.t + val newvar : unit -> t + val newvar_below : t -> t * bool + val newvar_above : t -> t * bool val check_const : @@ -346,5 +505,6 @@ module Value : sig modes val print' : ?verbose:bool -> Format.formatter -> t -> unit + val print : Format.formatter -> t -> unit end diff --git a/typing/uniqueness_analysis.ml b/typing/uniqueness_analysis.ml index 98bb63a2c4f..93f4368f304 100644 --- a/typing/uniqueness_analysis.ml +++ b/typing/uniqueness_analysis.ml @@ -22,9 +22,9 @@ module Uniqueness = Mode.Uniqueness module Linearity = Mode.Linearity module Occurrence = struct - type t = { loc : Location.t } (** The occurrence of a potentially unique ident in the expression. Currently it's just the location; might add more things in the future *) + type t = { loc : Location.t } let mk loc = { loc } end @@ -34,32 +34,36 @@ let rec iter_error f = function | x :: xs -> ( match f x with Ok () -> iter_error f xs | Error e -> Error e) module Maybe_unique : sig - type t (** The type representing a usage that could be either unique or shared *) + type t - val extract_occurrence : t -> Occurrence.t (** extract an arbitrary occurrence from this usage *) + val extract_occurrence : t -> Occurrence.t - val singleton : unique_use -> Occurrence.t -> t (** construct a single usage *) + val singleton : unique_use -> Occurrence.t -> t val meet : t -> t -> t - type axis = Uniqueness | Linearity + type axis = + | Uniqueness + | Linearity - type cannot_force = { occ : Occurrence.t; axis : axis } (** Describes why cannot force shared - including the failing occurrence, and the failing axis *) + type cannot_force = + { occ : Occurrence.t; + axis : axis + } - val mark_multi_use : t -> (unit, cannot_force) result (** Call this function to indicate that this is used multiple times *) + val mark_multi_use : t -> (unit, cannot_force) result - val uniqueness : t -> Uniqueness.t (** Returns the uniqueness represented by this usage. If this identifier is expected to be unique in any branch, it will return unique. If the current usage is forced, it will return shared. *) + val uniqueness : t -> Uniqueness.t end = struct - type t = (unique_use * Occurrence.t) list (** Occurrences with modes to be forced shared and many in the future if needed. This is a list because of multiple control flows. For example, if a value is used shared in one branch but unique in another branch, then @@ -68,12 +72,20 @@ end = struct modes in the lists. (recall that shared > unique). Therefore, if this virtual mode needs to be forced shared, the whole list needs to be forced shared. *) + type t = (unique_use * Occurrence.t) list + + let singleton unique_use occ : t = [unique_use, occ] - let singleton unique_use occ : t = [ (unique_use, occ) ] let uniqueness l = Uniqueness.meet (List.map (fun ((uniq, _), _) -> uniq) l) - type axis = Uniqueness | Linearity - type cannot_force = { occ : Occurrence.t; axis : axis } + type axis = + | Uniqueness + | Linearity + + type cannot_force = + { occ : Occurrence.t; + axis : axis + } let mark_multi_use l = let force_one ((uni, lin), occ) = @@ -83,42 +95,48 @@ end = struct match Linearity.submode lin Linearity.many with | Error () -> Error { occ; axis = Linearity } | Ok () -> ( - match Uniqueness.submode Uniqueness.shared uni with - | Ok () -> Ok () - | Error () -> Error { occ; axis = Uniqueness }) + match Uniqueness.submode Uniqueness.shared uni with + | Ok () -> Ok () + | Error () -> Error { occ; axis = Uniqueness }) in iter_error force_one l let extract_occurrence = function [] -> assert false | (_, occ) :: _ -> occ + let meet l0 l1 = l0 @ l1 end module Maybe_shared : sig type t - type access = Read | Write + + type access = + | Read + | Write val string_of_access : access -> string (** The type representing a usage that could be either shared or borrowed *) - val extract_occurrence_access : t -> Occurrence.t * access (** Extract an arbitrary occurrence from the usage *) + val extract_occurrence_access : t -> Occurrence.t * access - val set_barrier : t -> Uniqueness.t -> unit (** set a barrier. The uniqueness mode represents the usage immediately following the current usage. If that mode is Unique, the current usage must be Borrowed (hence no code motion); if that mode is not restricted to Unique, this usage can be Borrowed or Shared (prefered). Raise if called more than once. *) + val set_barrier : t -> Uniqueness.t -> unit val meet : t -> t -> t + val singleton : unique_barrier ref -> Occurrence.t -> access -> t end = struct - type access = Read | Write + type access = + | Read + | Write let string_of_access = function Read -> "read from" | Write -> "written to" - type t = (unique_barrier ref * Occurrence.t * access) list (** list of occurences together with modes to be forced as borrowed in the future if needed. It is a list because of multiple control flows. For example, if a value is used borrowed in one branch but shared in another, @@ -126,13 +144,15 @@ end = struct is the meet of all modes in the list. (recall that borrowed > shared). Therefore, if this virtual mode needs to be forced borrowed, the whole list needs to be forced borrowed. *) + type t = (unique_barrier ref * Occurrence.t * access) list let meet l0 l1 = l0 @ l1 - let singleton r occ access = [ (r, occ, access) ] + + let singleton r occ access = [r, occ, access] let extract_occurrence_access = function | [] -> assert false - | (_, occ, access) :: _ -> (occ, access) + | (_, occ, access) :: _ -> occ, access let set_barrier t uniq = List.iter @@ -153,18 +173,25 @@ module Shared : sig (** shared because lifted from implicit borrowing, carries the original access *) - val singleton : Occurrence.t -> reason -> t (** The occurrence is only for future error messages. The share_reason must corresponds to the occurrence *) + val singleton : Occurrence.t -> reason -> t val extract_occurrence : t -> Occurrence.t + val reason : t -> reason end = struct - type reason = Forced | Lazy | Lifted of Maybe_shared.access + type reason = + | Forced + | Lazy + | Lifted of Maybe_shared.access + type t = Occurrence.t * reason - let singleton occ reason = (occ, reason) + let singleton occ reason = occ, reason + let extract_occurrence (occ, _) = occ + let reason (_, reason) = reason end @@ -182,30 +209,33 @@ module Usage : sig (** A usage that could be either unique or shared. *) val shared : Occurrence.t -> Shared.reason -> t + val maybe_unique : unique_use -> Occurrence.t -> t - val extract_occurrence : t -> Occurrence.t option (** Extract an arbitrary occurrence from a usage *) + val extract_occurrence : t -> Occurrence.t option - type first_or_second = First | Second + type first_or_second = + | First + | Second - type error = { - cannot_force : Maybe_unique.cannot_force; - there : t; (** The other usage *) - first_or_second : first_or_second; - (** Is it the first or second usage that's failing force? *) - } + type error = + { cannot_force : Maybe_unique.cannot_force; + there : t; (** The other usage *) + first_or_second : first_or_second + (** Is it the first or second usage that's failing force? *) + } exception Error of error - val seq : t -> t -> t (** Sequential composition *) + val seq : t -> t -> t - val choose : t -> t -> t (** Non-deterministic choice *) + val choose : t -> t -> t - val par : t -> t -> t (** Parallel composition *) + val par : t -> t -> t end = struct (* We have Unused (top) > Borrowed > Shared > Unique > Error (bot). @@ -279,23 +309,23 @@ end = struct | Maybe_unique t -> Some (Maybe_unique.extract_occurrence t) let choose m0 m1 = - match (m0, m1) with + match m0, m1 with | Unused, m | m, Unused -> m | Borrowed _, t | t, Borrowed _ -> t - | Maybe_shared l0, Maybe_shared l1 -> - Maybe_shared (Maybe_shared.meet l0 l1) + | Maybe_shared l0, Maybe_shared l1 -> Maybe_shared (Maybe_shared.meet l0 l1) | Maybe_shared _, t | t, Maybe_shared _ -> t | Shared _, t | t, Shared _ -> t - | Maybe_unique l0, Maybe_unique l1 -> - Maybe_unique (Maybe_unique.meet l0 l1) + | Maybe_unique l0, Maybe_unique l1 -> Maybe_unique (Maybe_unique.meet l0 l1) - type first_or_second = First | Second + type first_or_second = + | First + | Second - type error = { - cannot_force : Maybe_unique.cannot_force; - there : t; - first_or_second : first_or_second; - } + type error = + { cannot_force : Maybe_unique.cannot_force; + there : t; + first_or_second : first_or_second + } exception Error of error @@ -303,105 +333,103 @@ end = struct match Maybe_unique.mark_multi_use t with | Ok () -> () | Error cannot_force -> - raise (Error { cannot_force; there; first_or_second }) + raise (Error { cannot_force; there; first_or_second }) let par m0 m1 = - match (m0, m1) with + match m0, m1 with | Unused, m | m, Unused -> m | Borrowed occ, Borrowed _ -> Borrowed occ | Borrowed _, Maybe_shared t | Maybe_shared t, Borrowed _ -> Maybe_shared t | Borrowed _, Shared t | Shared t, Borrowed _ -> Shared t | Borrowed occ, Maybe_unique t | Maybe_unique t, Borrowed occ -> - force_shared_multiuse t (Borrowed occ) First; - shared (Maybe_unique.extract_occurrence t) Shared.Forced - | Maybe_shared t0, Maybe_shared t1 -> - Maybe_shared (Maybe_shared.meet t0 t1) + force_shared_multiuse t (Borrowed occ) First; + shared (Maybe_unique.extract_occurrence t) Shared.Forced + | Maybe_shared t0, Maybe_shared t1 -> Maybe_shared (Maybe_shared.meet t0 t1) | Maybe_shared _, Shared occ | Shared occ, Maybe_shared _ -> - (* The barrier stays empty; if there is any unique after this, it - will error *) - Shared occ + (* The barrier stays empty; if there is any unique after this, it + will error *) + Shared occ | Maybe_shared t0, Maybe_unique t1 | Maybe_unique t1, Maybe_shared t0 -> - (* t1 must be shared *) - force_shared_multiuse t1 (Maybe_shared t0) First; - (* The barrier stays empty; if there is any unique after this, it will - error *) - shared (Maybe_unique.extract_occurrence t1) Shared.Forced + (* t1 must be shared *) + force_shared_multiuse t1 (Maybe_shared t0) First; + (* The barrier stays empty; if there is any unique after this, it will + error *) + shared (Maybe_unique.extract_occurrence t1) Shared.Forced | Shared t0, Shared _ -> Shared t0 | Shared t0, Maybe_unique t1 -> - force_shared_multiuse t1 (Shared t0) Second; - Shared t0 + force_shared_multiuse t1 (Shared t0) Second; + Shared t0 | Maybe_unique t1, Shared t0 -> - force_shared_multiuse t1 (Shared t0) First; - Shared t0 + force_shared_multiuse t1 (Shared t0) First; + Shared t0 | Maybe_unique t0, Maybe_unique t1 -> - force_shared_multiuse t0 m1 First; - force_shared_multiuse t1 m0 Second; - shared (Maybe_unique.extract_occurrence t0) Shared.Forced + force_shared_multiuse t0 m1 First; + force_shared_multiuse t1 m0 Second; + shared (Maybe_unique.extract_occurrence t0) Shared.Forced let seq m0 m1 = - match (m0, m1) with + match m0, m1 with | Unused, m | m, Unused -> m | Borrowed _, t -> t | Maybe_shared _, Borrowed _ -> m0 - | Maybe_shared l0, Maybe_shared l1 -> - Maybe_shared (Maybe_shared.meet l0 l1) + | Maybe_shared l0, Maybe_shared l1 -> Maybe_shared (Maybe_shared.meet l0 l1) | Maybe_shared _, Shared _ -> m1 | Maybe_shared l0, Maybe_unique l1 -> - (* Four cases (semi-colon meaning sequential composition): - Borrowed;Shared = Shared - Borrowed;Unique = Unique - Shared;Shared = Shared - Shared;Unique = Error - - We are in a dilemma: recall that Borrowed->Shared allows code - motion, and Shared->Unique allows unique overwriting. We can't have - both. We first note is that the first is a soft optimization, and - the second is a hard requirement. - - A reasonable solution is thus to check if the m1 actually needs - to use the "unique" capabilities. If not, there is no need to - relax it to Unique, and we will make it Shared, and make m0 - Shared for code-motion. However, there is no good way to do that, - because the "unique_use" in "maybe_unique" is not complete, - because the type-checking and uniqueness analysis is performed on - a per-top-level-expr basis. - - Our solution is to record on the m0 that it is constrained by the - m1. I.e. if m1 is Unique, then m0 cannot be Shared. After the type - checking of the whole file, m1 will correctly tells whether it needs - to be Unique, and by extension whether m0 can be Shared. *) - let uniq = Maybe_unique.uniqueness l1 in - Maybe_shared.set_barrier l0 uniq; - m1 + (* Four cases (semi-colon meaning sequential composition): + Borrowed;Shared = Shared + Borrowed;Unique = Unique + Shared;Shared = Shared + Shared;Unique = Error + + We are in a dilemma: recall that Borrowed->Shared allows code + motion, and Shared->Unique allows unique overwriting. We can't have + both. We first note is that the first is a soft optimization, and + the second is a hard requirement. + + A reasonable solution is thus to check if the m1 actually needs + to use the "unique" capabilities. If not, there is no need to + relax it to Unique, and we will make it Shared, and make m0 + Shared for code-motion. However, there is no good way to do that, + because the "unique_use" in "maybe_unique" is not complete, + because the type-checking and uniqueness analysis is performed on + a per-top-level-expr basis. + + Our solution is to record on the m0 that it is constrained by the + m1. I.e. if m1 is Unique, then m0 cannot be Shared. After the type + checking of the whole file, m1 will correctly tells whether it needs + to be Unique, and by extension whether m0 can be Shared. *) + let uniq = Maybe_unique.uniqueness l1 in + Maybe_shared.set_barrier l0 uniq; + m1 | Shared _, Borrowed _ -> m0 | Maybe_unique l, Borrowed occ -> - force_shared_multiuse l m1 First; - shared occ Shared.Forced + force_shared_multiuse l m1 First; + shared occ Shared.Forced | Shared _, Maybe_shared _ -> m0 | Maybe_unique l0, Maybe_shared l1 -> - (* Four cases: - Shared;Borrowed = Shared - Shared;Shared = Shared - Unique;Borrowed = Error - Unique;Shared = Error - - As you can see, we need to force the m0 to Shared, and m1 needn't - be constrained. The result is always Shared. - *) - let occ, _ = Maybe_shared.extract_occurrence_access l1 in - force_shared_multiuse l0 m1 First; - shared occ Shared.Forced + (* Four cases: + Shared;Borrowed = Shared + Shared;Shared = Shared + Unique;Borrowed = Error + Unique;Shared = Error + + As you can see, we need to force the m0 to Shared, and m1 needn't + be constrained. The result is always Shared. + *) + let occ, _ = Maybe_shared.extract_occurrence_access l1 in + force_shared_multiuse l0 m1 First; + shared occ Shared.Forced | Shared _, Shared _ -> m0 | Maybe_unique l, Shared _ -> - force_shared_multiuse l m1 First; - m1 + force_shared_multiuse l m1 First; + m1 | Shared _, Maybe_unique l -> - force_shared_multiuse l m0 Second; - m0 + force_shared_multiuse l m0 Second; + m0 | Maybe_unique l0, Maybe_unique l1 -> - force_shared_multiuse l0 m1 First; - force_shared_multiuse l1 m0 Second; - shared (Maybe_unique.extract_occurrence l0) Shared.Forced + force_shared_multiuse l0 m1 First; + force_shared_multiuse l1 m0 Second; + shared (Maybe_unique.extract_occurrence l0) Shared.Forced end module Projection : sig @@ -424,26 +452,26 @@ end = struct | Memory_address let compare t1 t2 = - match (t1, t2) with + match t1, t2 with | Tuple_field i, Tuple_field j -> Int.compare i j | Record_field l1, Record_field l2 -> String.compare l1 l2 | Construct_field (l1, i), Construct_field (l2, j) -> ( - match String.compare l1 l2 with 0 -> Int.compare i j | i -> i) + match String.compare l1 l2 with 0 -> Int.compare i j | i -> i) | Variant_field l1, Variant_field l2 -> String.compare l1 l2 | Memory_address, Memory_address -> 0 | ( Tuple_field _, (Record_field _ | Construct_field _ | Variant_field _ | Memory_address) ) -> - -1 + -1 | ( (Record_field _ | Construct_field _ | Variant_field _ | Memory_address), Tuple_field _ ) -> - 1 + 1 | Record_field _, (Construct_field _ | Variant_field _ | Memory_address) -> - -1 + -1 | (Construct_field _ | Variant_field _ | Memory_address), Record_field _ -> - 1 + 1 | Construct_field _, (Variant_field _ | Memory_address) -> -1 | (Variant_field _ | Memory_address), Construct_field _ -> 1 | Variant_field _, Memory_address -> -1 @@ -467,51 +495,50 @@ type relation = | Descendant of Projection.t list type error = - | Usage of { - inner : Usage.error; - (** Describes the error concerning the two usages *) - first_is_of_second : relation; - (** The relation between the two usages in the tree *) - } - | Boundary of { - cannot_force : Maybe_unique.cannot_force; - reason : boundary_reason; - } + | Usage of + { inner : Usage.error; + (** Describes the error concerning the two usages *) + first_is_of_second : relation + (** The relation between the two usages in the tree *) + } + | Boundary of + { cannot_force : Maybe_unique.cannot_force; + reason : boundary_reason + } exception Error of error (** lifting module Usage to trees *) module Usage_tree : sig module Path : sig - type t (** Represents a path from the root to a node in a tree *) + type t - val child : Projection.t -> t -> t (** Constructing a child path *) + val child : Projection.t -> t -> t - val root : t (** The path representing the root node *) + val root : t end - type t (** Usage tree, lifted from [Usage.t] *) + type t - val seq : t -> t -> t (** Sequential composition lifted from [Usage.seq] *) + val seq : t -> t -> t - val choose : t -> t -> t (** Non-deterministic choice lifted from [Usage.choose] *) + val choose : t -> t -> t - val par : t -> t -> t (** Parallel composition lifted from [Usage.par] *) + val par : t -> t -> t - val singleton : Usage.t -> Path.t -> t (** A singleton tree containing only one leaf *) + val singleton : Usage.t -> Path.t -> t - val mapi : (Path.t -> Usage.t -> Usage.t) -> t -> t (** Runs a function through the tree; the function must be monotone *) + val mapi : (Path.t -> Usage.t -> Usage.t) -> t -> t end = struct - type t = { children : t Projection.Map.t; usage : Usage.t } (** Represents a tree of usage. Each node records the choose on all possible execution paths. As a result, trees such as `S -> U` is valid, even though it would be invalid if it was the result of a single path: using a parent @@ -522,11 +549,16 @@ end = struct unique parent is nonsense. The invariant is preserved because Usage.choose, Usage.par, and Usage.seq above are monotone, and Usage_tree.par and Usage_tree.seq, Usage_tree.choose here are node-wise. *) + type t = + { children : t Projection.Map.t; + usage : Usage.t + } module Path = struct type t = Projection.t list - let child (a : Projection.t) (p : t) : t = p @ [ a ] + let child (a : Projection.t) (p : t) : t = p @ [a] + let root : t = [] end @@ -547,18 +579,18 @@ end = struct let children = Projection.Map.merge (fun proj c0 c1 -> - match (c0, c1) with + match c0, c1 with | None, None -> assert false | None, Some c1 -> - Some - (mapi_aux [ proj ] - (fun projs r -> f (Ancestor projs) t0.usage r) - c1) + Some + (mapi_aux [proj] + (fun projs r -> f (Ancestor projs) t0.usage r) + c1) | Some c0, None -> - Some - (mapi_aux [ proj ] - (fun projs l -> f (Descendant projs) l t1.usage) - c0) + Some + (mapi_aux [proj] + (fun projs l -> f (Descendant projs) l t1.usage) + c0) | Some c0, Some c1 -> Some (mapi2 f c0 c1)) t0.children t1.children in @@ -573,16 +605,17 @@ end = struct t0 t1 let choose t0 t1 = lift Usage.choose t0 t1 + let seq t0 t1 = lift Usage.seq t0 t1 + let par t0 t1 = lift Usage.par t0 t1 let rec singleton leaf = function | [] -> { usage = leaf; children = Projection.Map.empty } | proj :: path -> - { - usage = Unused; - children = Projection.Map.singleton proj (singleton leaf path); - } + { usage = Unused; + children = Projection.Map.singleton proj (singleton leaf path) + } end (** Lift Usage_tree to forest *) @@ -590,37 +623,39 @@ module Usage_forest : sig module Path : sig type t - val child : Projection.t -> t -> t (** Construct a child path from a parent *) + val child : Projection.t -> t -> t - val fresh_root : unit -> t (** Create a fresh tree in the forest *) + val fresh_root : unit -> t end - type t (** Represents a forest of usage. *) + type t - val seq : t -> t -> t (** Similar to [Usage_tree.seq] but lifted to forests *) + val seq : t -> t -> t - val choose : t -> t -> t (** Similar to [Usage_tree.choose] but lifted to forests *) + val choose : t -> t -> t - val par : t -> t -> t (** Similar to [Usage_tree.par] but lifted to forests *) + val par : t -> t -> t val seqs : t list -> t + val chooses : t list -> t + val pars : t list -> t - val unused : t (** The empty forest *) + val unused : t - val singleton : Usage.t -> Path.t -> t (** The forest with only one usage, given by the path and the usage *) + val singleton : Usage.t -> Path.t -> t - val map : (Usage.t -> Usage.t) -> t -> t (** Run a function through a forest. The function must be monotone *) + val map : (Usage.t -> Usage.t) -> t -> t end = struct module Root_id = struct module T = struct @@ -647,9 +682,9 @@ end = struct type t = Root_id.t * Usage_tree.Path.t let child proj ((rootid, path) : t) : t = - (rootid, Usage_tree.Path.child proj path) + rootid, Usage_tree.Path.child proj path - let fresh_root () : t = (Root_id.fresh (), Usage_tree.Path.root) + let fresh_root () : t = Root_id.fresh (), Usage_tree.Path.root end let unused = Root_id.Map.empty @@ -658,7 +693,7 @@ end = struct let map2 f t0 t1 = Root_id.Map.merge (fun _rootid t0 t1 -> - match (t0, t1) with + match t0, t1 with | None, None -> assert false | None, Some t1 -> Some t1 | Some t0, None -> Some t0 @@ -666,10 +701,15 @@ end = struct t0 t1 let choose t0 t1 = map2 Usage_tree.choose t0 t1 + let seq t0 t1 = map2 Usage_tree.seq t0 t1 + let par t0 t1 = map2 Usage_tree.par t0 t1 + let chooses l = List.fold_left choose unused l + let seqs l = List.fold_left seq unused l + let pars l = List.fold_left par unused l let singleton leaf ((rootid, path') : Path.t) = @@ -686,39 +726,41 @@ module UF = Usage_forest module Paths : sig [@@@warning "-unused-value-declaration"] - type t (** Represents a list of [UF.Path.t] *) + type t - val child : Projection.t -> t -> t (** Returns the element-wise child *) + val child : Projection.t -> t -> t - val untracked : t (** Representing values whose modes are managed by the type checker. They are ignored by uniqueness analysis and represented as empty lists *) + val untracked : t - val modal_child : global_flag -> Projection.t -> t -> t (** [modal_child gf proj t] is [child prof t] when [gf] is [Unrestricted] and is [untracked] otherwise. *) + val modal_child : global_flag -> Projection.t -> t -> t - val tuple_field : int -> t -> t (** [tuple_field i t] is [child (Projection.Tuple_field i) t]. *) + val tuple_field : int -> t -> t - val record_field : global_flag -> string -> t -> t (** [record_field gf s t] is [modal_child gf (Projection.Record_field s) t]. *) + val record_field : global_flag -> string -> t -> t - val construct_field : global_flag -> string -> int -> t -> t (** [construct_field gf s i t] is [modal_child gf (Projection.Construct_field(s, i)) t]. *) + val construct_field : global_flag -> string -> int -> t -> t - val variant_field : string -> t -> t (** [variant_field s t] is [child (Projection.Variant_field s) t]. *) + val variant_field : string -> t -> t - val memory_address : t -> t (** [memory_address t] is [child Projection.Memory_address t]. *) + val memory_address : t -> t val mark : Usage.t -> t -> UF.t + val fresh : unit -> t + val choose : t -> t -> t val mark_implicit_borrow_memory_address : @@ -729,24 +771,28 @@ end = struct type t = UF.Path.t list let choose a b = a @ b + let untracked = [] + let child proj t = List.map (UF.Path.child proj) t let modal_child gf proj t = - match gf with - | Global -> untracked - | Unrestricted -> child proj t + match gf with Global -> untracked | Unrestricted -> child proj t let tuple_field i t = child (Projection.Tuple_field i) t + let record_field gf s t = modal_child gf (Projection.Record_field s) t let construct_field gf s i t = modal_child gf (Projection.Construct_field (s, i)) t let variant_field s t = child (Projection.Variant_field s) t + let memory_address t = child Projection.Memory_address t + let mark usage t = UF.chooses (List.map (UF.singleton usage) t) - let fresh () = [ UF.Path.fresh_root () ] + + let fresh () = [UF.Path.fresh_root ()] let mark_implicit_borrow_memory_address access occ paths = (* Currently we just generate a dummy unique_barrier ref that won't be @@ -767,114 +813,117 @@ let force_shared_boundary unique_use occ ~reason = | Error cannot_force -> raise (Error (Boundary { cannot_force; reason })) module Value : sig - type t (** See [mk] for its meaning *) + type t - val existing : Paths.t -> unique_use -> Occurrence.t -> t (** A value contains the list of paths it could points to, the unique_use if it's a variable, and its occurrence in the source code. [unique_use] could be None if it's not a variable (e.g. result of an application) *) + val existing : Paths.t -> unique_use -> Occurrence.t -> t - val fresh : t (** A value not yet being existing by the analysis *) + val fresh : t - val untracked : unique_use -> Occurrence.t -> t (** The untracked value, lifted from [Paths.untracked] *) + val untracked : unique_use -> Occurrence.t -> t - val paths : t -> Paths.t option (** [paths t] is [None] if [t] is fresh and [Some p] if [t] is existing where [p] are its associated paths *) + val paths : t -> Paths.t option - val implicit_record_field : global_flag -> string -> t -> unique_use -> t (** [implicit_record_field gf s t u] is [fresh] if [t] is [fresh], otherwise it is [existing (Paths.record_field gf s p) o u] where [p] are the paths of [t] and [o] is [t]'s occurrence. This is used for the implicit record field values for kept fields in a [{ foo with ... }] expression. *) + val implicit_record_field : global_flag -> string -> t -> unique_use -> t - val mark_maybe_unique : t -> UF.t (** Mark the value as shared_or_unique *) + val mark_maybe_unique : t -> UF.t - val mark_implicit_borrow_memory_address : Maybe_shared.access -> t -> UF.t (** Mark the memory_address of the value as implicitly borrowed (borrow_or_shared). We still ask for the [occ] argument, because [Value.occ] is the occurrence of the value, not necessary the place where it is borrowed. *) + val mark_implicit_borrow_memory_address : Maybe_shared.access -> t -> UF.t val mark_shared : reason:boundary_reason -> t -> UF.t end = struct type t = | Fresh - | Existing of { - paths : Paths.t; - unique_use : unique_use; - occ : Occurrence.t; - } + | Existing of + { paths : Paths.t; + unique_use : unique_use; + occ : Occurrence.t + } let existing paths unique_use occ = Existing { paths; unique_use; occ } + let fresh = Fresh + let paths = function Fresh -> None | Existing { paths; _ } -> Some paths + let untracked unique_use occ = existing Paths.untracked unique_use occ let implicit_record_field gf s t unique_use = match t with | Fresh -> Fresh | Existing { paths; occ; unique_use = _ } -> - let paths = Paths.record_field gf s paths in - Existing { paths; occ; unique_use } + let paths = Paths.record_field gf s paths in + Existing { paths; occ; unique_use } let mark_implicit_borrow_memory_address access = function | Fresh -> UF.unused | Existing { paths; occ; _ } -> - Paths.mark_implicit_borrow_memory_address access occ paths + Paths.mark_implicit_borrow_memory_address access occ paths let mark_maybe_unique = function | Fresh -> UF.unused | Existing { paths; unique_use; occ } -> - Paths.mark (Usage.maybe_unique unique_use occ) paths + Paths.mark (Usage.maybe_unique unique_use occ) paths let mark_shared ~reason = function | Fresh -> UF.unused | Existing { paths; unique_use; occ } -> - force_shared_boundary unique_use occ ~reason; - let shared = Usage.shared occ Shared.Forced in - Paths.mark shared paths + force_shared_boundary unique_use occ ~reason; + let shared = Usage.shared occ Shared.Forced in + Paths.mark shared paths end module Ienv : sig module Extension : sig - type t (** Extention to Ienv. Usually generated by a pattern *) + type t - val disjunct : t -> t -> t (** Composition for [OR] patterns. This operation is commutative *) + val disjunct : t -> t -> t - val conjunct : t -> t -> t (** Composition for conjunctive patterns. The two extensions must be disjoint. *) + val conjunct : t -> t -> t - val conjuncts : t list -> t (** Similar to [conjunct] but lifted to lists *) + val conjuncts : t list -> t - val empty : t (** The empty extension *) + val empty : t val singleton : Ident.t -> Paths.t -> t (* Constructing a mapping with only one mapping *) end - type t (** Mapping from identifiers to a list of possible nodes, each represented by a path into the forest, instead of directly ponting to the node. *) + type t - val extend : t -> Extension.t -> t (** Extend a mapping with an extension *) + val extend : t -> Extension.t -> t - val empty : t (** The empty mapping *) + val empty : t - val find_opt : Ident.t -> t -> Paths.t option (** Find the list of paths corresponding to an identifier *) + val find_opt : Ident.t -> t -> Paths.t option end = struct module Extension = struct type t = Paths.t Ident.Map.t @@ -882,7 +931,7 @@ end = struct let disjunct ienv0 ienv1 = Ident.Map.merge (fun _id locs0 locs1 -> - match (locs0, locs1) with + match locs0, locs1 with | None, None -> None | Some paths0, Some paths1 -> Some (Paths.choose paths0 paths1) (* cannot bind variable only in one of the OR-patterns *) @@ -899,6 +948,7 @@ end = struct ienv0 ienv1 let conjuncts = List.fold_left conjunct empty + let singleton id locs = Ident.Map.singleton id locs end @@ -930,112 +980,112 @@ type value_to_match = let conjuncts_pattern_match l = let exts, ufs = List.split l in - (Ienv.Extension.conjuncts exts, UF.pars ufs) + Ienv.Extension.conjuncts exts, UF.pars ufs let rec pattern_match_tuple pat values = match pat.pat_desc with | Tpat_or (pat0, pat1, _) -> - let ext0, uf0 = pattern_match_tuple pat0 values in - let ext1, uf1 = pattern_match_tuple pat1 values in - (Ienv.Extension.disjunct ext0 ext1, UF.choose uf0 uf1) + let ext0, uf0 = pattern_match_tuple pat0 values in + let ext1, uf1 = pattern_match_tuple pat1 values in + Ienv.Extension.disjunct ext0 ext1, UF.choose uf0 uf1 | Tpat_tuple pats -> - List.map2 - (fun pat value -> - let paths = - match Value.paths value with - | None -> Paths.fresh () - | Some paths -> paths - in - pattern_match_single pat paths) - pats values - |> conjuncts_pattern_match + List.map2 + (fun pat value -> + let paths = + match Value.paths value with + | None -> Paths.fresh () + | Some paths -> paths + in + pattern_match_single pat paths) + pats values + |> conjuncts_pattern_match | _ -> - (* Mark all values in the tuple as used, because we are binding the tuple - to a variable *) - let uf = UF.seqs (List.map Value.mark_maybe_unique values) in - let paths = Paths.fresh () in - let ext, uf' = pattern_match_single pat paths in - (ext, UF.seq uf uf') + (* Mark all values in the tuple as used, because we are binding the tuple + to a variable *) + let uf = UF.seqs (List.map Value.mark_maybe_unique values) in + let paths = Paths.fresh () in + let ext, uf' = pattern_match_single pat paths in + ext, UF.seq uf uf' and pattern_match_single pat paths : Ienv.Extension.t * UF.t = let loc = pat.pat_loc in let occ = Occurrence.mk loc in match pat.pat_desc with | Tpat_or (pat0, pat1, _) -> - let ext0, uf0 = pattern_match_single pat0 paths in - let ext1, uf1 = pattern_match_single pat1 paths in - (Ienv.Extension.disjunct ext0 ext1, UF.choose uf0 uf1) - | Tpat_any -> (Ienv.Extension.empty, UF.unused) - | Tpat_var (id, _, _, _) -> (Ienv.Extension.singleton id paths, UF.unused) + let ext0, uf0 = pattern_match_single pat0 paths in + let ext1, uf1 = pattern_match_single pat1 paths in + Ienv.Extension.disjunct ext0 ext1, UF.choose uf0 uf1 + | Tpat_any -> Ienv.Extension.empty, UF.unused + | Tpat_var (id, _, _, _) -> Ienv.Extension.singleton id paths, UF.unused | Tpat_alias (pat', id, _, _, _) -> - let ext0 = Ienv.Extension.singleton id paths in - let ext1, uf = pattern_match_single pat' paths in - (Ienv.Extension.conjunct ext0 ext1, uf) + let ext0 = Ienv.Extension.singleton id paths in + let ext1, uf = pattern_match_single pat' paths in + Ienv.Extension.conjunct ext0 ext1, uf | Tpat_constant _ -> - ( Ienv.Extension.empty, - Paths.mark_implicit_borrow_memory_address Read occ paths ) + ( Ienv.Extension.empty, + Paths.mark_implicit_borrow_memory_address Read occ paths ) | Tpat_construct (lbl, cd, pats, _) -> - let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in - let pats_args = List.combine pats cd.cstr_args in - let ext, uf_pats = - List.mapi - (fun i (pat, (_, gf)) -> - let name = Longident.last lbl.txt in - let paths = Paths.construct_field gf name i paths in - pattern_match_single pat paths) - pats_args - |> conjuncts_pattern_match - in - (ext, UF.par uf_read uf_pats) + let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in + let pats_args = List.combine pats cd.cstr_args in + let ext, uf_pats = + List.mapi + (fun i (pat, (_, gf)) -> + let name = Longident.last lbl.txt in + let paths = Paths.construct_field gf name i paths in + pattern_match_single pat paths) + pats_args + |> conjuncts_pattern_match + in + ext, UF.par uf_read uf_pats | Tpat_variant (lbl, arg, _) -> - let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in - let ext, uf_arg = - match arg with - | Some arg -> - let paths = Paths.variant_field lbl paths in - pattern_match_single arg paths - | None -> (Ienv.Extension.empty, UF.unused) - in - (ext, UF.par uf_read uf_arg) + let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in + let ext, uf_arg = + match arg with + | Some arg -> + let paths = Paths.variant_field lbl paths in + pattern_match_single arg paths + | None -> Ienv.Extension.empty, UF.unused + in + ext, UF.par uf_read uf_arg | Tpat_record (pats, _) -> - let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in - let ext, uf_pats = - List.map - (fun (_, l, pat) -> - let paths = Paths.record_field l.lbl_global l.lbl_name paths in - pattern_match_single pat paths) - pats - |> conjuncts_pattern_match - in - (ext, UF.par uf_read uf_pats) + let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in + let ext, uf_pats = + List.map + (fun (_, l, pat) -> + let paths = Paths.record_field l.lbl_global l.lbl_name paths in + pattern_match_single pat paths) + pats + |> conjuncts_pattern_match + in + ext, UF.par uf_read uf_pats | Tpat_array (_, pats) -> - let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in - let ext, uf_pats = - List.map - (fun pat -> - let paths = Paths.fresh () in - pattern_match_single pat paths) - pats - |> conjuncts_pattern_match - in - (ext, UF.par uf_read uf_pats) + let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in + let ext, uf_pats = + List.map + (fun pat -> + let paths = Paths.fresh () in + pattern_match_single pat paths) + pats + |> conjuncts_pattern_match + in + ext, UF.par uf_read uf_pats | Tpat_lazy arg -> - (* forcing a lazy expression is like calling a nullary-function *) - let uf_force = Paths.mark_shared occ Lazy paths in - let paths = Paths.fresh () in - let ext, uf_arg = pattern_match_single arg paths in - (ext, UF.par uf_force uf_arg) + (* forcing a lazy expression is like calling a nullary-function *) + let uf_force = Paths.mark_shared occ Lazy paths in + let paths = Paths.fresh () in + let ext, uf_arg = pattern_match_single arg paths in + ext, UF.par uf_force uf_arg | Tpat_tuple args -> - let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in - let ext, uf_args = - List.mapi - (fun i arg -> - let paths = Paths.tuple_field i paths in - pattern_match_single arg paths) - args - |> conjuncts_pattern_match - in - (ext, UF.par uf_read uf_args) + let uf_read = Paths.mark_implicit_borrow_memory_address Read occ paths in + let ext, uf_args = + List.mapi + (fun i arg -> + let paths = Paths.tuple_field i paths in + pattern_match_single arg paths) + args + |> conjuncts_pattern_match + in + ext, UF.par uf_read uf_args let pattern_match pat = function | Match_tuple values -> pattern_match_tuple pat values @@ -1045,25 +1095,25 @@ let pattern_match pat = function let comp_pattern_match pat value = match split_pattern pat with | Some pat', _ -> pattern_match pat' value - | None, _ -> (Ienv.Extension.empty, UF.unused) + | None, _ -> Ienv.Extension.empty, UF.unused let value_of_ident ienv unique_use occ path = match path with | Path.Pident id -> ( - match Ienv.find_opt id ienv with - (* TODO: for better error message, we should record in ienv why some - variables are not in it. *) - | None -> - force_shared_boundary ~reason:Out_of_mod_class unique_use occ; - None - | Some paths -> - let value = Value.existing paths unique_use occ in - Some value) + match Ienv.find_opt id ienv with + (* TODO: for better error message, we should record in ienv why some + variables are not in it. *) + | None -> + force_shared_boundary ~reason:Out_of_mod_class unique_use occ; + None + | Some paths -> + let value = Value.existing paths unique_use occ in + Some value) (* accessing a module, which is forced by typemod to be shared and many. Here we force it again just to be sure *) | Path.Pdot _ -> - force_shared_boundary ~reason:Paths_from_mod_class unique_use occ; - None + force_shared_boundary ~reason:Paths_from_mod_class unique_use occ; + None | Path.Papply _ -> assert false (* TODO: replace the dirty hack. @@ -1080,18 +1130,17 @@ let value_of_ident ienv unique_use occ path = let open_variables ienv f = let ll = ref [] in let iter = - { - Tast_iterator.default_iterator with + { Tast_iterator.default_iterator with expr = (fun self e -> (match e.exp_desc with | Texp_ident (path, _, _, _, unique_use) -> ( - let occ = Occurrence.mk e.exp_loc in - match value_of_ident ienv unique_use occ path with - | None -> () - | Some value -> ll := value :: !ll) + let occ = Occurrence.mk e.exp_loc in + match value_of_ident ienv unique_use occ path with + | None -> () + | Some value -> ll := value :: !ll) | _ -> ()); - Tast_iterator.default_iterator.expr self e); + Tast_iterator.default_iterator.expr self e) } in f iter; @@ -1112,12 +1161,12 @@ let lift_implicit_borrowing uf = UF.map (function | Maybe_shared t -> - (* implicit borrowing lifted. *) - let occ, access = Maybe_shared.extract_occurrence_access t in - Usage.shared occ (Shared.Lifted access) + (* implicit borrowing lifted. *) + let occ, access = Maybe_shared.extract_occurrence_access t in + Usage.shared occ (Shared.Lifted access) | m -> - (* other usage stays the same *) - m) + (* other usage stays the same *) + m) uf (* There are two modes our algorithm will work at. @@ -1135,165 +1184,163 @@ let lift_implicit_borrowing uf = let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = match exp.exp_desc with | Texp_ident _ -> - let value, uf = check_uniqueness_exp_as_value ienv exp in - UF.seq uf (Value.mark_maybe_unique value) + let value, uf = check_uniqueness_exp_as_value ienv exp in + UF.seq uf (Value.mark_maybe_unique value) | Texp_constant _ -> UF.unused | Texp_let (_, vbs, body) -> - let ext, uf_vbs = check_uniqueness_value_bindings ienv vbs in - let uf_body = check_uniqueness_exp (Ienv.extend ienv ext) body in - UF.seq uf_vbs uf_body + let ext, uf_vbs = check_uniqueness_value_bindings ienv vbs in + let uf_body = check_uniqueness_exp (Ienv.extend ienv ext) body in + UF.seq uf_vbs uf_body | Texp_function { cases; _ } -> - (* `param` is only a hint not a binder; - actual binding done in cases by Tpat_var and Tpat_alias *) - let value = Match_single (Paths.fresh ()) in - let uf = check_uniqueness_cases ienv value cases in - (* we are constructing a closure here, and therefore any implicit - borrowing of free variables in the closure is in fact using shared. *) - lift_implicit_borrowing uf + (* `param` is only a hint not a binder; + actual binding done in cases by Tpat_var and Tpat_alias *) + let value = Match_single (Paths.fresh ()) in + let uf = check_uniqueness_cases ienv value cases in + (* we are constructing a closure here, and therefore any implicit + borrowing of free variables in the closure is in fact using shared. *) + lift_implicit_borrowing uf | Texp_apply (fn, args, _, _) -> - let uf_fn = check_uniqueness_exp ienv fn in - let uf_args = - List.map - (fun (_, arg) -> - match arg with - | Arg (e, _) -> check_uniqueness_exp ienv e - | Omitted _ -> UF.unused) - args - in - UF.pars (uf_fn :: uf_args) + let uf_fn = check_uniqueness_exp ienv fn in + let uf_args = + List.map + (fun (_, arg) -> + match arg with + | Arg (e, _) -> check_uniqueness_exp ienv e + | Omitted _ -> UF.unused) + args + in + UF.pars (uf_fn :: uf_args) | Texp_match (arg, _, cases, _) -> - let value, uf_arg = check_uniqueness_exp_for_match ienv arg in - let uf_cases = check_uniqueness_comp_cases ienv value cases in - UF.seq uf_arg uf_cases + let value, uf_arg = check_uniqueness_exp_for_match ienv arg in + let uf_cases = check_uniqueness_comp_cases ienv value cases in + UF.seq uf_arg uf_cases | Texp_try (body, cases) -> - let uf_body = check_uniqueness_exp ienv body in - let value = Match_single (Paths.fresh ()) in - let uf_cases = check_uniqueness_cases ienv value cases in - (* we don't know how much of e will be run; safe to assume all of them *) - UF.seq uf_body uf_cases + let uf_body = check_uniqueness_exp ienv body in + let value = Match_single (Paths.fresh ()) in + let uf_cases = check_uniqueness_cases ienv value cases in + (* we don't know how much of e will be run; safe to assume all of them *) + UF.seq uf_body uf_cases | Texp_tuple (es, _) -> - UF.pars (List.map (fun e -> check_uniqueness_exp ienv e) es) + UF.pars (List.map (fun e -> check_uniqueness_exp ienv e) es) | Texp_construct (_, _, es, _) -> - UF.pars (List.map (fun e -> check_uniqueness_exp ienv e) es) + UF.pars (List.map (fun e -> check_uniqueness_exp ienv e) es) | Texp_variant (_, None) -> UF.unused | Texp_variant (_, Some (arg, _)) -> check_uniqueness_exp ienv arg | Texp_record { fields; extended_expression } -> - let value, uf_ext = - match extended_expression with - | None -> (Value.fresh, UF.unused) - | Some exp -> - let value, uf_exp = check_uniqueness_exp_as_value ienv exp in - let uf_read = - Value.mark_implicit_borrow_memory_address Read value + let value, uf_ext = + match extended_expression with + | None -> Value.fresh, UF.unused + | Some exp -> + let value, uf_exp = check_uniqueness_exp_as_value ienv exp in + let uf_read = Value.mark_implicit_borrow_memory_address Read value in + value, UF.par uf_exp uf_read + in + let uf_fields = + Array.map + (fun field -> + match field with + | l, Kept (_, unique_use) -> + let value = + Value.implicit_record_field l.lbl_global l.lbl_name value + unique_use in - (value, UF.par uf_exp uf_read) - in - let uf_fields = - Array.map - (fun field -> - match field with - | l, Kept (_, unique_use) -> - let value = - Value.implicit_record_field l.lbl_global l.lbl_name value - unique_use - in - Value.mark_maybe_unique value - | _, Overridden (_, e) -> check_uniqueness_exp ienv e) - fields - in - UF.par uf_ext (UF.pars (Array.to_list uf_fields)) + Value.mark_maybe_unique value + | _, Overridden (_, e) -> check_uniqueness_exp ienv e) + fields + in + UF.par uf_ext (UF.pars (Array.to_list uf_fields)) | Texp_field _ -> - let value, uf = check_uniqueness_exp_as_value ienv exp in - UF.seq uf (Value.mark_maybe_unique value) + let value, uf = check_uniqueness_exp_as_value ienv exp in + UF.seq uf (Value.mark_maybe_unique value) | Texp_setfield (rcd, _, _, _, arg) -> - let value, uf_rcd = check_uniqueness_exp_as_value ienv rcd in - let uf_arg = check_uniqueness_exp ienv arg in - let uf_write = Value.mark_implicit_borrow_memory_address Write value in - UF.pars [ uf_rcd; uf_arg; uf_write ] + let value, uf_rcd = check_uniqueness_exp_as_value ienv rcd in + let uf_arg = check_uniqueness_exp ienv arg in + let uf_write = Value.mark_implicit_borrow_memory_address Write value in + UF.pars [uf_rcd; uf_arg; uf_write] | Texp_array (_, es, _) -> - UF.pars (List.map (fun e -> check_uniqueness_exp ienv e) es) + UF.pars (List.map (fun e -> check_uniqueness_exp ienv e) es) | Texp_ifthenelse (if_, then_, else_opt) -> - (* if' is only borrowed, not used; but probably doesn't matter because of - mode crossing *) - let uf_cond = check_uniqueness_exp ienv if_ in - let uf_then = check_uniqueness_exp ienv then_ in - let uf_else = - match else_opt with - | Some else_ -> check_uniqueness_exp ienv else_ - | None -> UF.unused - in - UF.seq uf_cond (UF.choose uf_then uf_else) + (* if' is only borrowed, not used; but probably doesn't matter because of + mode crossing *) + let uf_cond = check_uniqueness_exp ienv if_ in + let uf_then = check_uniqueness_exp ienv then_ in + let uf_else = + match else_opt with + | Some else_ -> check_uniqueness_exp ienv else_ + | None -> UF.unused + in + UF.seq uf_cond (UF.choose uf_then uf_else) | Texp_sequence (e0, _, e1) -> - let uf0 = check_uniqueness_exp ienv e0 in - let uf1 = check_uniqueness_exp ienv e1 in - UF.seq uf0 uf1 + let uf0 = check_uniqueness_exp ienv e0 in + let uf1 = check_uniqueness_exp ienv e1 in + UF.seq uf0 uf1 | Texp_while { wh_cond; wh_body; _ } -> - let uf_cond = check_uniqueness_exp ienv wh_cond in - let uf_body = check_uniqueness_exp ienv wh_body in - UF.seq uf_cond uf_body + let uf_cond = check_uniqueness_exp ienv wh_cond in + let uf_body = check_uniqueness_exp ienv wh_body in + UF.seq uf_cond uf_body | Texp_list_comprehension { comp_body; comp_clauses } -> - let uf_body = check_uniqueness_exp ienv comp_body in - let uf_clauses = check_uniqueness_comprehensions ienv comp_clauses in - UF.par uf_body uf_clauses + let uf_body = check_uniqueness_exp ienv comp_body in + let uf_clauses = check_uniqueness_comprehensions ienv comp_clauses in + UF.par uf_body uf_clauses | Texp_array_comprehension (_, { comp_body; comp_clauses }) -> - let uf_body = check_uniqueness_exp ienv comp_body in - let uf_clauses = check_uniqueness_comprehensions ienv comp_clauses in - UF.par uf_body uf_clauses + let uf_body = check_uniqueness_exp ienv comp_body in + let uf_clauses = check_uniqueness_comprehensions ienv comp_clauses in + UF.par uf_body uf_clauses | Texp_for { for_from; for_to; for_body; _ } -> - let uf_from = check_uniqueness_exp ienv for_from in - let uf_to = check_uniqueness_exp ienv for_to in - let uf_body = check_uniqueness_exp ienv for_body in - UF.seq (UF.par uf_from uf_to) uf_body + let uf_from = check_uniqueness_exp ienv for_from in + let uf_to = check_uniqueness_exp ienv for_to in + let uf_body = check_uniqueness_exp ienv for_body in + UF.seq (UF.par uf_from uf_to) uf_body | Texp_send (e, _, _, _) -> check_uniqueness_exp ienv e | Texp_new _ -> UF.unused | Texp_instvar _ -> UF.unused | Texp_setinstvar (_, _, _, e) -> check_uniqueness_exp ienv e | Texp_override (_, ls) -> - UF.pars (List.map (fun (_, _, e) -> check_uniqueness_exp ienv e) ls) + UF.pars (List.map (fun (_, _, e) -> check_uniqueness_exp ienv e) ls) | Texp_letmodule (_, _, _, mod_expr, body) -> - let uf_mod = - mark_shared_open_variables ienv - (fun iter -> iter.module_expr iter mod_expr) - mod_expr.mod_loc - in - let uf_body = check_uniqueness_exp ienv body in - UF.seq uf_mod uf_body + let uf_mod = + mark_shared_open_variables ienv + (fun iter -> iter.module_expr iter mod_expr) + mod_expr.mod_loc + in + let uf_body = check_uniqueness_exp ienv body in + UF.seq uf_mod uf_body | Texp_letexception (_, e) -> check_uniqueness_exp ienv e | Texp_assert e -> check_uniqueness_exp ienv e | Texp_lazy e -> - let uf = check_uniqueness_exp ienv e in - lift_implicit_borrowing uf + let uf = check_uniqueness_exp ienv e in + lift_implicit_borrowing uf | Texp_object (cls_struc, _) -> - (* the object (methods, values) will be type-checked by Typeclass, - which invokes uniqueness check.*) - mark_shared_open_variables ienv - (fun iter -> iter.class_structure iter cls_struc) - exp.exp_loc + (* the object (methods, values) will be type-checked by Typeclass, + which invokes uniqueness check.*) + mark_shared_open_variables ienv + (fun iter -> iter.class_structure iter cls_struc) + exp.exp_loc | Texp_pack mod_expr -> - (* the module will be type-checked by Typemod which invokes uniqueness - analysis. *) - mark_shared_open_variables ienv - (fun iter -> iter.module_expr iter mod_expr) - mod_expr.mod_loc + (* the module will be type-checked by Typemod which invokes uniqueness + analysis. *) + mark_shared_open_variables ienv + (fun iter -> iter.module_expr iter mod_expr) + mod_expr.mod_loc | Texp_letop { let_; ands; body } -> - let uf_let = check_uniqueness_binding_op ienv let_ in - let uf_ands = - List.map (fun bop -> check_uniqueness_binding_op ienv bop) ands - in - let uf_body = - check_uniqueness_cases ienv (Match_single (Paths.fresh ())) [ body ] - in - let uf_body = lift_implicit_borrowing uf_body in - UF.pars (uf_let :: (uf_ands @ [ uf_body ])) + let uf_let = check_uniqueness_binding_op ienv let_ in + let uf_ands = + List.map (fun bop -> check_uniqueness_binding_op ienv bop) ands + in + let uf_body = + check_uniqueness_cases ienv (Match_single (Paths.fresh ())) [body] + in + let uf_body = lift_implicit_borrowing uf_body in + UF.pars (uf_let :: (uf_ands @ [uf_body])) | Texp_unreachable -> UF.unused | Texp_extension_constructor _ -> UF.unused | Texp_open (open_decl, e) -> - let uf = - mark_shared_open_variables ienv - (fun iter -> iter.open_declaration iter open_decl) - open_decl.open_loc - in - UF.seq uf (check_uniqueness_exp ienv e) + let uf = + mark_shared_open_variables ienv + (fun iter -> iter.open_declaration iter open_decl) + open_decl.open_loc + in + UF.seq uf (check_uniqueness_exp ienv e) | Texp_probe { handler } -> check_uniqueness_exp ienv handler | Texp_probe_is_enabled _ -> UF.unused | Texp_exclave e -> check_uniqueness_exp ienv e @@ -1308,46 +1355,46 @@ and check_uniqueness_exp_as_value ienv exp : Value.t * UF.t = let loc = exp.exp_loc in match exp.exp_desc with | Texp_ident (p, _, _, _, unique_use) -> - let occ = Occurrence.mk loc in - let value = - match value_of_ident ienv unique_use occ p with - | None -> - (* cross module access - don't track *) - Value.untracked unique_use occ - | Some value -> value - in - (value, UF.unused) + let occ = Occurrence.mk loc in + let value = + match value_of_ident ienv unique_use occ p with + | None -> + (* cross module access - don't track *) + Value.untracked unique_use occ + | Some value -> value + in + value, UF.unused | Texp_field (e, _, l, unique_use, _) -> ( - let value, uf = check_uniqueness_exp_as_value ienv e in - match Value.paths value with - | None -> (Value.fresh, uf) - | Some paths -> - (* accessing the field meaning borrowing the parent record's mem - block. Note that the field itself is not borrowed or used *) - let uf_read = Value.mark_implicit_borrow_memory_address Read value in - let occ = Occurrence.mk loc in - let paths = Paths.record_field l.lbl_global l.lbl_name paths in - let value = Value.existing paths unique_use occ in - (value, UF.seq uf uf_read)) + let value, uf = check_uniqueness_exp_as_value ienv e in + match Value.paths value with + | None -> Value.fresh, uf + | Some paths -> + (* accessing the field meaning borrowing the parent record's mem + block. Note that the field itself is not borrowed or used *) + let uf_read = Value.mark_implicit_borrow_memory_address Read value in + let occ = Occurrence.mk loc in + let paths = Paths.record_field l.lbl_global l.lbl_name paths in + let value = Value.existing paths unique_use occ in + value, UF.seq uf uf_read) (* CR-someday anlorenzen: This could also support let-bindings. *) - | _ -> (Value.fresh, check_uniqueness_exp ienv exp) + | _ -> Value.fresh, check_uniqueness_exp ienv exp (** take typed expression, do some parsing and returns [value_to_match] *) and check_uniqueness_exp_for_match ienv exp : value_to_match * UF.t = match exp.exp_desc with | Texp_tuple (es, _) -> - let values, ufs = - List.split (List.map (check_uniqueness_exp_as_value ienv) es) - in - (Match_tuple values, UF.pars ufs) + let values, ufs = + List.split (List.map (check_uniqueness_exp_as_value ienv) es) + in + Match_tuple values, UF.pars ufs | _ -> - let value, uf = check_uniqueness_exp_as_value ienv exp in - let paths = - match Value.paths value with - | None -> Paths.fresh () - | Some paths -> paths - in - (Match_single paths, uf) + let value, uf = check_uniqueness_exp_as_value ienv exp in + let paths = + match Value.paths value with + | None -> Paths.fresh () + | Some paths -> paths + in + Match_single paths, uf (** Returns [ienv] and [uf]. [ienv] is the new bindings introduced; @@ -1363,10 +1410,10 @@ and check_uniqueness_value_bindings ienv vbs = check_uniqueness_exp_for_match ienv vb.vb_expr in let ienv, uf_pat = pattern_match vb.vb_pat value in - (ienv, UF.seq uf_value uf_pat)) + ienv, UF.seq uf_value uf_pat) vbs) in - (Ienv.Extension.conjuncts exts, UF.pars uf_vbs) + Ienv.Extension.conjuncts exts, UF.pars uf_vbs (* type signature needed because high-ranked *) and check_uniqueness_cases_gen : @@ -1385,7 +1432,7 @@ and check_uniqueness_cases_gen : | None -> UF.unused | Some g -> check_uniqueness_exp (Ienv.extend ienv ext) g in - (ext, UF.par uf_lhs uf_guard)) + ext, UF.par uf_lhs uf_guard) cases) in (* we then evaluate all RHS, in _parallel_ *) @@ -1409,7 +1456,7 @@ and check_uniqueness_comprehensions ienv cs = match c with | Texp_comp_when e -> check_uniqueness_exp ienv e | Texp_comp_for cbs -> - check_uniqueness_comprehension_clause_binding ienv cbs) + check_uniqueness_comprehension_clause_binding ienv cbs) cs) and check_uniqueness_comprehension_clause_binding ienv cbs = @@ -1418,9 +1465,9 @@ and check_uniqueness_comprehension_clause_binding ienv cbs = (fun cb -> match cb.comp_cb_iterator with | Texp_comp_range { start; stop; _ } -> - let uf_start = check_uniqueness_exp ienv start in - let uf_stop = check_uniqueness_exp ienv stop in - UF.par uf_start uf_stop + let uf_start = check_uniqueness_exp ienv start in + let uf_stop = check_uniqueness_exp ienv stop in + UF.par uf_start uf_stop | Texp_comp_in { sequence; _ } -> check_uniqueness_exp ienv sequence) cbs) @@ -1448,63 +1495,56 @@ let report_multi_use inner first_is_of_second = let there_usage = match there with | Usage.Maybe_shared t -> ( - let _, access = Maybe_shared.extract_occurrence_access t in - match access with Read -> "read from" | Write -> "written to") + let _, access = Maybe_shared.extract_occurrence_access t in + match access with Read -> "read from" | Write -> "written to") | Usage.Shared t -> ( - match Shared.reason t with - | Forced | Lazy -> "used" - | Lifted access -> - Maybe_shared.string_of_access access - ^ " in a closure that might be called later") + match Shared.reason t with + | Forced | Lazy -> "used" + | Lifted access -> + Maybe_shared.string_of_access access + ^ " in a closure that might be called later") | _ -> "used" in let first, first_usage, second, second_usage = match first_or_second with | Usage.First -> - ( occ, - here_usage, - Option.get (Usage.extract_occurrence there), - there_usage ) + occ, here_usage, Option.get (Usage.extract_occurrence there), there_usage | Usage.Second -> - ( Option.get (Usage.extract_occurrence there), - there_usage, - occ, - here_usage ) + Option.get (Usage.extract_occurrence there), there_usage, occ, here_usage in let first_is_of_second = match first_is_of_second with | Self - | Ancestor [ Projection.Memory_address ] - | Descendant [ Projection.Memory_address ] -> - "it" + | Ancestor [Projection.Memory_address] + | Descendant [Projection.Memory_address] -> + "it" | Descendant _ -> "part of it" | Ancestor _ -> "it is part of a value that" in - (* English is sadly not very composible, we write out all four cases manually *) let error = - match (first_or_second, axis) with + match first_or_second, axis with | First, Uniqueness -> - Format.dprintf - "This value is %s here,@ but %s has already been %s as unique:" - second_usage first_is_of_second first_usage + Format.dprintf + "This value is %s here,@ but %s has already been %s as unique:" + second_usage first_is_of_second first_usage | First, Linearity -> - Format.dprintf - "This value is %s here,@ but %s is defined as once and has already \ - been %s:" - second_usage first_is_of_second first_usage + Format.dprintf + "This value is %s here,@ but %s is defined as once and has already \ + been %s:" + second_usage first_is_of_second first_usage | Second, Uniqueness -> - Format.dprintf - "This value is %s here as unique,@ but %s has already been %s:" - second_usage first_is_of_second first_usage + Format.dprintf + "This value is %s here as unique,@ but %s has already been %s:" + second_usage first_is_of_second first_usage | Second, Linearity -> - Format.dprintf - "This value is defined as once and %s here,@ but %s has already been \ - %s:" - second_usage first_is_of_second first_usage + Format.dprintf + "This value is defined as once and %s here,@ but %s has already been \ + %s:" + second_usage first_is_of_second first_usage in - let sub = [ Location.msg ~loc:first.loc "" ] in + let sub = [Location.msg ~loc:first.loc ""] in Location.errorf ~loc:second.loc ~sub "@[%t@]" error let report_boundary cannot_force reason = @@ -1527,7 +1567,7 @@ let report_error err = Printtyp.wrap_printing_env ~error:true Env.empty (fun () -> match err with | Usage { inner; first_is_of_second } -> - report_multi_use inner first_is_of_second + report_multi_use inner first_is_of_second | Boundary { cannot_force; reason } -> report_boundary cannot_force reason) let () = diff --git a/typing/uniqueness_analysis.mli b/typing/uniqueness_analysis.mli index 5786dada150..6a2f0892388 100644 --- a/typing/uniqueness_analysis.mli +++ b/typing/uniqueness_analysis.mli @@ -15,8 +15,10 @@ open Typedtree -(* Check that idents which are used more than once, are not used with mode unique. *) +(* Check that idents which are used more than once, are not used with mode + unique. *) val check_uniqueness_exp : expression -> unit -(* Check that idents which are used more than once, are not used with mode unique. *) +(* Check that idents which are used more than once, are not used with mode + unique. *) val check_uniqueness_value_bindings : value_binding list -> unit