From 26c8602bfe1772888be01603ad19cadfab8c8081 Mon Sep 17 00:00:00 2001 From: Zesen Qian Date: Tue, 11 Jun 2024 13:54:31 +0100 Subject: [PATCH] Refactor modality logic (#2344) --- ocaml/.depend | 6 +- ocaml/ocamldoc/odoc_sig.ml | 2 +- ocaml/otherlibs/dynlink/dune | 5 - ocaml/testsuite/tests/typing-local/local.ml | 10 +- ocaml/testsuite/tests/typing-modes/modes.ml | 50 ++- ocaml/testsuite/tests/typing-modes/mutable.ml | 7 +- ocaml/testsuite/tests/typing-unique/unique.ml | 10 +- .../tests/typing-unique/unique_analysis.ml | 24 +- ocaml/typing/ctype.ml | 2 +- ocaml/typing/ctype.mli | 2 +- ocaml/typing/datarepr.ml | 6 +- ocaml/typing/includecore.ml | 58 ++-- ocaml/typing/includecore.mli | 7 +- ocaml/typing/mode.ml | 297 +++++++++++++++--- ocaml/typing/mode_intf.mli | 72 ++++- ocaml/typing/oprint.ml | 50 ++- ocaml/typing/oprint.mli | 6 +- ocaml/typing/outcometree.mli | 16 +- ocaml/typing/predef.ml | 10 +- ocaml/typing/printtyp.ml | 53 +++- ocaml/typing/printtyp.mli | 4 + ocaml/typing/subst.ml | 2 +- ocaml/typing/typecore.ml | 45 +-- ocaml/typing/typedecl.ml | 16 +- ocaml/typing/typedtree.ml | 4 +- ocaml/typing/typedtree.mli | 4 +- ocaml/typing/typemode.ml | 66 ++-- ocaml/typing/typemode.mli | 7 +- ocaml/typing/types.ml | 8 +- ocaml/typing/types.mli | 8 +- ocaml/typing/uniqueness_analysis.ml | 30 +- ocaml/utils/warnings.ml | 8 - ocaml/utils/warnings.mli | 1 - 33 files changed, 627 insertions(+), 269 deletions(-) diff --git a/ocaml/.depend b/ocaml/.depend index c212628a00d..6d604ae8c21 100644 --- a/ocaml/.depend +++ b/ocaml/.depend @@ -1002,6 +1002,7 @@ typing/includecore.cmi : \ typing/types.cmi \ typing/typedtree.cmi \ typing/path.cmi \ + typing/mode.cmi \ parsing/location.cmi \ typing/jkind.cmi \ typing/ident.cmi \ @@ -1486,6 +1487,7 @@ typing/printtyp.cmi : \ typing/shape.cmi \ typing/path.cmi \ typing/outcometree.cmi \ + typing/mode.cmi \ parsing/longident.cmi \ parsing/location.cmi \ typing/ident.cmi \ @@ -1943,6 +1945,7 @@ typing/typedecl.cmi : \ typing/shape.cmi \ typing/path.cmi \ parsing/parsetree.cmi \ + typing/mode.cmi \ parsing/longident.cmi \ parsing/location.cmi \ utils/language_extension.cmi \ @@ -2185,14 +2188,12 @@ typing/typemod.cmi : \ utils/compilation_unit.cmi \ file_formats/cmi_format.cmi typing/typemode.cmo : \ - utils/warnings.cmi \ typing/mode.cmi \ parsing/location.cmi \ parsing/jane_syntax_parsing.cmi \ parsing/jane_syntax.cmi \ typing/typemode.cmi typing/typemode.cmx : \ - utils/warnings.cmx \ typing/mode.cmx \ parsing/location.cmx \ parsing/jane_syntax_parsing.cmx \ @@ -2200,6 +2201,7 @@ typing/typemode.cmx : \ typing/typemode.cmi typing/typemode.cmi : \ typing/mode.cmi \ + parsing/location.cmi \ parsing/jane_syntax.cmi typing/typeopt.cmo : \ typing/types.cmi \ diff --git a/ocaml/ocamldoc/odoc_sig.ml b/ocaml/ocamldoc/odoc_sig.ml index c59fe94262b..e3b6e604c50 100644 --- a/ocaml/ocamldoc/odoc_sig.ml +++ b/ocaml/ocamldoc/odoc_sig.ml @@ -492,7 +492,7 @@ module Analyser = let record comments { Typedtree.ld_id; ld_mutable; ld_type; ld_loc; ld_attributes } = get_field env comments @@ - {Types.ld_id; ld_mutable; ld_global = Unrestricted; + {Types.ld_id; ld_mutable; ld_modalities = Mode.Modality.Value.id; ld_jkind=Jkind.any ~why:Dummy_jkind (* ignored *); ld_type=ld_type.Typedtree.ctyp_type; ld_loc; ld_attributes; ld_uid=Types.Uid.internal_not_actually_unique} in diff --git a/ocaml/otherlibs/dynlink/dune b/ocaml/otherlibs/dynlink/dune index a2bdc54f3a0..f965c9794f7 100644 --- a/ocaml/otherlibs/dynlink/dune +++ b/ocaml/otherlibs/dynlink/dune @@ -91,7 +91,6 @@ solver mode_intf mode - typemode jkind_intf jkind_types primitive @@ -199,7 +198,6 @@ (copy_files ../../typing/solver.ml) (copy_files ../../typing/shape_reduce.ml) (copy_files ../../typing/mode.ml) -(copy_files ../../typing/typemode.ml) (copy_files ../../typing/types.ml) (copy_files ../../typing/btype.ml) (copy_files ../../typing/subst.ml) @@ -269,7 +267,6 @@ (copy_files ../../typing/solver.mli) (copy_files ../../typing/shape_reduce.mli) (copy_files ../../typing/mode.mli) -(copy_files ../../typing/typemode.mli) (copy_files ../../typing/types.mli) (copy_files ../../typing/btype.mli) (copy_files ../../typing/subst.mli) @@ -380,7 +377,6 @@ .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Ast_mapper.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Solver.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Mode.cmo - .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Typemode.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind_intf.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind_types.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Types.cmo @@ -464,7 +460,6 @@ .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Ast_mapper.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Solver.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Mode.cmx - .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Typemode.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind_intf.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind_types.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Types.cmx diff --git a/ocaml/testsuite/tests/typing-local/local.ml b/ocaml/testsuite/tests/typing-local/local.ml index cd4268e7730..6229d413059 100644 --- a/ocaml/testsuite/tests/typing-local/local.ml +++ b/ocaml/testsuite/tests/typing-local/local.ml @@ -1672,7 +1672,7 @@ Error: Signature mismatch: foo : string; is not the same as: global_ foo : string; - The second is global and the first is not. + The second is global_ and the first is not. |}] module M : sig @@ -1698,7 +1698,7 @@ Error: Signature mismatch: global_ foo : string; is not the same as: foo : string; - The first is global and the second is not. + The first is global_ and the second is not. |}] (* Special handling of tuples in matches and let bindings *) @@ -2523,7 +2523,8 @@ Error: Signature mismatch: Bar of int * string is not the same as: Bar of int * global_ string - Locality mismatch at argument position 2 : The second is global and the first is not. + Modality mismatch at argument position 2: + The second is global_ and the first is not. |}] @@ -2550,7 +2551,8 @@ Error: Signature mismatch: Bar of int * global_ string is not the same as: Bar of int * string - Locality mismatch at argument position 2 : The first is global and the second is not. + Modality mismatch at argument position 2: + The first is global_ and the second is not. |}] (* global_ binds closer than star *) diff --git a/ocaml/testsuite/tests/typing-modes/modes.ml b/ocaml/testsuite/tests/typing-modes/modes.ml index a5cdbdb16fb..b3239182dae 100644 --- a/ocaml/testsuite/tests/typing-modes/modes.ml +++ b/ocaml/testsuite/tests/typing-modes/modes.ml @@ -231,12 +231,8 @@ Error: Unrecognized modality foo. |}] type t = Foo of global_ string @@ global +(* CR reduced-modality: this should warn. *) [%%expect{| -Line 1, characters 34-40: -1 | type t = Foo of global_ string @@ global - ^^^^^^ -Warning 250 [redundant-modality]: This global modality is redundant. - type t = Foo of global_ string |}] @@ -260,15 +256,49 @@ Error: Unrecognized modality foo. type r = { global_ x : string @@ global } +(* CR reduced-modality: this should warn. *) [%%expect{| -Line 2, characters 24-30: -2 | global_ x : string @@ global - ^^^^^^ -Warning 250 [redundant-modality]: This global modality is redundant. - type r = { global_ x : string; } |}] +(* Modalities don't imply each other; this will change as we add borrowing. *) +type r = { + global_ x : string @@ shared +} +[%%expect{| +type r = { global_ x : string @@ shared; } +|}] + +type r = { + x : string @@ shared global many +} +[%%expect{| +type r = { global_ x : string @@ many shared; } +|}] + +type r = { + x : string @@ shared global many shared +} +(* CR reduced-modality: this should warn. *) +[%%expect{| +type r = { global_ x : string @@ many shared; } +|}] + +type r = Foo of string @@ global shared many +[%%expect{| +type r = Foo of global_ string @@ many shared +|}] + +(* mutable implies global shared many. No warnings are given since we imagine + that the coupling will be removed soon. *) +type r = { + mutable x : string @@ global shared many +} +[%%expect{| +type r = { mutable x : string; } +|}] + + (* patterns *) let foo ?(local_ x @ unique once = 42) () = () diff --git a/ocaml/testsuite/tests/typing-modes/mutable.ml b/ocaml/testsuite/tests/typing-modes/mutable.ml index f82691093f2..5e474258653 100644 --- a/ocaml/testsuite/tests/typing-modes/mutable.ml +++ b/ocaml/testsuite/tests/typing-modes/mutable.ml @@ -3,9 +3,10 @@ expect; *) -(* Since [mutable] implies [global] modality, which in turns implies [shared] - and [many] modalities, the effect of mutable in isolation is not testable - yet. *) +(* This file tests the typing around mutable() logic. *) + +(* For legacy compatibility, [mutable] implies [global] [shared] and [many]. + Therefore, the effect of mutable in isolation is not testable yet. *) (* CR zqian: add test for mutable when mutable is decoupled from modalities. *) diff --git a/ocaml/testsuite/tests/typing-unique/unique.ml b/ocaml/testsuite/tests/typing-unique/unique.ml index 2d663aaf3b3..1864e569ab1 100644 --- a/ocaml/testsuite/tests/typing-unique/unique.ml +++ b/ocaml/testsuite/tests/typing-unique/unique.ml @@ -241,12 +241,11 @@ Error: This value is shared but expected to be unique. |}] -(* global modality entails shared modality; -this is crucial once we introduce borrowing whose scope is controlled -by locality *) -type 'a glob = { global_ glob: 'a } [@@unboxed] +(* CR zqian: [global] should imply [shared]/[many], once we introduce borrowing whose +scope is controlled by locality *) +type 'a glob = { glob: 'a @@ shared many } [@@unboxed] [%%expect{| -type 'a glob = { global_ glob : 'a; } [@@unboxed] +type 'a glob = { glob : 'a @@ many shared; } [@@unboxed] |}] let dup (glob : 'a) : 'a glob * 'a glob = unique_ ({glob}, {glob}) [%%expect{| @@ -655,4 +654,3 @@ Line 2, characters 11-19: ^^^^^^^^ |}] - diff --git a/ocaml/testsuite/tests/typing-unique/unique_analysis.ml b/ocaml/testsuite/tests/typing-unique/unique_analysis.ml index 5e935911294..c7fa7029445 100644 --- a/ocaml/testsuite/tests/typing-unique/unique_analysis.ml +++ b/ocaml/testsuite/tests/typing-unique/unique_analysis.ml @@ -612,9 +612,9 @@ val foo : unit -> unit = |}] (* Testing modalities in records *) -type r_global = {x : string; global_ y : string} +type r_shared = {x : string; y : string @@ shared many} [%%expect{| -type r_global = { x : string; global_ y : string; } +type r_shared = { x : string; y : string @@ many shared; } |}] let foo () = @@ -697,14 +697,14 @@ Line 3, characters 19-20: |}] (* testing modalities in constructors *) -type r_global = R_global of string * global_ string +type r_shared = R_shared of string * string @@ shared many [%%expect{| -type r_global = R_global of string * global_ string +type r_shared = R_shared of string * string @@ many shared |}] let foo () = - let r = R_global ("hello", "world") in - let R_global (_, y) = r in + let r = R_shared ("hello", "world") in + let R_shared (_, y) = r in ignore (shared_id y); (* the following is allowed, because using r uniquely implies using r.x shared *) @@ -715,8 +715,8 @@ val foo : unit -> unit = (* Similarly for linearity *) let foo () = - let r = once_ (R_global ("hello", "world")) in - let R_global (_, y) = r in + let r = once_ (R_shared ("hello", "world")) in + let R_shared (_, y) = r in ignore_once y; ignore_once r; [%%expect{| @@ -724,8 +724,8 @@ val foo : unit -> unit = |}] let foo () = - let r = once_ (R_global ("hello", "world")) in - let R_global (x, _) = r in + let r = once_ (R_shared ("hello", "world")) in + let R_shared (x, _) = r in ignore_once x; ignore_once r; [%%expect{| @@ -741,8 +741,8 @@ Line 4, characters 14-15: |}] let foo () = - let r = R_global ("hello", "world") in - let R_global (x, _) = r in + let r = R_shared ("hello", "world") in + let R_shared (x, _) = r in ignore (shared_id x); (* doesn't work for normal fields *) ignore (unique_id r) diff --git a/ocaml/typing/ctype.ml b/ocaml/typing/ctype.ml index ff4ef2c006f..e72d9492177 100644 --- a/ocaml/typing/ctype.ml +++ b/ocaml/typing/ctype.ml @@ -3144,7 +3144,7 @@ and mcomp_record_description type_pairs env = mcomp type_pairs env l1.ld_type l2.ld_type; if Ident.name l1.ld_id = Ident.name l2.ld_id && l1.ld_mutable = l2.ld_mutable && - l1.ld_global = l2.ld_global + l1.ld_modalities = l2.ld_modalities then iter xs ys else raise Incompatible | [], [] -> () diff --git a/ocaml/typing/ctype.mli b/ocaml/typing/ctype.mli index 90c9ab1a765..28ef0291a31 100644 --- a/ocaml/typing/ctype.mli +++ b/ocaml/typing/ctype.mli @@ -186,7 +186,7 @@ type existential_treatment = val instance_constructor: existential_treatment -> constructor_description -> - (type_expr * Global_flag.t) list * type_expr * type_expr list + (type_expr * Modality.Value.t) list * type_expr * type_expr list (* Same, for a constructor. Also returns existentials. *) val instance_parameterized_type: ?keep_names:bool -> diff --git a/ocaml/typing/datarepr.ml b/ocaml/typing/datarepr.ml index d02ceebff19..9627ab568c6 100644 --- a/ocaml/typing/datarepr.ml +++ b/ocaml/typing/datarepr.ml @@ -95,7 +95,7 @@ let constructor_args ~current_unit priv cd_args cd_res path rep = } in existentials, - [ newgenconstr path type_params, Global_flag.Unrestricted ], + [ newgenconstr path type_params, Modality.Value.id ], Some tdecl let constructor_descrs ~current_unit ty_path decl cstrs rep = @@ -201,7 +201,7 @@ let none = let dummy_label = { lbl_name = ""; lbl_res = none; lbl_arg = none; - lbl_mut = Immutable; lbl_global = Unrestricted; + lbl_mut = Immutable; lbl_modalities = Modality.Value.id; lbl_jkind = Jkind.any ~why:Dummy_jkind; lbl_num = -1; lbl_pos = -1; lbl_all = [||]; lbl_repres = Record_unboxed; @@ -222,7 +222,7 @@ let label_descrs ty_res lbls repres priv = lbl_res = ty_res; lbl_arg = l.ld_type; lbl_mut = l.ld_mutable; - lbl_global = l.ld_global; + lbl_modalities = l.ld_modalities; lbl_jkind = l.ld_jkind; lbl_pos = if is_void then lbl_pos_void else pos; lbl_num = num; diff --git a/ocaml/typing/includecore.ml b/ocaml/typing/includecore.ml index a1c9d864455..dad926a4e10 100644 --- a/ocaml/typing/includecore.ml +++ b/ocaml/typing/includecore.ml @@ -18,6 +18,7 @@ open Asttypes open Path open Types +open Mode open Typedtree type position = Errortrace.position = First | Second @@ -249,8 +250,6 @@ type privacy_mismatch = | Private_extensible_variant | Private_row_type -type locality_mismatch = { order : position } - type type_kind = | Kind_abstract | Kind_record @@ -268,7 +267,7 @@ type kind_mismatch = type_kind * type_kind type label_mismatch = | Type of Errortrace.equality_error | Mutability of position - | Nonlocality of locality_mismatch + | Modality of Modality.Value.equate_error type record_change = (Types.label_declaration, Types.label_declaration, label_mismatch) @@ -287,7 +286,7 @@ type constructor_mismatch = | Inline_record of record_change list | Kind of position | Explicit_return_type of position - | Nonlocality of int * locality_mismatch + | Modality of int * Modality.Value.equate_error type extension_constructor_mismatch = | Constructor_privacy @@ -326,13 +325,21 @@ type type_mismatch = | Extensible_representation of position | Jkind of Jkind.Violation.t -let report_locality_mismatch first second ppf err = - let {order} = err in - let sort = "global" in - Format.fprintf ppf "%s is %s and %s is not." - (String.capitalize_ascii (choose order first second)) - sort - (choose_other order first second) +let report_modality_sub_error first second ppf e = + let print_modality id ppf m = + Printtyp.modality ~id:(fun ppf -> Format.pp_print_string ppf id) ppf m + in + let Modality.Value.Error(ax, {left; right}) = e in + Format.fprintf ppf "%s is %a and %s is %a." + (String.capitalize_ascii second) + (print_modality "empty") (Atom (ax, right) : Modality.t) + first + (print_modality "not") (Atom (ax, left) : Modality.t) + +let report_modality_equate_error first second ppf ((equate_step, sub_error) : Modality.Value.equate_error) = + match equate_step with + | Left_le_right -> report_modality_sub_error first second ppf sub_error + | Right_le_left -> report_modality_sub_error second first ppf sub_error let report_primitive_mismatch first second ppf err = let pr fmt = Format.fprintf ppf fmt in @@ -410,7 +417,7 @@ let report_label_mismatch first second env ppf err = Format.fprintf ppf "%s is mutable and %s is not." (String.capitalize_ascii (choose ord first second)) (choose_other ord first second) - | Nonlocality err_ -> report_locality_mismatch first second ppf err_ + | Modality err_ -> report_modality_equate_error first second ppf err_ let pp_record_diff first second prefix decl env ppf (x : record_change) = match x with @@ -494,9 +501,9 @@ let report_constructor_mismatch first second decl env ppf err = pr "%s has explicit return type and %s doesn't." (String.capitalize_ascii (choose ord first second)) (choose_other ord first second) - | Nonlocality (i, err) -> - pr "Locality mismatch at argument position %i : %a" - (i + 1) (report_locality_mismatch first second) err + | Modality (i, err) -> + pr "Modality mismatch at argument position %i:@ %a" + (i + 1) (report_modality_equate_error first second) err (* argument position is one-based; more intuitive *) let pp_variant_diff first second prefix decl env ppf (x : variant_change) = @@ -619,12 +626,6 @@ let report_type_mismatch first second decl env ppf err = | Jkind v -> Jkind.Violation.report_with_name ~name:first ppf v -let compare_global_flags flag0 flag1 = - let c = Mode.Global_flag.compare flag0 flag1 in - if c < 0 then Some {order = First} - else if c > 0 then Some {order = Second} - else None - module Record_diffing = struct let compare_labels env params1 params2 @@ -646,8 +647,8 @@ module Record_diffing = struct begin match mut with | Some mut -> Some (Mutability mut) | None -> - match compare_global_flags ld1.ld_global ld2.ld_global with - | None -> + match Modality.Value.equate ld1.ld_modalities ld2.ld_modalities with + | Ok () -> let tl1 = params1 @ [ld1.ld_type] in let tl2 = params2 @ [ld2.ld_type] in begin @@ -656,7 +657,7 @@ module Record_diffing = struct Some (Type err : label_mismatch) | () -> None end - | Some e -> Some (Nonlocality e : label_mismatch) + | Error e -> Some (Modality e : label_mismatch) end let rec equal ~loc env params1 params2 @@ -798,6 +799,10 @@ let rec find_map_idx f ?(off = 0) l = | Some y -> Some (off, y) end +let get_error = function + | Ok () -> None + | Error e -> Some e + module Variant_diffing = struct let compare_constructor_arguments ~loc env params1 params2 arg1 arg2 = @@ -813,8 +818,9 @@ module Variant_diffing = struct match Ctype.equal env true (params1 @ arg1_tys) (params2 @ arg2_tys) with | exception Ctype.Equality err -> Some (Type err) | () -> List.combine arg1_gfs arg2_gfs - |> find_map_idx (fun (x,y) -> compare_global_flags x y) - |> Option.map (fun (i, err) -> Nonlocality (i, err)) + |> find_map_idx + (fun (x,y) -> get_error @@ Modality.Value.equate x y) + |> Option.map (fun (i, err) -> Modality (i, err)) end | Types.Cstr_record l1, Types.Cstr_record l2 -> Option.map diff --git a/ocaml/typing/includecore.mli b/ocaml/typing/includecore.mli index aac298595de..61fa5f8dc3e 100644 --- a/ocaml/typing/includecore.mli +++ b/ocaml/typing/includecore.mli @@ -17,6 +17,7 @@ open Typedtree open Types +open Mode type position = Errortrace.position = First | Second @@ -49,8 +50,6 @@ type privacy_mismatch = | Private_extensible_variant | Private_row_type -type locality_mismatch = { order : position } - type type_kind = | Kind_abstract | Kind_record @@ -62,7 +61,7 @@ type kind_mismatch = type_kind * type_kind type label_mismatch = | Type of Errortrace.equality_error | Mutability of position - | Nonlocality of locality_mismatch + | Modality of Modality.Value.equate_error type record_change = (Types.label_declaration as 'ld, 'ld, label_mismatch) Diffing_with_keys.change @@ -80,7 +79,7 @@ type constructor_mismatch = | Inline_record of record_change list | Kind of position | Explicit_return_type of position - | Nonlocality of int * locality_mismatch + | Modality of int * Modality.Value.equate_error type extension_constructor_mismatch = | Constructor_privacy diff --git a/ocaml/typing/mode.ml b/ocaml/typing/mode.ml index 671b2e94db1..353aa490c8e 100644 --- a/ocaml/typing/mode.ml +++ b/ocaml/typing/mode.ml @@ -25,18 +25,6 @@ type nonrec disallowed = disallowed type nonrec equate_step = equate_step -module Global_flag = struct - type t = - | Global - | Unrestricted - - let compare flag0 flag1 = - match flag0, flag1 with - | Global, Unrestricted -> -1 - | Unrestricted, Global -> 1 - | Global, Global | Unrestricted, Unrestricted -> 0 -end - module type BiHeyting = sig (** Extend the [Lattice] interface with operations of bi-Heyting algebras *) @@ -46,8 +34,8 @@ module type BiHeyting = sig [meet c a <= b] iff [a <= imply c b] *) val imply : t -> t -> t - (** [subtract c] is the left adjoint of [join c]. That is, for any [a] and [b], - [subtract c a <= b] iff [a <= join c b] *) + (** [subtract _ c] is the left adjoint of [join c]. That is, for any [a] and [b], + [subtract a c <= b] iff [a <= join c b] *) val subtract : t -> t -> t end @@ -71,9 +59,9 @@ module Lattices = struct let print = L.print - let imply = L.subtract + let imply a b = L.subtract b a - let subtract = L.imply + let subtract a b = L.imply b a end [@@inline] @@ -83,18 +71,18 @@ module Lattices = struct include L (* Prove the [subtract] below is the left adjoint of [join]. - - If [subtract c a <= b], by the definition of [subtract] below, + - If [subtract a c <= b], by the definition of [subtract] below, that could mean one of two things: - Took the branch [a <= c], and [min <= b]. In this case, we have [a <= c <= join c b]. - Took the other branch, and [a <= b]. In this case, we have [a <= b <= join c b]. - In the other direction: Given [a <= join c b], compare [c] and [b]: - if [c <= b], then [a <= join c b = b], and: - - either [a <= c], then [subtract c a = min <= b] - - or the other branch, then [subtract c a = a <= b] - - if [b <= c], then [a <= join c b = c], then [subtract c a = min <= b] + - either [a <= c], then [subtract a c = min <= b] + - or the other branch, then [subtract a c = a <= b] + - if [b <= c], then [a <= join c b = c], then [subtract a c = min <= b] *) - let subtract c a = if le a c then min else a + let subtract a c = if le a c then min else a (* The proof for [imply] is dual and omitted. *) let imply c b = if le c b then max else b @@ -970,7 +958,7 @@ module Lattices_mono = struct | Meet_with c -> meet dst c a | Join_with c -> join dst c a | Imply c -> imply dst c a - | Subtract c -> subtract dst c a + | Subtract c -> subtract dst a c | Monadic_to_comonadic_min -> monadic_to_comonadic_min dst a | Comonadic_to_monadic src -> comonadic_to_monadic src a | Monadic_to_comonadic_max -> monadic_to_comonadic_max dst a @@ -1497,14 +1485,8 @@ module type Areality = sig end module Comonadic_with (Areality : Areality) = struct - module Const = struct - include C.Comonadic_with (Areality.Const) - - let eq a b = le a b && le b a - end - module Obj = struct - type const = Const.t + type const = Areality.Obj.const C.comonadic_with module Solver = S.Positive @@ -1513,7 +1495,7 @@ module Comonadic_with (Areality : Areality) = struct include Common (Obj) - type error = Error : (Const.t, 'a) C.Axis.t * 'a Solver.error -> error + type error = Error : (Obj.const, 'a) C.Axis.t * 'a Solver.error -> error type equate_error = equate_step * error @@ -1521,6 +1503,26 @@ module Comonadic_with (Areality : Areality) = struct let proj_obj ax = C.proj_obj ax obj + module Const = struct + include C.Comonadic_with (Areality.Const) + + let eq a b = le a b && le b a + + let le_axis ax a b = + let obj = proj_obj ax in + C.le obj a b + + let min_axis ax = + let obj = proj_obj ax in + C.min obj + + let max_axis ax = + let obj = proj_obj ax in + C.max obj + + let max_with ax c = Axis.update ax c (C.max obj) + end + let proj ax m = Solver.via_monotone (proj_obj ax) (Proj (Obj.obj, ax)) m let meet_const c m = Solver.via_monotone obj (Meet_with c) m @@ -1547,20 +1549,23 @@ module Comonadic_with (Areality : Areality) = struct let legacy = of_const Const.legacy + let axis_of_error { left = area0, lin0, port0; right = area1, lin1, port1 } : + error = + if Areality.Const.le area0 area1 + then + if Linearity.Const.le lin0 lin1 + then + if Portability.Const.le port0 port1 + then assert false + else Error (Portability, { left = port0; right = port1 }) + else Error (Linearity, { left = lin0; right = lin1 }) + else Error (Areality, { left = area0; right = area1 }) + (* overriding to report the offending axis *) let submode_log m0 m1 ~log : _ result = match submode_log m0 m1 ~log with | Ok () -> Ok () - | Error { left = area0, lin0, port0; right = area1, lin1, port1 } -> - if Areality.Const.le area0 area1 - then - if Linearity.Const.le lin0 lin1 - then - if Portability.Const.le port0 port1 - then assert false - else Error (Error (Portability, { left = port0; right = port1 })) - else Error (Error (Linearity, { left = lin0; right = lin1 })) - else Error (Error (Areality, { left = area0; right = area1 })) + | Error e -> Error (axis_of_error e) let submode a b = try_with_log (submode_log a b) @@ -1570,10 +1575,8 @@ end [@@inline] module Monadic = struct - module Const = C.Monadic - module Obj = struct - type const = Const.t + type const = C.Monadic_op.t (* Negative solver on the opposite of monadic should give the monadic fragment with original ordering *) @@ -1584,7 +1587,7 @@ module Monadic = struct include Common (Obj) - type error = Error : (Const.t, 'a) C.Axis.t * 'a Solver.error -> error + type error = Error : (Obj.const, 'a) C.Axis.t * 'a Solver.error -> error type equate_error = equate_step * error @@ -1592,6 +1595,27 @@ module Monadic = struct let proj_obj ax = C.proj_obj ax obj + module Const = struct + include C.Monadic + + (* CR zqian: The flipping logic leaking to here is bad. Refactoring needed. *) + + (* Monadic fragment is flipped, so are the following definitions. *) + let min_with ax c = Axis.update ax c (C.max obj) + + let min_axis ax = + let obj = proj_obj ax in + C.max obj + + let max_axis ax = + let obj = proj_obj ax in + C.min obj + + let le_axis ax a b = + let obj = proj_obj ax in + C.le obj b a + end + let proj ax m = Solver.via_monotone (proj_obj ax) (Proj (Obj.obj, ax)) m (* The monadic fragment is inverted. Most of the inversion logic is taken care @@ -1621,17 +1645,19 @@ module Monadic = struct let legacy = of_const Const.legacy + let axis_of_error { left = uni0, con0; right = uni1, con1 } : error = + if Uniqueness.Const.le uni0 uni1 + then + if Contention.Const.le con0 con1 + then assert false + else Error (Contention, { left = con0; right = con1 }) + else Error (Uniqueness, { left = uni0; right = uni1 }) + (* overriding to report the offending axis *) let submode_log m0 m1 ~log : _ result = match submode_log m0 m1 ~log with | Ok () -> Ok () - | Error { left = uni0, con0; right = uni1, con1 } -> - if Uniqueness.Const.le uni0 uni1 - then - if Contention.Const.le con0 con1 - then assert false - else Error (Error (Contention, { left = con0; right = con1 })) - else Error (Error (Uniqueness, { left = uni0; right = uni1 })) + | Error e -> Error (axis_of_error e) let submode a b = try_with_log (submode_log a b) @@ -1809,6 +1835,20 @@ module Value_with (Areality : Areality) = struct let obj = proj_obj ax in C.print obj ppf a + let le_axis : type m a d. (m, a, d) axis -> a -> a -> bool = + fun ax m0 m1 -> + match ax with + | Comonadic ax -> Comonadic.le_axis ax m0 m1 + | Monadic ax -> Monadic.le_axis ax m0 m1 + + let min_axis : type m a d. (m, a, d) axis -> a = function + | Comonadic ax -> Comonadic.min_axis ax + | Monadic ax -> Monadic.min_axis ax + + let max_axis : type m a d. (m, a, d) axis -> a = function + | Comonadic ax -> Comonadic.max_axis ax + | Monadic ax -> Monadic.max_axis ax + let split = split let merge = merge @@ -2100,3 +2140,158 @@ let value_to_alloc_r2l m = (Map_comonadic Regional_to_local) comonadic in { comonadic; monadic } + +module Modality = struct + type ('m, 'a) raw = + | Meet_with : 'a -> (('a, 'l * 'r) mode_comonadic, 'a) raw + | Join_with : 'a -> (('a, 'l * 'r) mode_monadic, 'a) raw + + type t = Atom : ('m, 'a, _) Value.axis * ('m, 'a) raw -> t + + let is_id (Atom (ax, a)) = + match a with + | Join_with c -> Value.Const.le_axis ax c (Value.Const.min_axis ax) + | Meet_with c -> Value.Const.le_axis ax (Value.Const.max_axis ax) c + + let print ppf = function + | Atom (ax, Join_with c) -> + Format.fprintf ppf "join_with(%a)" (C.print (Value.proj_obj ax)) c + | Atom (ax, Meet_with c) -> + Format.fprintf ppf "meet_with(%a)" (C.print (Value.proj_obj ax)) c + + module Monadic = struct + module Mode = Value.Monadic + module Const = Mode.Const + + type t = Join_const : Const.t -> t + + type 'a axis = (Const.t, 'a) Axis.t + + type error = + | Error : 'a axis * (('a, _) mode_monadic, 'a) raw Solver.error -> error + + let sub_log left right ~log:_ : (unit, error) Result.t = + match left, right with + | Join_const c0, Join_const c1 -> + if Const.le c0 c1 + then Ok () + else + let (Error (ax, { left; right })) = + Mode.axis_of_error { left = c0; right = c1 } + in + Error (Error (ax, { left = Join_with left; right = Join_with right })) + + let id = Join_const Const.min + + let cons : type a l r. a axis -> ((a, l * r) mode_monadic, a) raw -> t -> t + = + fun ax a t -> + match a, t with + | Join_with c0, Join_const c -> + Join_const (Const.join (Const.min_with ax c0) c) + | Meet_with _, Join_const _ -> assert false + + let apply : type l r. t -> (l * r) Mode.t -> (l * r) Mode.t = + fun t x -> match t with Join_const c -> Mode.join_const c x + + let to_list = function + | Join_const c -> + [ (let ax : _ Axis.t = Uniqueness in + Atom (Monadic ax, Join_with (Axis.proj ax c))) ] + + let print ppf = function + | Join_const c -> Format.fprintf ppf "join_const(%a)" Const.print c + end + + module Comonadic = struct + module Mode = Value.Comonadic + module Const = Mode.Const + + type t = Meet_const : Const.t -> t + + type 'a axis = (Const.t, 'a) Axis.t + + type error = + | Error : 'a axis * (('a, _) mode_comonadic, 'a) raw Solver.error -> error + + let sub_log left right ~log:_ : (unit, error) Result.t = + match left, right with + | Meet_const c0, Meet_const c1 -> + if Const.le c0 c1 + then Ok () + else + let (Error (ax, { left; right })) = + Mode.axis_of_error { left = c0; right = c1 } + in + Error (Error (ax, { left = Meet_with left; right = Meet_with right })) + + let id = Meet_const Const.max + + let cons : + type a l r. a axis -> ((a, l * r) mode_comonadic, a) raw -> t -> t = + fun ax a t -> + match a, t with + | Meet_with c0, Meet_const c -> + Meet_const (Const.meet (Const.max_with ax c0) c) + | Join_with _, Meet_const _ -> assert false + + let apply : type l r. t -> (l * r) Mode.t -> (l * r) Mode.t = + fun t x -> match t with Meet_const c -> Mode.meet_const c x + + let to_list = function + | Meet_const c -> + [ (let ax : _ Axis.t = Areality in + Atom (Comonadic ax, Meet_with (Axis.proj ax c))); + (let ax : _ Axis.t = Linearity in + Atom (Comonadic ax, Meet_with (Axis.proj ax c))) ] + + let print ppf = function + | Meet_const c -> Format.fprintf ppf "meet_const(%a)" Const.print c + end + + module Value = struct + type t = (Monadic.t, Comonadic.t) monadic_comonadic + + let apply t { monadic; comonadic } = + let monadic = Monadic.apply t.monadic monadic in + let comonadic = Comonadic.apply t.comonadic comonadic in + { monadic; comonadic } + + type error = + | Error : ('m, 'a, _) Value.axis * ('m, 'a) raw Solver.error -> error + + let sub_log : t -> t -> log:_ -> (unit, error) Result.t = + fun t0 t1 ~log -> + match Monadic.sub_log t0.monadic t1.monadic ~log with + | Error (Error (ax, e)) -> Error (Error (Monadic ax, e)) + | Ok () -> ( + match Comonadic.sub_log t0.comonadic t1.comonadic ~log with + | Ok () -> Ok () + | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e))) + + let sub l r = try_with_log (sub_log l r) + + type equate_error = equate_step * error + + let equate m0 m1 = try_with_log (equate_from_submode sub_log m0 m1) + + let id = { monadic = Monadic.id; comonadic = Comonadic.id } + + let cons (Atom (ax, a)) t = + match ax with + | Monadic ax -> + let monadic = Monadic.cons ax a t.monadic in + { t with monadic } + | Comonadic ax -> + let comonadic = Comonadic.cons ax a t.comonadic in + { t with comonadic } + + let singleton a = cons a id + + let to_list { monadic; comonadic } = + Comonadic.to_list comonadic @ Monadic.to_list monadic + + let print ppf ({ monadic; comonadic } : t) = + Format.fprintf ppf "%a,%a" Monadic.print monadic Comonadic.print comonadic + end +end diff --git a/ocaml/typing/mode_intf.mli b/ocaml/typing/mode_intf.mli index f53d1522873..567f7271e1e 100644 --- a/ocaml/typing/mode_intf.mli +++ b/ocaml/typing/mode_intf.mli @@ -89,14 +89,6 @@ module type Common = sig end module type S = sig - module Global_flag : sig - type t = - | Global - | Unrestricted - - val compare : t -> t -> int - end - type changes val undo_changes : changes -> unit @@ -451,4 +443,68 @@ module type S = sig (** Similar to [regional_to_global], behaves as identity on other axes *) val value_to_alloc_r2g : ('l * 'r) Value.t -> ('l * 'r) Alloc.t + + module Modality : sig + type ('m, 'a) raw = + | Meet_with : 'a -> (('a, 'd) mode_comonadic, 'a) raw + (** [Meet_with c] takes [x] and returns [meet c x]. [c] can be [max] + in which case it's the identity modality. *) + | Join_with : 'a -> (('a, 'd) mode_monadic, 'a) raw + (** [Join_with c] takes [x] and returns [join c x]. [c] can be [min] + in which case it's the identity modality. *) + + (** An atom modality is a [raw] accompanied by the axis it acts on. *) + type t = Atom : ('m, 'a, _) Value.axis * ('m, 'a) raw -> t + + (** Test if the given modality is the identity modality. *) + val is_id : t -> bool + + (** Printing for debugging *) + val print : Format.formatter -> t -> unit + + module Value : sig + type atom := t + + (** A modality that acts on [Value] modes. Conceptually it is a sequnce of + [atom] that acts on individual axes. *) + type t + + (** The identity modality. *) + val id : t + + (** Apply a modality on mode. *) + val apply : t -> ('l * 'r) Value.t -> ('l * 'r) Value.t + + (** [cons m t] returns the modality that is [m] after [t]. *) + val cons : atom -> t -> t + + (** [singleton m] returns the modality containing only [m]. *) + val singleton : atom -> t + + (** Returns the list of [atom] in the given modality. The list is + commutative. *) + val to_list : t -> atom list + + type error = + | Error : ('m, 'a, _) Value.axis * ('m, 'a) raw Solver.error -> error + + (** [sub t0 t1] checks that [t0 <= t1]. + Definition: [t0 <= t1] iff [forall a. t0(a) <= t1(a)]. + + In case of failure, [Error (ax, {left; right})] is returned, where + [ax] is the axis on which the modalities disagree. [left] is the + projection of [t0] on [ax], and [right] is the projection of [t1] on + [ax]. *) + val sub : t -> t -> (unit, error) Result.t + + type nonrec equate_error = equate_step * error + + (** [equate t0 t1] checks that [t0 = t1]. + Definition: [t0 = t1] iff [t0 <= t1] and [t1 <= t0]. *) + val equate : t -> t -> (unit, equate_error) Result.t + + (** Printing for debugging. *) + val print : Format.formatter -> t -> unit + end + end end diff --git a/ocaml/typing/oprint.ml b/ocaml/typing/oprint.ml index c1d6230b569..371e55374f6 100644 --- a/ocaml/typing/oprint.ml +++ b/ocaml/typing/oprint.ml @@ -379,9 +379,33 @@ let is_initially_labeled_tuple ty = | Otyp_tuple ((Some _, _) :: _) -> true | _ -> false -let string_of_gbl_space = function - | Ogf_global -> "global_ " - | Ogf_unrestricted -> "" +let print_out_modality_legacy ppf = function + | Ogf_global -> Format.fprintf ppf "global_" + +let print_out_modality ppf = function + | Ogf_legacy m -> print_out_modality_legacy ppf m + | Ogf_new m -> pp_print_string ppf m + +let print_out_modalities_new ppf l = + match l with + | [] -> () + | _ -> + pp_print_space ppf (); + pp_print_string ppf "@@"; + pp_print_space ppf (); + pp_print_list ~pp_sep:pp_print_space pp_print_string ppf l + +let print_out_modalities_legacy = + pp_print_list + (fun ppf m -> + print_out_modality_legacy ppf m; + pp_print_space ppf ()) + +let partition_modalities l = + List.partition_map (function + | Ogf_legacy m -> Left m + | Ogf_new m -> Right m + ) l let rec print_out_type_0 ppf = function @@ -572,14 +596,18 @@ and print_out_label ppf (name, mut, arg, gbl) = | Om_mutable None -> "mutable " | Om_mutable (Some s) -> "mutable(" ^ s ^ ") " in - fprintf ppf "@[<2>%s%s%s :@ %a@];" + let m_legacy, m_new = partition_modalities gbl in + fprintf ppf "@[<2>%s%a%s :@ %a%a@];" mut - (string_of_gbl_space gbl) + print_out_modalities_legacy m_legacy name print_out_type arg + print_out_modalities_new m_new let out_label = ref print_out_label +let out_modality = ref print_out_modality + let out_type = ref print_out_type let out_type_args = ref print_typargs @@ -922,14 +950,10 @@ and print_out_type_decl kwd ppf td = print_unboxed and print_simple_out_gf_type ppf (ty, gf) = - match gf with - | Ogf_global -> - (* See the notes [NON-LEGACY MODES] *) - pp_print_string ppf "global_"; - pp_print_space ppf (); - print_simple_out_type ppf ty - | Ogf_unrestricted -> - print_simple_out_type ppf ty + let m_legacy, m_new = partition_modalities gf in + print_out_modalities_legacy ppf m_legacy; + print_simple_out_type ppf ty; + print_out_modalities_new ppf m_new and print_out_constr_args ppf tyl = print_typlist print_simple_out_gf_type " *" ppf tyl diff --git a/ocaml/typing/oprint.mli b/ocaml/typing/oprint.mli index 6f223acaae7..1a218088042 100644 --- a/ocaml/typing/oprint.mli +++ b/ocaml/typing/oprint.mli @@ -18,12 +18,14 @@ open Outcometree val out_ident : (formatter -> out_ident -> unit) ref val out_value : (formatter -> out_value -> unit) ref -val out_label : (formatter -> string * out_mutability * out_type * out_global -> unit) ref +val out_label : (formatter -> string * out_mutability * out_type + * out_modality list -> unit) ref +val out_modality : (formatter -> out_modality -> unit) ref val out_type : (formatter -> out_type -> unit) ref val out_type_args : (formatter -> out_type list -> unit) ref val out_constr : (formatter -> out_constructor -> unit) ref val out_constr_args : - (formatter -> ((out_type * out_global) list) -> unit) ref + (formatter -> ((out_type * out_modality list) list) -> unit) ref val out_class_type : (formatter -> out_class_type -> unit) ref val out_module_type : (formatter -> out_module_type -> unit) ref val out_sig_item : (formatter -> out_sig_item -> unit) ref diff --git a/ocaml/typing/outcometree.mli b/ocaml/typing/outcometree.mli index f22af086fb8..57950aebc3a 100644 --- a/ocaml/typing/outcometree.mli +++ b/ocaml/typing/outcometree.mli @@ -67,9 +67,13 @@ type out_type_param = oparam_injectivity : Asttypes.injectivity; oparam_jkind : out_jkind option } -type out_global = - | Ogf_global - | Ogf_unrestricted +type out_modality_legacy = Ogf_global + +type out_modality_new = string + +type out_modality = + | Ogf_legacy of out_modality_legacy + | Ogf_new of out_modality_new type out_mutability = | Om_immutable @@ -118,7 +122,7 @@ type out_type = | Otyp_constr of out_ident * out_type list | Otyp_manifest of out_type * out_type | Otyp_object of { fields: (string * out_type) list; open_row:bool} - | Otyp_record of (string * out_mutability * out_type * out_global) list + | Otyp_record of (string * out_mutability * out_type * out_modality list) list | Otyp_stuff of string | Otyp_sum of out_constructor list | Otyp_tuple of (string option * out_type) list @@ -133,7 +137,7 @@ type out_type = and out_constructor = { ocstr_name: string; - ocstr_args: (out_type * out_global) list; + ocstr_args: (out_type * out_modality list) list; ocstr_return_type: (out_vars_jkinds * out_type) option; } @@ -187,7 +191,7 @@ and out_extension_constructor = { oext_name: string; oext_type_name: string; oext_type_params: string list; - oext_args: (out_type * out_global) list; + oext_args: (out_type * out_modality list) list; oext_ret_type: (out_vars_jkinds * out_type) option; oext_private: Asttypes.private_flag } and out_type_extension = diff --git a/ocaml/typing/predef.ml b/ocaml/typing/predef.ml index 6e10a918a47..44e4ec98805 100644 --- a/ocaml/typing/predef.ml +++ b/ocaml/typing/predef.ml @@ -289,7 +289,7 @@ let build_initial_env add_type add_extension empty_env = add_extension id { ext_type_path = path_exn; ext_type_params = []; - ext_args = Cstr_tuple (List.map (fun x -> (x, Global_flag.Unrestricted)) args); + ext_args = Cstr_tuple (List.map (fun x -> (x, Modality.Value.id)) args); ext_arg_jkinds = jkinds; ext_shape = Constructor_uniform_value; ext_constant = args = []; @@ -337,8 +337,8 @@ let build_initial_env add_type add_extension empty_env = ~separability:Separability.Ind ~kind:(fun tvar -> variant [cstr ident_nil []; - cstr ident_cons [tvar, Unrestricted; - type_list tvar, Unrestricted]] + cstr ident_cons [tvar, Modality.Value.id; + type_list tvar, Modality.Value.id]] [| Constructor_uniform_value, [| |]; Constructor_uniform_value, [| list_argument_jkind; @@ -351,7 +351,7 @@ let build_initial_env add_type add_extension empty_env = ~variance:Variance.covariant ~separability:Separability.Ind ~kind:(fun tvar -> - variant [cstr ident_none []; cstr ident_some [tvar, Unrestricted]] + variant [cstr ident_none []; cstr ident_some [tvar, Modality.Value.id]] [| Constructor_uniform_value, [| |]; Constructor_uniform_value, [| option_argument_jkind |]; |]) @@ -363,7 +363,7 @@ let build_initial_env add_type add_extension empty_env = { ld_id=id; ld_mutable=Immutable; - ld_global=Unrestricted; + ld_modalities=Modality.Value.id; ld_type=field_type; ld_jkind=jkind; ld_loc=Location.none; diff --git a/ocaml/typing/printtyp.ml b/ocaml/typing/printtyp.ml index c4d7d4c2627..3723ed25655 100644 --- a/ocaml/typing/printtyp.ml +++ b/ocaml/typing/printtyp.ml @@ -1275,6 +1275,31 @@ let outcome_label : Types.arg_label -> Outcometree.arg_label = function | Optional l -> Optional l | Position l -> Position l +let tree_of_modality_new (t : Mode.Modality.t) = + if Mode.Modality.is_id t then None + else match t with + | Atom (Comonadic Areality, Meet_with Global) -> Some "global" + | Atom (Comonadic Linearity, Meet_with Many) -> Some "many" + | Atom (Monadic Uniqueness, Join_with Shared) -> Some "shared" + | e -> Misc.fatal_errorf "Unexpected modality %a" Mode.Modality.print e + +let tree_of_modality (t : Mode.Modality.t) = + match t with + | Atom (Comonadic Areality, Meet_with Global) -> + Some (Ogf_legacy Ogf_global) + | _ -> Option.map (fun x -> Ogf_new x) (tree_of_modality_new t) + +let tree_of_modalities mutability t = + let l = Mode.Modality.Value.to_list t in + (* CR zqian: decouple mutable and modalities *) + let l = + if Types.is_mutable mutability then + List.filter (fun m -> not @@ Typemode.is_mutable_implied_modality m) l + else + l + in + List.filter_map tree_of_modality l + (** [tree_of_mode m l] finds the outcome node in [l] that corresponds to [m]. Raise if not found. *) let tree_of_mode (mode : 'm option) (l : ('m * out_mode) list) : out_mode option = @@ -1457,12 +1482,7 @@ and tree_of_labeled_typlist mode tyl = List.map (fun (label, ty) -> label, tree_of_typexp mode Alloc.Const.legacy ty) tyl and tree_of_typ_gf (ty, gf) = - let gf = - match gf with - | Global_flag.Global -> Ogf_global - | Global_flag.Unrestricted -> Ogf_unrestricted - in - (tree_of_typexp Type Alloc.Const.legacy ty, gf) + (tree_of_typexp Type Alloc.Const.legacy ty, tree_of_modalities Immutable gf) (** We are on the RHS of an arrow type, where [ty] is the return type, and [m] is the return mode. This function decides the printed modes on [ty]. @@ -1540,6 +1560,11 @@ let tree_of_typexp mode ty = tree_of_typexp mode Alloc.Const.legacy ty let typexp mode ppf ty = !Oprint.out_type ppf (tree_of_typexp mode ty) +let modality ?(id = fun _ppf -> ()) ppf modality = + match tree_of_modality modality with + | None -> id ppf + | Some m -> !Oprint.out_modality ppf m + let prepared_type_expr ppf ty = typexp Type ppf ty let type_expr ppf ty = @@ -1632,24 +1657,24 @@ let param_jkind ty = | _ -> None (* this is (C2.2) from Note [When to print jkind annotations] *) let tree_of_label l = - let mut, gbl = - match l.ld_mutable, l.ld_global with - | Mutable m, _ -> + let mut = + match l.ld_mutable with + | Mutable m -> let mut = if Alloc.Comonadic.Const.eq m Alloc.Comonadic.Const.legacy then Om_mutable None else Om_mutable (Some "") in - mut, Ogf_unrestricted - | Immutable, Global -> Om_immutable, Ogf_global - | Immutable, Unrestricted -> Om_immutable, Ogf_unrestricted + mut + | Immutable -> Om_immutable in - (Ident.name l.ld_id, mut, tree_of_typexp Type l.ld_type, gbl) + let ld_modalities = tree_of_modalities l.ld_mutable l.ld_modalities in + (Ident.name l.ld_id, mut, tree_of_typexp Type l.ld_type, ld_modalities) let tree_of_constructor_arguments = function | Cstr_tuple l -> List.map tree_of_typ_gf l - | Cstr_record l -> [ Otyp_record (List.map tree_of_label l), Ogf_unrestricted ] + | Cstr_record l -> [ Otyp_record (List.map tree_of_label l), [] ] let tree_of_constructor_args_and_ret_type args ret_type = match ret_type with diff --git a/ocaml/typing/printtyp.mli b/ocaml/typing/printtyp.mli index 94f13c6aba6..33b97a33b60 100644 --- a/ocaml/typing/printtyp.mli +++ b/ocaml/typing/printtyp.mli @@ -106,6 +106,10 @@ val reset: unit -> unit [prepared_type_expr]. *) val type_expr: formatter -> type_expr -> unit +(** Prints a modality. If it is the identity modality, prints [id], which + defaults to nothing. *) +val modality : ?id:(formatter -> unit) -> formatter -> Mode.Modality.t -> unit + (** [prepare_for_printing] resets the global printing environment, a la [reset], and prepares the types for printing by reserving names and marking loops. Any type variables that are shared between multiple types in the input list diff --git a/ocaml/typing/subst.ml b/ocaml/typing/subst.ml index f1a8e037d5a..5071e27bd75 100644 --- a/ocaml/typing/subst.ml +++ b/ocaml/typing/subst.ml @@ -402,7 +402,7 @@ let label_declaration copy_scope s l = { ld_id = l.ld_id; ld_mutable = l.ld_mutable; - ld_global = l.ld_global; + ld_modalities = l.ld_modalities; ld_jkind = apply_prepare_jkind s l.ld_jkind l.ld_loc; ld_type = typexp copy_scope s l.ld_loc l.ld_type; ld_loc = loc s l.ld_loc; diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 37ab8289f1b..def69c54cb6 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -435,19 +435,6 @@ let value_regional_to_local mode = |> value_to_alloc_r2l |> alloc_as_value -(* Describes how a modality affects field projection. Returns the mode - of the projection given the mode of the record. *) -let apply_modality - : type l r. _ -> (l * r) Value.t -> (l * r) Value.t - = fun global_flag mode -> - match global_flag with - | Global_flag.Global -> - mode - |> Value.meet_with (Comonadic Areality) Regionality.Const.Global - |> Value.join_with (Monadic Uniqueness) Uniqueness.Const.Shared - |> Value.meet_with (Comonadic Linearity) Linearity.Const.Many - | Global_flag.Unrestricted -> mode - let mode_default mode = { position = RNontail; closure_context = None; @@ -460,7 +447,7 @@ let mode_legacy = mode_default Value.legacy let mode_modality modality expected_mode = expected_mode.mode - |> apply_modality modality + |> Modality.Value.apply modality |> mode_default (* used when entering a function; @@ -2420,12 +2407,12 @@ and type_pat_aux shouldn't be too bad. We can inline this when we upstream this code and combine the two array pattern constructors. *) let ty_elt, arg_sort = solve_Ppat_array ~refine loc env mutability expected_ty in - let modalities : Global_flag.t = - (* CR zqian: decouple mutable and global modality *) - if Types.is_mutable mutability then Global else Unrestricted + let modalities = + if Types.is_mutable mutability then Typemode.mutable_implied_modalities + else Modality.Value.id in check_project_mutability ~loc ~env:!env mutability alloc_mode.mode; - let alloc_mode = apply_modality modalities alloc_mode.mode in + let alloc_mode = Modality.Value.apply modalities alloc_mode.mode in let alloc_mode = simple_pat_mode alloc_mode in let pl = List.map (fun p -> type_pat ~alloc_mode tps Value p ty_elt) spl in rvp { @@ -2668,7 +2655,7 @@ and type_pat_aux let args = List.map2 (fun p (ty, gf) -> - let alloc_mode = apply_modality gf alloc_mode.mode in + let alloc_mode = Modality.Value.apply gf alloc_mode.mode in let alloc_mode = simple_pat_mode alloc_mode in type_pat ~alloc_mode tps Value p ty) sargs (List.combine ty_args_ty ty_args_gf) @@ -2712,7 +2699,7 @@ and type_pat_aux let ty_arg = solve_Ppat_record_field ~refine loc env label label_lid record_ty in check_project_mutability ~loc ~env:!env label.lbl_mut alloc_mode.mode; - let mode = apply_modality label.lbl_global alloc_mode.mode in + let mode = Modality.Value.apply label.lbl_modalities alloc_mode.mode in let alloc_mode = simple_pat_mode mode in (label_lid, label, type_pat tps Value ~alloc_mode sarg ty_arg) in @@ -2735,7 +2722,8 @@ and type_pat_aux let lbl_a_list = List.map type_label_pat lbl_a_list in rvp @@ solve_expected (make_record_pat lbl_a_list) | Ppat_array spl -> - type_pat_array (Mutable Alloc.Comonadic.Const.legacy) spl sp.ppat_attributes + type_pat_array (Mutable Alloc.Comonadic.Const.legacy) + spl sp.ppat_attributes | Ppat_or(sp1, sp2) -> (* Reset pattern forces for just [tps2] because later we append [tps1] and [tps2]'s pattern forces, and we don't want to @@ -5655,7 +5643,7 @@ and type_expect_ in let type_label_exp ((_, label, _) as x) = check_construct_mutability ~loc ~env label.lbl_mut argument_mode; - let argument_mode = mode_modality label.lbl_global argument_mode in + let argument_mode = mode_modality label.lbl_modalities argument_mode in type_label_exp true env argument_mode loc ty_record x in let lbl_exp_list = List.map type_label_exp lbl_a_list in @@ -5717,10 +5705,10 @@ and type_expect_ with_explanation (fun () -> unify_exp_types loc env (instance ty_expected) ty_res2); check_project_mutability ~loc:exp.exp_loc ~env lbl.lbl_mut mode; - let mode = apply_modality lbl.lbl_global mode in + let mode = Modality.Value.apply lbl.lbl_modalities mode in check_construct_mutability ~loc ~env lbl.lbl_mut argument_mode; let argument_mode = - mode_modality lbl.lbl_global argument_mode + mode_modality lbl.lbl_modalities argument_mode in submode ~loc ~env mode argument_mode; Kept (ty_arg1, lbl.lbl_mut, @@ -5768,7 +5756,7 @@ and type_expect_ end ~post:generalize_structure in check_project_mutability ~loc:record.exp_loc ~env label.lbl_mut rmode; - let mode = apply_modality label.lbl_global rmode in + let mode = Modality.Value.apply label.lbl_modalities rmode in let boxing : texp_field_boxing = let is_float_boxing = match label.lbl_repres with @@ -5813,7 +5801,7 @@ and type_expect_ | Mutable m0 -> submode ~loc:record.exp_loc ~env rmode mode_mutate_mutable; let mode = mutable_mode m0 |> mode_default in - let mode = mode_modality label.lbl_global mode in + let mode = mode_modality label.lbl_modalities mode in type_label_exp false env mode loc ty_record (lid, label, snewval) | Immutable -> raise(Error(loc, env, Label_not_mutable lid.txt)) @@ -8741,11 +8729,10 @@ and type_generic_array = let alloc_mode, argument_mode = register_allocation expected_mode in let type_, modalities = - (* CR zqian: decouple mutable and global *) if Types.is_mutable mutability then - Predef.type_array, Global_flag.Global + Predef.type_array, Typemode.mutable_implied_modalities else - Predef.type_iarray, Global_flag.Unrestricted + Predef.type_iarray, Modality.Value.id in check_construct_mutability ~loc ~env mutability argument_mode; let argument_mode = mode_modality modalities argument_mode in diff --git a/ocaml/typing/typedecl.ml b/ocaml/typing/typedecl.ml index d904df0877e..c125ff3d3b3 100644 --- a/ocaml/typing/typedecl.ml +++ b/ocaml/typing/typedecl.ml @@ -421,24 +421,22 @@ let transl_labels ~new_var_jkind ~allow_unboxed env univars closed lbls kloc = pld_attributes=attrs} = Builtin_attributes.warning_scope attrs (fun () -> - let gbl = - match mut with - | Mutable -> Mode.Global_flag.Global - | Immutable -> Typemode.transl_global_flags - (Jane_syntax.Mode_expr.of_attrs arg.ptyp_attributes |> fst) - in let mut : mutability = match mut with | Immutable -> Immutable | Mutable -> Mutable Mode.Alloc.Comonadic.Const.legacy in + let modalities = + Jane_syntax.Mode_expr.of_attrs arg.ptyp_attributes |> fst + in + let modalities = Typemode.transl_modalities mut modalities in let arg = Ast_helper.Typ.force_poly arg in let cty = transl_simple_type ~new_var_jkind env ?univars ~closed Mode.Alloc.Const.legacy arg in {ld_id = Ident.create_local name.txt; ld_name = name; ld_uid = Uid.mk ~current_unit:(Env.get_unit_name ()); ld_mutable = mut; - ld_global = gbl; + ld_modalities = modalities; ld_type = cty; ld_loc = loc; ld_attributes = attrs} ) in @@ -452,7 +450,7 @@ let transl_labels ~new_var_jkind ~allow_unboxed env univars closed lbls kloc = ~allow_unboxed env ld.ld_loc kloc ty; {Types.ld_id = ld.ld_id; ld_mutable = ld.ld_mutable; - ld_global = ld.ld_global; + ld_modalities = ld.ld_modalities; ld_jkind = Jkind.any ~why:Dummy_jkind; (* Updated by [update_label_jkinds] *) ld_type = ty; @@ -468,7 +466,7 @@ let transl_types_gf ~new_var_jkind ~allow_unboxed env loc univars closed tyl kloc = let mk arg = let cty = transl_simple_type ~new_var_jkind env ?univars ~closed Mode.Alloc.Const.legacy arg in - let gf = Typemode.transl_global_flags + let gf = Typemode.transl_modalities Immutable (Jane_syntax.Mode_expr.of_attrs arg.ptyp_attributes |> fst) in (cty, gf) in diff --git a/ocaml/typing/typedtree.ml b/ocaml/typing/typedtree.ml index ff8bc5131d9..d4dc141da2b 100644 --- a/ocaml/typing/typedtree.ml +++ b/ocaml/typing/typedtree.ml @@ -685,7 +685,7 @@ and label_declaration = ld_name: string loc; ld_uid: Uid.t; ld_mutable: mutability; - ld_global: Global_flag.t; + ld_modalities: Modality.Value.t; ld_type: core_type; ld_loc: Location.t; ld_attributes: attribute list; @@ -704,7 +704,7 @@ and constructor_declaration = } and constructor_arguments = - | Cstr_tuple of (core_type * Global_flag.t) list + | Cstr_tuple of (core_type * Modality.Value.t) list | Cstr_record of label_declaration list and type_extension = diff --git a/ocaml/typing/typedtree.mli b/ocaml/typing/typedtree.mli index bdd199496e1..b1b59d8a961 100644 --- a/ocaml/typing/typedtree.mli +++ b/ocaml/typing/typedtree.mli @@ -943,7 +943,7 @@ and label_declaration = ld_name: string loc; ld_uid: Uid.t; ld_mutable: Types.mutability; - ld_global: Mode.Global_flag.t; + ld_modalities: Mode.Modality.Value.t; ld_type: core_type; ld_loc: Location.t; ld_attributes: attributes; @@ -962,7 +962,7 @@ and constructor_declaration = } and constructor_arguments = - | Cstr_tuple of (core_type * Mode.Global_flag.t) list + | Cstr_tuple of (core_type * Mode.Modality.Value.t) list | Cstr_record of label_declaration list and type_extension = diff --git a/ocaml/typing/typemode.ml b/ocaml/typing/typemode.ml index 45370694537..64e5246ed6f 100644 --- a/ocaml/typing/typemode.ml +++ b/ocaml/typing/typemode.ml @@ -57,28 +57,50 @@ let transl_mode_annots modes = in loop Alloc.Const.Option.none modes.txt -let transl_global_flags gfs = - let rec loop (acc : Global_flag.t) = function - | [] -> acc - | m :: rest -> - let { txt; loc } = (m : Mode_expr.Const.t :> _ Location.loc) in - let acc : Global_flag.t = - match txt with - | "global" -> ( - Jane_syntax_parsing.assert_extension_enabled ~loc Mode (); - match acc with - | Unrestricted -> Global - (* Duplicated modality is not an error, just silly and thus a warning. - As we introduce more modalities, it might be in general difficult - to detect all redundant modalities, but we should do our best. *) - | Global -> - Location.prerr_warning loc (Warnings.Redundant_modality txt); - Global) - | s -> raise (Error (loc, Unrecognized_modality s)) - in - loop acc rest +let transl_modality m : Modality.t = + let { txt; loc } = (m : Mode_expr.Const.t :> _ Location.loc) in + Jane_syntax_parsing.assert_extension_enabled ~loc Mode (); + match txt with + | "global" -> Atom (Comonadic Areality, Meet_with Regionality.Const.Global) + | "local" -> Atom (Comonadic Areality, Meet_with Regionality.Const.Local) + | "many" -> Atom (Comonadic Linearity, Meet_with Linearity.Const.Many) + | "once" -> Atom (Comonadic Linearity, Meet_with Linearity.Const.Once) + | "shared" -> Atom (Monadic Uniqueness, Join_with Uniqueness.Const.Shared) + | "unique" -> Atom (Monadic Uniqueness, Join_with Uniqueness.Const.Unique) + | "portable" -> + Atom (Comonadic Portability, Meet_with Portability.Const.Portable) + | "nonportable" -> + Atom (Comonadic Portability, Meet_with Portability.Const.Nonportable) + | "contended" -> + Atom (Monadic Contention, Join_with Contention.Const.Contended) + | "uncontended" -> + Atom (Monadic Contention, Join_with Contention.Const.Uncontended) + | s -> raise (Error (loc, Unrecognized_modality s)) + +let compose_modalities modalities = + (* The ordering: + type r = { x : string @@ foo bar hello } + is interpreted as + x = foo (bar (hello (r))) *) + List.fold_right Modality.Value.cons modalities Modality.Value.id + +let mutable_implied_modalities : Modality.t list = + [ Atom (Comonadic Areality, Meet_with Regionality.Const.Global); + Atom (Comonadic Linearity, Meet_with Linearity.Const.Many); + Atom (Monadic Uniqueness, Join_with Uniqueness.Const.Shared) ] + +let is_mutable_implied_modality m = + (* polymorphic equality suffices for now. *) + List.mem m mutable_implied_modalities + +let transl_modalities mut modalities = + let modalities = List.map transl_modality modalities.txt in + let modalities = + if Types.is_mutable mut + then modalities @ mutable_implied_modalities + else modalities in - loop Unrestricted gfs.txt + compose_modalities modalities let transl_alloc_mode modes = let opt = transl_mode_annots modes in @@ -97,6 +119,8 @@ let report_error ppf = function | Unrecognized_mode s -> fprintf ppf "Unrecognized mode name %s." s | Unrecognized_modality s -> fprintf ppf "Unrecognized modality %s." s +let mutable_implied_modalities = compose_modalities mutable_implied_modalities + let () = Location.register_error_of_exn (function | Error (loc, err) -> Some (Location.error_of_printer ~loc report_error err) diff --git a/ocaml/typing/typemode.mli b/ocaml/typing/typemode.mli index 32da4ed47b7..a9431e62de4 100644 --- a/ocaml/typing/typemode.mli +++ b/ocaml/typing/typemode.mli @@ -6,4 +6,9 @@ val transl_mode_annots : Jane_syntax.Mode_expr.t -> Mode.Alloc.Const.Option.t val transl_alloc_mode : Jane_syntax.Mode_expr.t -> Mode.Alloc.Const.t (** Interpret mode syntax as modalities *) -val transl_global_flags : Jane_syntax.Mode_expr.t -> Mode.Global_flag.t +val transl_modalities : + Types.mutability -> Jane_syntax.Mode_expr.t -> Mode.Modality.Value.t + +val is_mutable_implied_modality : Mode.Modality.t -> bool + +val mutable_implied_modalities : Mode.Modality.Value.t diff --git a/ocaml/typing/types.ml b/ocaml/typing/types.ml index c86e3b61e9f..bab3e9c7b5a 100644 --- a/ocaml/typing/types.ml +++ b/ocaml/typing/types.ml @@ -318,7 +318,7 @@ and label_declaration = { ld_id: Ident.t; ld_mutable: mutability; - ld_global: Mode.Global_flag.t; + ld_modalities: Mode.Modality.Value.t; ld_type: type_expr; ld_jkind : jkind; ld_loc: Location.t; @@ -337,7 +337,7 @@ and constructor_declaration = } and constructor_arguments = - | Cstr_tuple of (type_expr * Mode.Global_flag.t) list + | Cstr_tuple of (type_expr * Mode.Modality.Value.t) list | Cstr_record of label_declaration list type extension_constructor = @@ -561,7 +561,7 @@ type constructor_description = { cstr_name: string; (* Constructor name *) cstr_res: type_expr; (* Type of the result *) cstr_existentials: type_expr list; (* list of existentials *) - cstr_args: (type_expr * Mode.Global_flag.t) list; (* Type of the arguments *) + cstr_args: (type_expr * Mode.Modality.Value.t) list; (* Type of the arguments *) cstr_arg_jkinds: jkind array; (* Jkinds of the arguments *) cstr_arity: int; (* Number of arguments *) cstr_tag: tag; (* Tag for heap blocks *) @@ -692,7 +692,7 @@ type label_description = lbl_res: type_expr; (* Type of the result *) lbl_arg: type_expr; (* Type of the argument *) lbl_mut: mutability; (* Is this a mutable field? *) - lbl_global: Mode.Global_flag.t; (* Is this a global field? *) + lbl_modalities: Mode.Modality.Value.t;(* Is this a global field? *) lbl_jkind : jkind; (* Jkind of the argument *) lbl_pos: int; (* Position in block *) lbl_num: int; (* Position in type *) diff --git a/ocaml/typing/types.mli b/ocaml/typing/types.mli index 32c25c1ae21..b9d60ab0004 100644 --- a/ocaml/typing/types.mli +++ b/ocaml/typing/types.mli @@ -622,7 +622,7 @@ and label_declaration = { ld_id: Ident.t; ld_mutable: mutability; - ld_global: Mode.Global_flag.t; + ld_modalities: Mode.Modality.Value.t; ld_type: type_expr; ld_jkind : jkind; ld_loc: Location.t; @@ -641,7 +641,7 @@ and constructor_declaration = } and constructor_arguments = - | Cstr_tuple of (type_expr * Mode.Global_flag.t) list + | Cstr_tuple of (type_expr * Mode.Modality.Value.t) list | Cstr_record of label_declaration list val tys_of_constr_args : constructor_arguments -> type_expr list @@ -817,7 +817,7 @@ type constructor_description = { cstr_name: string; (* Constructor name *) cstr_res: type_expr; (* Type of the result *) cstr_existentials: type_expr list; (* list of existentials *) - cstr_args: (type_expr * Mode.Global_flag.t) list; (* Type of the arguments *) + cstr_args: (type_expr * Mode.Modality.Value.t) list; (* Type of the arguments *) cstr_arg_jkinds: jkind array; (* Jkinds of the arguments *) cstr_arity: int; (* Number of arguments *) cstr_tag: tag; (* Tag for heap blocks *) @@ -858,7 +858,7 @@ type label_description = lbl_res: type_expr; (* Type of the result *) lbl_arg: type_expr; (* Type of the argument *) lbl_mut: mutability; (* Is this a mutable field? *) - lbl_global: Mode.Global_flag.t; (* Is this a global field? *) + lbl_modalities: Mode.Modality.Value.t; (* Modalities on the field *) lbl_jkind : jkind; (* Jkind of the argument *) lbl_pos: int; (* Position in block *) lbl_num: int; (* Position in the type *) diff --git a/ocaml/typing/uniqueness_analysis.ml b/ocaml/typing/uniqueness_analysis.ml index fcb405056fc..a38522d808a 100644 --- a/ocaml/typing/uniqueness_analysis.ml +++ b/ocaml/typing/uniqueness_analysis.ml @@ -739,18 +739,18 @@ module Paths : sig (** [modal_child gf proj t] is [child prof t] when [gf] is [Unrestricted] and is [untracked] otherwise. *) - val modal_child : Global_flag.t -> Projection.t -> t -> t + val modal_child : Modality.Value.t -> Projection.t -> t -> t (** [tuple_field i t] is [child (Projection.Tuple_field i) t]. *) val tuple_field : int -> t -> t (** [record_field gf s t] is [modal_child gf (Projection.Record_field s) t]. *) - val record_field : Global_flag.t -> string -> t -> t + val record_field : Modality.Value.t -> string -> t -> t (** [construct_field gf s i t] is [modal_child gf (Projection.Construct_field(s, i)) t]. *) - val construct_field : Global_flag.t -> string -> int -> t -> t + val construct_field : Modality.Value.t -> string -> int -> t -> t (** [variant_field s t] is [child (Projection.Variant_field s) t]. *) val variant_field : string -> t -> t @@ -778,9 +778,19 @@ end = struct let child proj t = List.map (UF.Path.child proj) t let modal_child gf proj t = - match gf with - | Global_flag.Global -> untracked - | Global_flag.Unrestricted -> child proj t + (* CR zqian: Instead of just ignoring such children, we should add modality + to [Projection.t] and add corresponding logic in [UsageTree]. *) + let gf = Modality.Value.to_list gf in + let l = + List.filter + (function + | Atom (Monadic Uniqueness, Join_with Shared) -> true + | Atom (Comonadic Linearity, Meet_with Many) -> true + | _ -> false + : Modality.t -> _) + gf + in + if List.length l = 2 then untracked else child proj t let tuple_field i t = child (Projection.Tuple_field i) t @@ -839,7 +849,7 @@ module Value : sig 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.t -> string -> t -> unique_use -> t + val implicit_record_field : Modality.Value.t -> string -> t -> unique_use -> t (** Mark the value as shared_or_unique *) val mark_maybe_unique : t -> UF.t @@ -1055,7 +1065,7 @@ and pattern_match_single pat paths : Ienv.Extension.t * UF.t = let ext, uf_pats = List.map (fun (_, l, pat) -> - let paths = Paths.record_field l.lbl_global l.lbl_name paths in + let paths = Paths.record_field l.lbl_modalities l.lbl_name paths in pattern_match_single pat paths) pats |> conjuncts_pattern_match @@ -1270,7 +1280,7 @@ let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = match field with | l, Kept (_, _, unique_use) -> let value = - Value.implicit_record_field l.lbl_global l.lbl_name value + Value.implicit_record_field l.lbl_modalities l.lbl_name value unique_use in Value.mark_maybe_unique value @@ -1404,7 +1414,7 @@ and check_uniqueness_exp_as_value ienv exp : Value.t * UF.t = let uf_read = Value.mark_implicit_borrow_memory_address Read value in let uf_boxing, value = let occ = Occurrence.mk loc in - let paths = Paths.record_field l.lbl_global l.lbl_name paths in + let paths = Paths.record_field l.lbl_modalities l.lbl_name paths in match float with | Non_boxing unique_use -> UF.unused, Value.existing paths unique_use occ diff --git a/ocaml/utils/warnings.ml b/ocaml/utils/warnings.ml index 5b2661e92b6..ba5f9a1e43b 100644 --- a/ocaml/utils/warnings.ml +++ b/ocaml/utils/warnings.ml @@ -123,7 +123,6 @@ type t = | Probe_name_too_long of string (* 190 *) | Unchecked_zero_alloc_attribute (* 199 *) | Unboxing_impossible (* 210 *) - | Redundant_modality of string (* 250 *) (* If you remove a warning, leave a hole in the numbering. NEVER change the numbers of existing warnings. @@ -211,7 +210,6 @@ let number = function | Probe_name_too_long _ -> 190 | Unchecked_zero_alloc_attribute -> 199 | Unboxing_impossible -> 210 - | Redundant_modality _ -> 250 ;; (* DO NOT REMOVE the ;; above: it is used by the testsuite/ests/warnings/mnemonics.mll test to determine where @@ -583,10 +581,6 @@ let descriptions = [ names = ["unboxing-impossible"]; description = "The parameter or return value corresponding @unboxed attribute cannot be unboxed."; since = since 4 14 }; - { number = 250; - names = ["redundant-modality"]; - description = "The modality is redundant."; - since = since 5 1 }; ] let name_to_number = @@ -1223,8 +1217,6 @@ let message = function Printf.sprintf "This [@unboxed] attribute cannot be used.\n\ The type of this value does not allow unboxing." - | Redundant_modality s -> - Printf.sprintf "This %s modality is redundant." s ;; let nerrors = ref 0 diff --git a/ocaml/utils/warnings.mli b/ocaml/utils/warnings.mli index f25b495aae6..47aad271a2d 100644 --- a/ocaml/utils/warnings.mli +++ b/ocaml/utils/warnings.mli @@ -124,7 +124,6 @@ type t = | Probe_name_too_long of string (* 190 *) | Unchecked_zero_alloc_attribute (* 199 *) | Unboxing_impossible (* 210 *) - | Redundant_modality of string (* 250 *) type alert = {kind:string; message:string; def:loc; use:loc}