From 2ae516c9cf1ee49ef4f6c01d9553e62ec66f0e00 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 31 Jan 2025 14:49:19 -0500 Subject: [PATCH 01/20] `local` implies `yielding` --- lambda/translcore.ml | 5 +- typing/ctype.ml | 60 +++++++++++++++--------- typing/ctype.mli | 5 +- typing/mode.ml | 4 ++ typing/mode_intf.mli | 4 ++ typing/printtyp.ml | 11 ++++- typing/typemode.ml | 106 +++++++++++++++++++++++++++++++++++++++---- 7 files changed, 160 insertions(+), 35 deletions(-) diff --git a/lambda/translcore.ml b/lambda/translcore.ml index 00cdb6ffa4a..dce17c944d8 100644 --- a/lambda/translcore.ml +++ b/lambda/translcore.ml @@ -325,7 +325,10 @@ let can_apply_primitive p pmode pos args = else if nargs < p.prim_arity then false else if pos <> Typedtree.Tail then true else begin - let return_mode = Ctype.prim_mode pmode p.prim_native_repr_res in + let return_mode, _ = + Ctype.prim_mode + pmode (Some (Mode.Yielding.newvar ())) p.prim_native_repr_res + in is_heap_mode (transl_locality_mode_l return_mode) end end diff --git a/typing/ctype.ml b/typing/ctype.ml index 51223c919a6..45e42eae9a1 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1662,22 +1662,37 @@ let instance_label ~fixed lbl = (vars, ty_arg, ty_res) ) -let prim_mode mvar = function - | Primitive.Prim_global, _ -> Locality.allow_right Locality.global - | Primitive.Prim_local, _ -> Locality.allow_right Locality.local +(* CR dkalinichenko: we must vary yieldingness together with locality to get + sane behavior around defaults. Remove once we have mode polymorphism. *) +let prim_mode mvar mvar' = function + | Primitive.Prim_global, _ -> + Locality.allow_right Locality.global, + Yielding.allow_right Yielding.unyielding + | Primitive.Prim_local, _ -> + Locality.allow_right Locality.local, + Yielding.allow_right Yielding.yielding | Primitive.Prim_poly, _ -> - match mvar with - | Some mvar -> mvar - | None -> assert false - -(** Returns a new mode variable whose locality is the given locality, while - all other axes are from the given [m]. This function is too specific to be - put in [mode.ml] *) -let with_locality locality m = + match mvar, mvar' with + | Some mvar, Some mvar' -> mvar, mvar' + | None, _ | _, None -> assert false + +(** Returns a new mode variable whose locality is the given locality and + whose yieldingness is the given yieldingness, while all other axes are + from the given [m]. This function is too specific to be put in [mode.ml] *) +let with_locality_and_yielding (locality, yielding) m = let m' = Alloc.newvar () in Locality.equate_exn (Alloc.proj (Comonadic Areality) m') locality; - Alloc.submode_exn m' (Alloc.join_with (Comonadic Areality) Locality.Const.max m); - Alloc.submode_exn (Alloc.meet_with (Comonadic Areality) Locality.Const.min m) m'; + Yielding.equate_exn (Alloc.proj (Comonadic Yielding) m') yielding; + Alloc.submode_exn m' + (Alloc.join_with + (Comonadic Yielding) + Yielding.Const.max + (Alloc.join_with (Comonadic Areality) Locality.Const.max m)); + Alloc.submode_exn + (Alloc.meet_with + (Comonadic Areality) + Locality.Const.min + (Alloc.meet_with (Comonadic Yielding) Yielding.Const.min m)) m'; m' let curry_mode alloc arg : Alloc.Const.t = @@ -1701,10 +1716,12 @@ let curry_mode alloc arg : Alloc.Const.t = of the return of a function). *) {acc with uniqueness=Uniqueness.Const.Aliased} -let rec instance_prim_locals locals mvar macc finalret ty = +let rec instance_prim_locals locals mvar_l mvar_y macc (loc, yld) ty = match locals, get_desc ty with | l :: locals, Tarrow ((lbl,marg,mret),arg,ret,commu) -> - let marg = with_locality (prim_mode (Some mvar) l) marg in + let marg = with_locality_and_yielding + (prim_mode (Some mvar_l) (Some mvar_y) l) marg + in let macc = Alloc.join [ Alloc.disallow_right mret; @@ -1714,12 +1731,12 @@ let rec instance_prim_locals locals mvar macc finalret ty = in let mret = match locals with - | [] -> with_locality finalret mret + | [] -> with_locality_and_yielding (loc, yld) mret | _ :: _ -> let mret', _ = Alloc.newvar_above macc in (* curried arrow *) mret' in - let ret = instance_prim_locals locals mvar macc finalret ret in + let ret = instance_prim_locals locals mvar_l mvar_y macc (loc, yld) ret in newty2 ~level:(get_level ty) (Tarrow ((lbl,marg,mret),arg,ret, commu)) | _ :: _, _ -> assert false | [], _ -> @@ -1796,11 +1813,12 @@ let instance_prim_mode (desc : Primitive.description) ty = let is_poly = function Primitive.Prim_poly, _ -> true | _ -> false in if is_poly desc.prim_native_repr_res || List.exists is_poly desc.prim_native_repr_args then - let mode = Locality.newvar () in - let finalret = prim_mode (Some mode) desc.prim_native_repr_res in + let mode_l = Locality.newvar () in + let mode_y = Yielding.newvar () in + let finalret = prim_mode (Some mode_l) (Some mode_y) desc.prim_native_repr_res in instance_prim_locals desc.prim_native_repr_args - mode (Alloc.disallow_right Alloc.legacy) finalret ty, - Some mode + mode_l mode_y (Alloc.disallow_right Alloc.legacy) finalret ty, + Some mode_l else ty, None diff --git a/typing/ctype.mli b/typing/ctype.mli index 68908817691..a8daf25658c 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -222,8 +222,11 @@ val instance_label: _ gen_label_description -> type_expr list * type_expr * type_expr (* Same, for a label *) val prim_mode : - (Mode.allowed * 'r) Mode.Locality.t option -> (Primitive.mode * Primitive.native_repr) + (Mode.allowed * 'r) Mode.Locality.t option + -> (Mode.allowed * 'r) Mode.Yielding.t option + -> (Primitive.mode * Primitive.native_repr) -> (Mode.allowed * 'r) Mode.Locality.t + * (Mode.allowed * 'r) Mode.Yielding.t val instance_prim: Primitive.description -> type_expr -> type_expr * Mode.Locality.lr option * Jkind.Sort.t option diff --git a/typing/mode.ml b/typing/mode.ml index 6c790605bfc..ba04140c2e4 100644 --- a/typing/mode.ml +++ b/typing/mode.ml @@ -1715,6 +1715,10 @@ module Yielding = struct include Common (Obj) + let yielding = of_const Yielding + + let unyielding = of_const Unyielding + let legacy = of_const Const.legacy let zap_to_legacy = zap_to_floor diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli index 8016e8b63b1..e8885056068 100644 --- a/typing/mode_intf.mli +++ b/typing/mode_intf.mli @@ -287,6 +287,10 @@ module type S = sig with module Const := Const and type error := error and type 'd t = (Const.t, 'd) mode_comonadic + + val yielding : lr + + val unyielding : lr end type 'a comonadic_with = diff --git a/typing/printtyp.ml b/typing/printtyp.ml index e28083ce475..4242791523c 100644 --- a/typing/printtyp.ml +++ b/typing/printtyp.ml @@ -1422,8 +1422,14 @@ Raise if not found. *) let tree_of_mode (mode : 'm option) (l : ('m * out_mode) list) : out_mode option = Option.map (fun x -> List.assoc x l) mode -let tree_of_modes modes = +let tree_of_modes (modes : Mode.Alloc.Const.t) = let diff = Mode.Alloc.Const.diff modes Mode.Alloc.Const.legacy in + (* [yielding] has custom defaults depending on [areality]: *) + let diff_yielding = + match modes.areality, modes.yielding with + | Local, Yielding | Global, Unyielding -> None + | _, _ -> Some modes.yielding + in (* The mapping passed to [tree_of_mode] must cover all non-legacy modes *) let l = [ tree_of_mode diff.areality [Mode.Locality.Const.Local, Omd_legacy Omd_local]; @@ -1432,7 +1438,8 @@ let tree_of_modes modes = tree_of_mode diff.portability [Mode.Portability.Const.Portable, Omd_new "portable"]; tree_of_mode diff.contention [Mode.Contention.Const.Contended, Omd_new "contended"; Mode.Contention.Const.Shared, Omd_new "shared"]; - tree_of_mode diff.yielding [Mode.Yielding.Const.Yielding, Omd_new "yielding"]] + tree_of_mode diff_yielding [Mode.Yielding.Const.Yielding, Omd_new "yielding"; + Mode.Yielding.Const.Unyielding, Omd_new "unyielding"]] in List.filter_map Fun.id l diff --git a/typing/typemode.ml b/typing/typemode.ml index 617ea9cb6bd..761bcf986d0 100644 --- a/typing/typemode.ml +++ b/typing/typemode.ml @@ -153,7 +153,27 @@ let transl_modifier_annots annots = Transled_modifiers.set ~axis modifiers_so_far (Some { txt = mode; loc }) in let empty_modifiers = Transled_modifiers.empty in - List.fold_left step empty_modifiers annots + let modifiers = List.fold_left step empty_modifiers annots in + (* Since [yielding] is the default mode in presence of [local], + the [global] modifier must also apply [unyielding] unless specified. *) + match Transled_modifiers.get ~axis:(Modal (Comonadic Yielding)) modifiers, + Transled_modifiers.get ~axis:(Modal (Comonadic Areality)) modifiers with + | None, Some { txt = Locality.Const.Global; _ } -> + Transled_modifiers.set ~axis:(Modal (Comonadic Yielding)) + modifiers (Some { txt = Yielding.Const.Unyielding; loc = Location.none }) + | _, _ -> modifiers + + +let default_mode_annots (annots : Alloc.Const.Option.t) = + (* Unlike all other modes, [yielding] has a different default + depending on whether [areality] is [Global] or [Local]. *) + let yielding = + match annots.yielding, annots.areality with + | (Some _ as y), _ | y, None -> y + | None, Some Locality.Const.Global -> Some Yielding.Const.Unyielding + | None, Some Locality.Const.Local -> Some Yielding.Const.Yielding + in + { annots with yielding } let transl_mode_annots annots : Alloc.Const.Option.t = let step modifiers_so_far annot = @@ -172,13 +192,14 @@ let transl_mode_annots annots : Alloc.Const.Option.t = in let empty_modifiers = Transled_modifiers.empty in let modes = List.fold_left step empty_modifiers annots in - { areality = Option.map get_txt modes.locality; - linearity = Option.map get_txt modes.linearity; - uniqueness = Option.map get_txt modes.uniqueness; - portability = Option.map get_txt modes.portability; - contention = Option.map get_txt modes.contention; - yielding = Option.map get_txt modes.yielding - } + default_mode_annots + { areality = Option.map get_txt modes.locality; + linearity = Option.map get_txt modes.linearity; + uniqueness = Option.map get_txt modes.uniqueness; + portability = Option.map get_txt modes.portability; + contention = Option.map get_txt modes.contention; + yielding = Option.map get_txt modes.yielding + } let untransl_mode_annots ~loc (modes : Mode.Alloc.Const.Option.t) = let print_to_string_opt print a = Option.map (Format.asprintf "%a" print) a in @@ -195,7 +216,15 @@ let untransl_mode_annots ~loc (modes : Mode.Alloc.Const.Option.t) = let contention = print_to_string_opt Mode.Contention.Const.print modes.contention in - let yielding = print_to_string_opt Mode.Yielding.Const.print modes.yielding in + let yielding = + (* Since [yielding] has non-standard defaults, we special-case + whether we want to print it here. *) + match modes.yielding, modes.areality with + | Some Yielding.Const.Yielding, Some Locality.Const.Local + | Some Yielding.Const.Unyielding, Some Locality.Const.Global -> + None + | _, _ -> print_to_string_opt Mode.Yielding.Const.print modes.yielding + in List.filter_map (fun x -> Option.map (fun s -> { txt = Parsetree.Mode s; loc }) x) [areality; uniqueness; linearity; portability; contention; yielding] @@ -269,9 +298,37 @@ let mutable_implied_modalities (mut : Types.mutability) attrs = then monadic else monadic @ comonadic +(* Since [yielding] is the default mode in presence of [local], + the [global] modality must also apply [unyielding] unless specified. *) +let default_modalities (modalities : Modality.t list) = + let areality = + List.find_map + (function + | Modality.Atom (Comonadic Areality, Meet_with a) -> + Some (a : Regionality.Const.t) + | _ -> None) + modalities + in + let yielding = + List.find_map + (function + | Modality.Atom (Comonadic Yielding, Meet_with y) -> + Some (y : Yielding.Const.t) + | _ -> None) + modalities + in + let extra = + match areality, yielding with + | Some Global, None -> + [Modality.Atom (Comonadic Yielding, Meet_with Yielding.Const.Unyielding)] + | _, _ -> [] + in + modalities @ extra + let transl_modalities ~maturity mut attrs modalities = let mut_modalities = mutable_implied_modalities mut attrs in let modalities = List.map (transl_modality ~maturity) modalities in + let modalities = default_modalities modalities in (* mut_modalities is applied before explicit modalities *) Modality.Value.Const.id |> List.fold_right @@ -285,9 +342,38 @@ let transl_modalities ~maturity mut attrs modalities = (fun atom m -> Modality.Value.Const.compose ~then_:atom m) modalities +let untransl_yielding l = + let areality = + List.find_map + (function + | Modality.Atom (Comonadic Areality, Meet_with a) -> + Some (a : Regionality.Const.t) + | _ -> None) + l + in + let yielding = + List.find_map + (function + | Modality.Atom (Comonadic Yielding, Meet_with y) -> + Some (y : Yielding.Const.t) + | _ -> None) + l + in + match areality, yielding with + | Some Global, Some Unyielding | Some Local, Some Yielding -> [] + | _, Some yld -> [Modality.Atom (Comonadic Yielding, Meet_with yld)] + | _, None -> [] + let untransl_modalities mut attrs t = let l = Modality.Value.Const.to_list t in - let l = List.filter (fun a -> not @@ Modality.is_id a) l in + let l = + untransl_yielding l + @ List.filter + (function + | Modality.Atom (Comonadic Yielding, _) -> false + | a -> not (Modality.is_id a)) + l + in let mut_modalities = mutable_implied_modalities mut attrs in (* polymorphic equality suffices for now. *) let l = List.filter (fun x -> not @@ List.mem x mut_modalities) l in From 29c5fc2b1f1a203b8218b891a1bf7a1208b1fdc6 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 31 Jan 2025 14:49:37 -0500 Subject: [PATCH 02/20] accept tests --- .../tests/parsetree/source_jane_street.ml | 30 ++++++- testsuite/tests/typing-local/exclave.ml | 10 +-- testsuite/tests/typing-local/local-layouts.ml | 4 +- testsuite/tests/typing-local/local.ml | 86 ++++++++++++------- testsuite/tests/typing-modes/crossing.ml | 8 +- testsuite/tests/typing-modes/lazy.ml | 2 +- testsuite/tests/typing-modes/modes.ml | 17 +++- testsuite/tests/typing-modes/stack.ml | 2 +- testsuite/tests/typing-unique/overwriting.ml | 2 +- testsuite/tests/typing-unique/unique.ml | 2 +- 10 files changed, 114 insertions(+), 49 deletions(-) diff --git a/testsuite/tests/parsetree/source_jane_street.ml b/testsuite/tests/parsetree/source_jane_street.ml index 9d125e71d73..9a9f897f963 100644 --- a/testsuite/tests/parsetree/source_jane_street.ml +++ b/testsuite/tests/parsetree/source_jane_street.ml @@ -492,6 +492,23 @@ let f ~(x1 @ many) stack_ (x1, x2, x3, x4, x5, x9, x10, x11, (* x12, *) x13, x14, x15) [%%expect{| +val f : + ('b : value_or_null) ('c : value_or_null) ('d : value_or_null) 'e. + x1:'b -> + x2:local_ string -> local_ + (x3:local_ (string -> string) -> + x4:local_ ('a. 'a -> 'a) -> + x5:local_ 'c -> + x6:local_ bool -> + x7:local_ bool -> + x8:local_ unit -> + string -> + local_ 'd -> local_ + 'b * string * (string -> string) * ('e -> 'e) * 'c * string * string * + int array * string * (int -> local_ (int -> int) @ unyielding) * + (int -> local_ (int -> int) @ unyielding) @ contended) @ unyielding = + +|}, Principal{| val f : x1:'b -> x2:local_ string -> @@ -504,8 +521,8 @@ val f : string -> local_ 'd -> local_ 'b * string * (string -> string) * ('e -> 'e) * 'c * string * string * - int array * string * (int -> local_ (int -> int)) * - (int -> local_ (int -> int)) @ contended = + int array * string * (int -> local_ (int -> int) @ unyielding) * + (int -> local_ (int -> int) @ unyielding) @ contended = |}] let f1 (_ @ local) = () @@ -585,7 +602,14 @@ Error: This value escapes its region. let f2 (x @ local) (f @ once) : t2 = exclave_ { x; f } [%%expect{| -val f2 : local_ float -> (float -> float) @ once -> local_ t2 @ once = +val f2 : + local_ float -> local_ + ((float -> float) @ once -> local_ t2 @ once unyielding) @ unyielding = + +|}, Principal{| +val f2 : + local_ float -> (float -> float) @ once -> local_ t2 @ once unyielding = + |}] diff --git a/testsuite/tests/typing-local/exclave.ml b/testsuite/tests/typing-local/exclave.ml index f4948e33919..6f41c8d3246 100644 --- a/testsuite/tests/typing-local/exclave.ml +++ b/testsuite/tests/typing-local/exclave.ml @@ -36,7 +36,7 @@ let foo () = let _ = escape x in x [%%expect{| -val foo : unit -> local_ int option = +val foo : unit -> local_ int option @ unyielding = |}] (* this still applies even when the exclave doesn't allocate in outer region at all, @@ -48,7 +48,7 @@ let foo x = let _ = escape x in x [%%expect{| -val foo : 'a -> local_ int option = +val foo : 'a -> local_ int option @ unyielding = |}] @@ -196,8 +196,8 @@ let f () = f ();; [%%expect{| type 'a glob = Glob of global_ 'a -val return_local : 'a -> local_ 'a glob = -val f : unit -> local_ unit = +val return_local : 'a -> local_ 'a glob @ unyielding = +val f : unit -> local_ unit @ unyielding = - : unit = () |}] @@ -233,7 +233,7 @@ let f () = (fun x -> fun y -> ()) : (string -> string -> unit) ) [%%expect{| -val f : unit -> local_ (string -> (string -> unit)) = +val f : unit -> local_ (string -> (string -> unit)) @ unyielding = |}] let f : local_ string -> string = diff --git a/testsuite/tests/typing-local/local-layouts.ml b/testsuite/tests/typing-local/local-layouts.ml index b07f65b5699..45a4786cdf7 100644 --- a/testsuite/tests/typing-local/local-layouts.ml +++ b/testsuite/tests/typing-local/local-layouts.ml @@ -6,6 +6,6 @@ let foo _t (type a) = exclave_ 1 let bar _t (type a : value) = exclave_ 2 [%%expect{| -val foo : 'a -> local_ int = -val bar : 'a -> local_ int = +val foo : 'a -> local_ int @ unyielding = +val bar : 'a -> local_ int @ unyielding = |}] diff --git a/testsuite/tests/typing-local/local.ml b/testsuite/tests/typing-local/local.ml index b186d0e488e..cb0366fa27d 100644 --- a/testsuite/tests/typing-local/local.ml +++ b/testsuite/tests/typing-local/local.ml @@ -378,6 +378,8 @@ val foo : ?x:local_ 'a -> unit -> local_ 'a option = let foo ?(local_ x = "hello") () = x;; [%%expect{| +val foo : ?x:local_ string -> unit -> local_ string @ unyielding = +|}, Principal{| val foo : ?x:local_ string -> unit -> local_ string = |}] @@ -897,7 +899,7 @@ let foo x = exclave_ let r = local_ { contents = x } in print r [%%expect{| -val foo : string -> local_ unit = +val foo : string -> local_ unit @ unyielding = |}] (* Can pass local values to calls explicitly marked as nontail *) @@ -944,7 +946,7 @@ let foo x = exclave_ let local_ foo () = r.contents in foo () [%%expect{| -val foo : 'a -> local_ 'a = +val foo : 'a -> local_ 'a @ unyielding = |}] (* Cannot return local values without annotations on all exits *) @@ -1004,14 +1006,14 @@ let foo () = exclave_ let _ = local_ (52, 24) in 42 [%%expect{| -val foo : unit -> local_ int = +val foo : unit -> local_ int @ unyielding = |}] let bar () = let _x = 52 in foo () [%%expect{| -val bar : unit -> local_ int = +val bar : unit -> local_ int @ unyielding = |}] (* if not at tail, then not affected *) @@ -1746,17 +1748,25 @@ Line 2, characters 2-32: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Signature mismatch: Modules do not match: - sig val add : local_ int32 -> local_ int32 -> local_ int32 end + sig + val add : + local_ int32 @ unyielding -> + local_ int32 @ unyielding -> local_ int32 @ unyielding + end is not included in sig val add : local_ int32 -> local_ int32 -> int32 end Values do not match: - val add : local_ int32 -> local_ int32 -> local_ int32 + val add : + local_ int32 @ unyielding -> + local_ int32 @ unyielding -> local_ int32 @ unyielding is not included in val add : local_ int32 -> local_ int32 -> int32 - The type "local_ int32 -> local_ int32 -> local_ int32" + The type + "local_ int32 @ unyielding -> + local_ int32 @ unyielding -> local_ int32 @ unyielding" is not compatible with the type "local_ int32 -> local_ int32 -> int32" - Type "local_ int32 -> local_ int32" is not compatible with type - "local_ int32 -> int32" + Type "local_ int32 @ unyielding -> local_ int32 @ unyielding" + is not compatible with type "local_ int32 -> int32" |}] module Opt32 : sig external add : (int32[@local_opt]) -> (int32[@local_opt]) -> (int32[@local_opt]) = "%int32_add" end = Int32 module Bad32_2 : sig val add : local_ int32 -> local_ int32 -> int32 end = @@ -1786,10 +1796,12 @@ Error: Signature mismatch: (int32 [@local_opt]) -> (int32 [@local_opt]) = "%int32_add" is not included in val add : local_ int32 -> local_ int32 -> int32 - The type "local_ int32 -> local_ int32 -> local_ int32" + The type + "local_ int32 @ unyielding -> + local_ int32 @ unyielding -> local_ int32 @ unyielding" is not compatible with the type "local_ int32 -> local_ int32 -> int32" - Type "local_ int32 -> local_ int32" is not compatible with type - "local_ int32 -> int32" + Type "local_ int32 @ unyielding -> local_ int32 @ unyielding" + is not compatible with type "local_ int32 -> int32" |}] module Contravariant_instantiation : sig @@ -1825,11 +1837,25 @@ let nativeint (local_ x) (local_ y) = exclave_ let float (local_ x) (local_ y) = exclave_ (x +. y *. x -. 42.) [%%expect{| -val int32 : local_ int32 -> local_ int32 -> local_ int32 = -val int64 : local_ int64 -> local_ int64 -> local_ int64 = -val nativeint : local_ nativeint -> local_ nativeint -> local_ nativeint = +val int32 : + local_ int32 -> local_ + (local_ int32 -> local_ int32 @ unyielding) @ unyielding = +val int64 : + local_ int64 -> local_ + (local_ int64 -> local_ int64 @ unyielding) @ unyielding = +val nativeint : + local_ nativeint -> local_ + (local_ nativeint -> local_ nativeint @ unyielding) @ unyielding = +val float : + local_ float -> local_ + (local_ float -> local_ float @ unyielding) @ unyielding = +|}, Principal{| +val int32 : local_ int32 -> local_ int32 -> local_ int32 @ unyielding = +val int64 : local_ int64 -> local_ int64 -> local_ int64 @ unyielding = +val nativeint : + local_ nativeint -> local_ nativeint -> local_ nativeint @ unyielding = -val float : local_ float -> local_ float -> local_ float = +val float : local_ float -> local_ float -> local_ float @ unyielding = |}] let etapair (local_ x) = exclave_ (fst x, snd x) @@ -1887,8 +1913,8 @@ Error: This value escapes its region. let foo () = exclave_ let local_ _x = "hello" in true let testboo3 () = true && (foo ()) [%%expect{| -val foo : unit -> local_ bool = -val testboo3 : unit -> local_ bool = +val foo : unit -> local_ bool @ unyielding = +val testboo3 : unit -> local_ bool @ unyielding = |}] (* Test from Nathanaëlle Courant. @@ -2440,7 +2466,7 @@ Error: This value escapes its region. (* constructing local iarray from local elements is fine *) let f (local_ x : string) = exclave_ [:x; "foo":] [%%expect{| -val f : local_ string -> local_ string iarray = +val f : local_ string -> local_ string iarray @ unyielding = |}] (* constructing global iarray from global elements is fine *) @@ -2479,7 +2505,7 @@ let f (local_ a : string iarray) = | [: x; _ :] -> x | _ -> "foo" [%%expect{| -val f : local_ string iarray -> local_ string = +val f : local_ string iarray -> local_ string @ unyielding = |}] (* projecting out of global iarray gives global elements *) @@ -2506,7 +2532,7 @@ Error: This value escapes its region. (* constructing local array from global elements is allowed *) let f (x : string) = exclave_ [| x |] [%%expect{| -val f : string -> local_ string array = +val f : string -> local_ string array @ unyielding = |}] (* projecting out of local array gives global elements *) @@ -2560,16 +2586,18 @@ Lines 3-6, characters 6-3: Error: Signature mismatch: Modules do not match: sig - val g : 'a -> 'b -> local_ string - val f : 'a -> local_ ('b -> local_ string) + val g : 'a -> 'b -> local_ string @ unyielding + val f : + 'a -> local_ ('b -> local_ string @ unyielding) @ unyielding end is not included in sig val f : string -> string -> local_ string end Values do not match: - val f : 'a -> local_ ('b -> local_ string) + val f : 'a -> local_ ('b -> local_ string @ unyielding) @ unyielding is not included in val f : string -> string -> local_ string - The type "string -> local_ (string -> local_ string)" + The type + "string -> local_ (string -> local_ string @ unyielding) @ unyielding" is not compatible with the type "string -> string -> local_ string" |}] @@ -2641,13 +2669,13 @@ val f : unit -> local_ string -> (string -> string) = let f () = exclave_ ((fun x -> fun y -> x + y) : (_ -> _));; [%%expect{| -val f : unit -> local_ (int -> (int -> int)) = +val f : unit -> local_ (int -> (int -> int)) @ unyielding = |}];; (* ok if curried *) let f () = exclave_ ((fun x -> (fun y -> x + y) [@extension.curry]) : (_ -> _));; [%%expect{| -val f : unit -> local_ (int -> (int -> int)) = +val f : unit -> local_ (int -> (int -> int)) @ unyielding = |}];; (* Type annotations on a [local_] binding are interpreted in a local context, @@ -2737,12 +2765,12 @@ val _ret : unit -> M.t -> unit = let _ret () : M.t -> unit = exclave_ (fun M_constructor -> ()) [%%expect{| -val _ret : unit -> local_ (M.t -> unit) = +val _ret : unit -> local_ (M.t -> unit) @ unyielding = |}] let _ret () : M.t -> unit = exclave_ (fun M_constructor -> ()) [%%expect{| -val _ret : unit -> local_ (M.t -> unit) = +val _ret : unit -> local_ (M.t -> unit) @ unyielding = |}] type r = {global_ x : string; y : string} diff --git a/testsuite/tests/typing-modes/crossing.ml b/testsuite/tests/typing-modes/crossing.ml index 51b9d9f3f4a..20ad39423b3 100644 --- a/testsuite/tests/typing-modes/crossing.ml +++ b/testsuite/tests/typing-modes/crossing.ml @@ -68,15 +68,15 @@ Lines 3-5, characters 6-3: 5 | end Error: Signature mismatch: Modules do not match: - sig val f : unit -> local_ int end + sig val f : unit -> local_ int @ unyielding end is not included in sig val f : unit -> int end Values do not match: - val f : unit -> local_ int + val f : unit -> local_ int @ unyielding is not included in val f : unit -> int - The type "unit -> local_ int" is not compatible with the type - "unit -> int" + The type "unit -> local_ int @ unyielding" + is not compatible with the type "unit -> int" |}] module M : sig diff --git a/testsuite/tests/typing-modes/lazy.ml b/testsuite/tests/typing-modes/lazy.ml index fd834b214e5..2b1eaecc6eb 100644 --- a/testsuite/tests/typing-modes/lazy.ml +++ b/testsuite/tests/typing-modes/lazy.ml @@ -40,7 +40,7 @@ let foo (x @ local) = match x with | lazy y -> y [%%expect{| -val foo : local_ 'a lazy_t -> 'a = +val foo : local_ 'a lazy_t -> 'a @ yielding = |}] (* one can construct [portable] lazy only if the result is [portable] *) diff --git a/testsuite/tests/typing-modes/modes.ml b/testsuite/tests/typing-modes/modes.ml index 39d880861f3..199e843825a 100644 --- a/testsuite/tests/typing-modes/modes.ml +++ b/testsuite/tests/typing-modes/modes.ml @@ -482,11 +482,11 @@ let local_ret a = exclave_ (Some a) let bad_use = use_global_ret local_ret "hello" [%%expect{| val use_global_ret : ('a -> 'b) -> 'a -> 'b lazy_t = -val local_ret : 'a -> local_ 'a option = +val local_ret : 'a -> local_ 'a option @ unyielding = Line 3, characters 29-38: 3 | let bad_use = use_global_ret local_ret "hello" ^^^^^^^^^ -Error: This expression has type "'a -> local_ 'a option" +Error: This expression has type "'a -> local_ 'a option @ unyielding" but an expression was expected of type "'b -> 'c" |}] @@ -559,6 +559,12 @@ let result = use_local foo 1. 2. val use_local : local_ ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = val use_global : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = val foo : float -> float -> float = +val bar : local_ float -> local_ (local_ float -> unit) @ unyielding = +val result : float = 3. +|}, Principal{| +val use_local : local_ ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = +val use_global : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = +val foo : float -> float -> float = val bar : local_ float -> local_ float -> unit = val result : float = 3. |}] @@ -576,6 +582,13 @@ val result : float = 3. let result = use_global bar 1. 2. [%%expect{| Line 1, characters 24-27: +1 | let result = use_global bar 1. 2. + ^^^ +Error: This expression has type + "local_ float -> local_ (local_ float -> unit) @ unyielding" + but an expression was expected of type "local_ 'a -> ('b -> 'c)" +|}, Principal{| +Line 1, characters 24-27: 1 | let result = use_global bar 1. 2. ^^^ Error: This expression has type "local_ float -> local_ float -> unit" diff --git a/testsuite/tests/typing-modes/stack.ml b/testsuite/tests/typing-modes/stack.ml index 062b70e3225..6477d0ff8f5 100644 --- a/testsuite/tests/typing-modes/stack.ml +++ b/testsuite/tests/typing-modes/stack.ml @@ -202,7 +202,7 @@ Error: This value escapes its region. let f () = exclave_ stack_ (3, 5) [%%expect{| -val f : unit -> local_ int * int = +val f : unit -> local_ int * int @ unyielding = |}] let f () = diff --git a/testsuite/tests/typing-unique/overwriting.ml b/testsuite/tests/typing-unique/overwriting.ml index 1ad6c335fc4..d73e6ae3358 100644 --- a/testsuite/tests/typing-unique/overwriting.ml +++ b/testsuite/tests/typing-unique/overwriting.ml @@ -176,7 +176,7 @@ let disallowed_by_regionality (local_ unique_ r) x = Line 3, characters 16-17: 3 | let ref = ref r in ^ -Error: This value escapes its region. +Error: This value is "yielding" but expected to be "unyielding". |}] let gc_soundness_no_bug (unique_ r) x = diff --git a/testsuite/tests/typing-unique/unique.ml b/testsuite/tests/typing-unique/unique.ml index 2ae43cc457f..f4ee08f1b43 100644 --- a/testsuite/tests/typing-unique/unique.ml +++ b/testsuite/tests/typing-unique/unique.ml @@ -367,7 +367,7 @@ val ul : local_ 'a @ unique -> local_ 'a = let ul_ret x = exclave_ unique_ x [%%expect{| -val ul_ret : 'a @ unique -> local_ 'a = +val ul_ret : 'a @ unique -> local_ 'a @ unyielding = |}] let rec foo = From 58760bd7d16e088d7939e82891d13e1469d82ece Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 31 Jan 2025 15:07:10 -0500 Subject: [PATCH 03/20] `yielding` tests --- testsuite/tests/typing-modes/yielding.ml | 130 +++++++++++++++++++++-- 1 file changed, 121 insertions(+), 9 deletions(-) diff --git a/testsuite/tests/typing-modes/yielding.ml b/testsuite/tests/typing-modes/yielding.ml index e472f807124..a9a25e54a69 100644 --- a/testsuite/tests/typing-modes/yielding.ml +++ b/testsuite/tests/typing-modes/yielding.ml @@ -18,7 +18,7 @@ let with_effect : ((string -> unit) @ local yielding -> 'a) -> 'a = [%%expect{| val storage : string ref = {contents = ""} -val with_effect : (local_ (string -> unit) @ yielding -> 'a) -> 'a = +val with_effect : (local_ (string -> unit) -> 'a) -> 'a = |}] let () = with_effect (fun k -> k "Hello, world!") @@ -36,7 +36,7 @@ let () = with_effect (fun k -> run_yielding k) let _ = !storage [%%expect{| -val run_yielding : local_ (string -> unit) @ yielding -> unit = +val run_yielding : local_ (string -> unit) -> unit = - : string = "my string" |}] @@ -45,25 +45,19 @@ let run_unyielding : (string -> unit) @ local unyielding -> unit = fun f -> f "a let () = with_effect (fun k -> run_unyielding k) [%%expect{| -val run_unyielding : local_ (string -> unit) -> unit = +val run_unyielding : local_ (string -> unit) @ unyielding -> unit = Line 3, characters 46-47: 3 | let () = with_effect (fun k -> run_unyielding k) ^ Error: This value is "yielding" but expected to be "unyielding". |}] -(* CR dkalinichenko: default [local] arguments to [yielding]. *) - let run_default : (string -> unit) @ local -> unit = fun f -> f "some string" let () = with_effect (fun k -> run_default k) [%%expect{| val run_default : local_ (string -> unit) -> unit = -Line 3, characters 43-44: -3 | let () = with_effect (fun k -> run_default k) - ^ -Error: This value is "yielding" but expected to be "unyielding". |}] (* A closure over a [yielding] value must be [yielding]. *) @@ -78,3 +72,121 @@ Line 2, characters 45-46: ^ Error: The value "k" is yielding, so cannot be used inside a function that may not yield. |}] + + +type 'a t1 = Mk1 of 'a @@ global + +type 'a t2 = Mk2 of 'a @@ global yielding + +type 'a t3 = Mk3 of 'a @@ unyielding + +type 'a t4 = Mk4 of 'a @@ yielding + +let with_global_effect : ((string -> unit) @ yielding -> 'a) -> 'a = + fun f -> f ((:=) storage) + +[%%expect{| +type 'a t1 = Mk1 of global_ 'a +type 'a t2 = Mk2 of global_ 'a @@ yielding +type 'a t3 = Mk3 of 'a @@ unyielding +type 'a t4 = Mk4 of 'a +val with_global_effect : ((string -> unit) @ yielding -> 'a) -> 'a = +|}] + +(* [global] modality implies [unyielding]. *) +let _ = with_global_effect (fun k -> let _ = Mk1 k in ()) + +[%%expect{| +Line 1, characters 49-50: +1 | let _ = with_global_effect (fun k -> let _ = Mk1 k in ()) + ^ +Error: This value is "yielding" but expected to be "unyielding". +|}] + +(* [global yielding] works: *) +let _ = with_global_effect (fun k -> let _ = Mk2 k in ()) + +[%%expect{| +- : unit = () +|}] + +(* [unyielding] and [yielding] modalities: *) +let _ = with_global_effect (fun k -> let _ = Mk3 k in ()) + +[%%expect{| +Line 1, characters 49-50: +1 | let _ = with_global_effect (fun k -> let _ = Mk3 k in ()) + ^ +Error: This value is "yielding" but expected to be "unyielding". +|}] + +let _ = with_global_effect (fun k -> let _ = Mk4 k in ()) + +[%%expect{| +- : unit = () +|}] + +(* [@local_opt] and [yielding]: *) + +external id : ('a[@local_opt]) -> ('a[@local_opt]) = "%identity" + +let f1 x = id x +let f2 (x @ local) = exclave_ id x +let f3 (x @ yielding) = id x +let f4 (x @ local unyielding) = exclave_ id x + +[%%expect{| +external id : ('a [@local_opt]) -> ('a [@local_opt]) = "%identity" +val f1 : 'a -> 'a = +val f2 : local_ 'a -> local_ 'a = +val f3 : 'a @ yielding -> 'a @ yielding = +val f4 : local_ 'a @ unyielding -> local_ 'a @ unyielding = +|}] + +(* [mod global] implies [mod unyielding] by default. *) + +type ('a : value mod global) u1 + +type ('a : value mod global yielding) u2 + +type w1 : value mod global yielding + +type w2 : value mod global unyielding + +[%%expect{| +type ('a : value mod global) u1 +type ('a : value mod global) u2 +type w1 : value mod global +type w2 : value mod global +|}] + +type _z1 = w1 u1 + +[%%expect{| +Line 1, characters 11-13: +1 | type _z1 = w1 u1 + ^^ +Error: This type "w1" should be an instance of type "('a : value mod global)" + The kind of w1 is value mod global + because of the definition of w1 at line 5, characters 0-35. + But the kind of w1 must be a subkind of value mod global + because of the definition of u1 at line 1, characters 0-31. +|}] + +type _z2 = w2 u1 + +[%%expect{| +type _z2 = w2 u1 +|}] + +type _z3 = w1 u2 + +[%%expect{| +type _z3 = w1 u2 +|}] + +type _z4 = w2 u2 + +[%%expect{| +type _z4 = w2 u2 +|}] From f9d86e162bb51615125ad4c7e01968aef0a55a3a Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 31 Jan 2025 15:23:30 -0500 Subject: [PATCH 04/20] format --- .../tests/parsetree/source_jane_street.ml | 27 +++++++++---------- typing/typemode.ml | 11 ++++---- 2 files changed, 19 insertions(+), 19 deletions(-) diff --git a/testsuite/tests/parsetree/source_jane_street.ml b/testsuite/tests/parsetree/source_jane_street.ml index 9a9f897f963..cb9837f3093 100644 --- a/testsuite/tests/parsetree/source_jane_street.ml +++ b/testsuite/tests/parsetree/source_jane_street.ml @@ -493,20 +493,19 @@ let f ~(x1 @ many) [%%expect{| val f : - ('b : value_or_null) ('c : value_or_null) ('d : value_or_null) 'e. - x1:'b -> - x2:local_ string -> local_ - (x3:local_ (string -> string) -> - x4:local_ ('a. 'a -> 'a) -> - x5:local_ 'c -> - x6:local_ bool -> - x7:local_ bool -> - x8:local_ unit -> - string -> - local_ 'd -> local_ - 'b * string * (string -> string) * ('e -> 'e) * 'c * string * string * - int array * string * (int -> local_ (int -> int) @ unyielding) * - (int -> local_ (int -> int) @ unyielding) @ contended) @ unyielding = + x1:'b -> + x2:local_ string -> local_ + (x3:local_ (string -> string) -> + x4:local_ ('a. 'a -> 'a) -> + x5:local_ 'c -> + x6:local_ bool -> + x7:local_ bool -> + x8:local_ unit -> + string -> + local_ 'd -> local_ + 'b * string * (string -> string) * ('e -> 'e) * 'c * string * string * + int array * string * (int -> local_ (int -> int) @ unyielding) * + (int -> local_ (int -> int) @ unyielding) @ contended) @ unyielding = |}, Principal{| val f : diff --git a/typing/typemode.ml b/typing/typemode.ml index 761bcf986d0..e514114777d 100644 --- a/typing/typemode.ml +++ b/typing/typemode.ml @@ -156,14 +156,15 @@ let transl_modifier_annots annots = let modifiers = List.fold_left step empty_modifiers annots in (* Since [yielding] is the default mode in presence of [local], the [global] modifier must also apply [unyielding] unless specified. *) - match Transled_modifiers.get ~axis:(Modal (Comonadic Yielding)) modifiers, - Transled_modifiers.get ~axis:(Modal (Comonadic Areality)) modifiers with + match + ( Transled_modifiers.get ~axis:(Modal (Comonadic Yielding)) modifiers, + Transled_modifiers.get ~axis:(Modal (Comonadic Areality)) modifiers ) + with | None, Some { txt = Locality.Const.Global; _ } -> - Transled_modifiers.set ~axis:(Modal (Comonadic Yielding)) - modifiers (Some { txt = Yielding.Const.Unyielding; loc = Location.none }) + Transled_modifiers.set ~axis:(Modal (Comonadic Yielding)) modifiers + (Some { txt = Yielding.Const.Unyielding; loc = Location.none }) | _, _ -> modifiers - let default_mode_annots (annots : Alloc.Const.Option.t) = (* Unlike all other modes, [yielding] has a different default depending on whether [areality] is [Global] or [Local]. *) From 04375831e3972a927869d27a25a2a0fc4d4727a2 Mon Sep 17 00:00:00 2001 From: Zesen Qian Date: Fri, 14 Feb 2025 11:59:40 +0000 Subject: [PATCH 05/20] dirty fix test change --- testsuite/tests/typing-unique/overwriting.ml | 2 +- typing/typecore.ml | 12 +++++++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/testsuite/tests/typing-unique/overwriting.ml b/testsuite/tests/typing-unique/overwriting.ml index d73e6ae3358..1ad6c335fc4 100644 --- a/testsuite/tests/typing-unique/overwriting.ml +++ b/testsuite/tests/typing-unique/overwriting.ml @@ -176,7 +176,7 @@ let disallowed_by_regionality (local_ unique_ r) x = Line 3, characters 16-17: 3 | let ref = ref r in ^ -Error: This value is "yielding" but expected to be "unyielding". +Error: This value escapes its region. |}] let gc_soundness_no_bug (unique_ r) x = diff --git a/typing/typecore.ml b/typing/typecore.ml index 1478f732c82..5cfc2c5e094 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -6831,13 +6831,19 @@ and type_expect_ mk_expected (newvar (Jkind.Builtin.value ~why:Boxed_record)) in let exp1 = type_expect ~recarg env (mode_default cell_mode) exp1 cell_type in - let exp2 = + let new_fields_mode = (* The newly-written fields have to be global to avoid heap-to-stack pointers. We enforce that here, by asking the allocation to be global. This makes the block alloc_heap, but we ignore that information anyway. *) + (* CR uniqueness: this shouldn't mention yielding *) + { Value.Const.max with + areality = Regionality.Const.Global + ; yielding = Yielding.Const.Unyielding } + in + let exp2 = let exp2_mode = mode_coerce - (Value.max_with (Comonadic Areality) Regionality.global) + (Value.(meet_const new_fields_mode max |> disallow_left)) expected_mode in (* When typing holes, we will enforce: fields_mode <= expected_mode. @@ -6848,7 +6854,7 @@ and type_expect_ And we have also checked above that for regionality cell_mode <= expected_mode. Therefore, we can safely ignore regionality when checking the mode of holes. *) let fields_mode = - Value.meet_with (Comonadic Areality) Regionality.Const.Global cell_mode + Value.meet_const new_fields_mode cell_mode |> Value.disallow_right in let overwrite = From 2695443ff8778b3518c72e994e02aa262832ce60 Mon Sep 17 00:00:00 2001 From: Zesen Qian Date: Fri, 14 Feb 2025 12:00:01 +0000 Subject: [PATCH 06/20] small improvement --- typing/ctype.ml | 18 ++++++++---------- typing/mode.ml | 6 ++++++ typing/mode_intf.mli | 2 ++ 3 files changed, 16 insertions(+), 10 deletions(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index 45e42eae9a1..a554b706dca 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1683,16 +1683,14 @@ let with_locality_and_yielding (locality, yielding) m = let m' = Alloc.newvar () in Locality.equate_exn (Alloc.proj (Comonadic Areality) m') locality; Yielding.equate_exn (Alloc.proj (Comonadic Yielding) m') yielding; - Alloc.submode_exn m' - (Alloc.join_with - (Comonadic Yielding) - Yielding.Const.max - (Alloc.join_with (Comonadic Areality) Locality.Const.max m)); - Alloc.submode_exn - (Alloc.meet_with - (Comonadic Areality) - Locality.Const.min - (Alloc.meet_with (Comonadic Yielding) Yielding.Const.min m)) m'; + Alloc.submode_exn m' (Alloc.join_const + { Alloc.Const.min with + areality = Locality.Const.max; + yielding = Yielding.Const.max} m); + Alloc.submode_exn (Alloc.meet_const + { Alloc.Const.max with + areality = Locality.Const.min; + yielding = Yielding.Const.min} m) m'; m' let curry_mode alloc arg : Alloc.Const.t = diff --git a/typing/mode.ml b/typing/mode.ml index ba04140c2e4..775a31b61f4 100644 --- a/typing/mode.ml +++ b/typing/mode.ml @@ -2424,6 +2424,12 @@ module Value_with (Areality : Areality) = struct let monadic = Monadic.meet_const c.monadic monadic in { monadic; comonadic } + let join_const c { comonadic; monadic } = + let c = split c in + let comonadic = Comonadic.join_const c.comonadic comonadic in + let monadic = Monadic.join_const c.monadic monadic in + { monadic; comonadic } + let imply c { comonadic; monadic } = let c = split c in let comonadic = Comonadic.imply c.comonadic comonadic in diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli index e8885056068..36bf7f19f9d 100644 --- a/typing/mode_intf.mli +++ b/typing/mode_intf.mli @@ -475,6 +475,8 @@ module type S = sig val meet_const : Const.t -> ('l * 'r) t -> ('l * 'r) t + val join_const : Const.t -> ('l * 'r) t -> ('l * 'r) t + val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t val join_const : Const.t -> ('l * 'r) t -> ('l * 'r) t From 95773483fff6ca7f7f106bb8b003783febe40c75 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 28 Feb 2025 14:29:41 -0500 Subject: [PATCH 07/20] merge fix --- otherlibs/stdlib_alpha/capsule.ml | 10 +++++----- typing/mode.ml | 6 ------ typing/mode_intf.mli | 2 -- 3 files changed, 5 insertions(+), 13 deletions(-) diff --git a/otherlibs/stdlib_alpha/capsule.ml b/otherlibs/stdlib_alpha/capsule.ml index ef6e17cf201..58707f5d7d8 100644 --- a/otherlibs/stdlib_alpha/capsule.ml +++ b/otherlibs/stdlib_alpha/capsule.ml @@ -86,7 +86,7 @@ module Password : sig type 'k t : value mod many portable contended (* Can break the soundness of the API. *) - val unsafe_mk : unit -> 'k t @ local @@ portable + val unsafe_mk : unit -> 'k t @ local unyielding @@ portable val id : 'k t @ local -> 'k Id.t @@ portable end @@ -131,7 +131,7 @@ end = struct | already_set_id -> already_set_id) | set_id -> set_id - let unsafe_mk () : _ @@ local = A.make Id.uninitialized + let unsafe_mk () : _ @@ local unyielding = A.make Id.uninitialized end let[@inline] shared t = t @@ -405,13 +405,13 @@ module Key : sig val with_password_shared : 'k t - -> ('k Password.Shared.t @ local -> 'a) @ local + -> ('k Password.Shared.t @ local unyielding -> 'a) @ local -> 'a @@ portable val with_password_shared_local : 'k t - -> ('k Password.Shared.t @ local -> 'a @ local) @ local + -> ('k Password.Shared.t @ local unyielding -> 'a @ local) @ local -> 'a @ local @@ portable @@ -680,7 +680,7 @@ module Rwlock = struct let[@inline] with_read_lock : type k. k t - -> (k Password.Shared.t @ local -> 'a) @ local + -> (k Password.Shared.t @ local unyielding -> 'a) @ local -> 'a @@ portable = fun t f -> diff --git a/typing/mode.ml b/typing/mode.ml index 775a31b61f4..ca7a92c1b6e 100644 --- a/typing/mode.ml +++ b/typing/mode.ml @@ -2436,12 +2436,6 @@ module Value_with (Areality : Areality) = struct let monadic = Monadic.imply c.monadic monadic in { monadic; comonadic } - let join_const c { comonadic; monadic } = - let c = split c in - let comonadic = Comonadic.join_const c.comonadic comonadic in - let monadic = Monadic.join_const c.monadic monadic in - { monadic; comonadic } - let subtract c { comonadic; monadic } = let c = split c in let comonadic = Comonadic.subtract c.comonadic comonadic in diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli index 36bf7f19f9d..f549bec72e7 100644 --- a/typing/mode_intf.mli +++ b/typing/mode_intf.mli @@ -479,8 +479,6 @@ module type S = sig val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t - val join_const : Const.t -> ('l * 'r) t -> ('l * 'r) t - val subtract : Const.t -> ('l * 'r) t -> ('l * disallowed) t (* The following two are about the scenario where we partially apply a From 2e0affa8f34287629f3ea4e9d08d1eda987ac52e Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 28 Feb 2025 18:36:50 -0500 Subject: [PATCH 08/20] fix printing bounds --- typing/jkind.ml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/typing/jkind.ml b/typing/jkind.ml index 219f02e429a..bcfbcbeab78 100644 --- a/typing/jkind.ml +++ b/typing/jkind.ml @@ -1441,6 +1441,24 @@ module Const = struct | acc, `Valid None -> acc | Some acc, `Valid (Some mode) -> Some (mode :: acc)) (Some []) + |> function + | None -> None + | Some modes -> ( + match List.mem "global" modes, List.mem "unyielding" modes with + | true, true -> + (* We default [mod global] to [mod global unyielding], + so we don't want to print the latter. *) + Some (List.filter (fun m -> m <> "unyielding") modes) + | true, false -> + (* Otherwise, print [mod global yielding] to indicate [yielding]. *) + let rec insert_after_global acc = function + | [] -> List.rev acc + | "global" :: rest -> + List.rev_append acc ["global"; "yielding"] @ rest + | x :: rest -> insert_after_global (x :: acc) rest + in + Some (insert_after_global [] modes) + | _, _ -> Some modes) let modality_to_ignore_axes axes_to_ignore = (* The modality is constant along axes to ignore and id along others *) From 1dec1077f8b0e44d63892d7d9deac82a8ad0486c Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 28 Feb 2025 18:39:32 -0500 Subject: [PATCH 09/20] accept tests --- testsuite/tests/lib-array/test_iarray.ml | 14 ++++++++ testsuite/tests/typing-jkind-bounds/basics.ml | 35 ++++++++----------- .../tests/typing-jkind-bounds/composite.ml | 4 +-- testsuite/tests/typing-jkind-bounds/predef.ml | 6 ++-- .../tests/typing-jkind-bounds/printing.ml | 14 ++++---- .../tests/typing-jkind-bounds/records.ml | 4 +-- .../typing-jkind-bounds/subsumption/basics.ml | 8 ++--- .../subsumption/constraint.ml | 2 +- .../subsumption/functors.ml | 4 +-- .../subsumption/modalities.ml | 3 +- .../tests/typing-jkind-bounds/variants.ml | 4 +-- .../typing-layouts-products/basics_alpha.ml | 18 ++++------ testsuite/tests/typing-layouts/allow_any.ml | 2 +- testsuite/tests/typing-local/exclave.ml | 5 ++- testsuite/tests/typing-local/local.ml | 22 +++++++----- testsuite/tests/typing-modal-kinds/basics.ml | 2 +- testsuite/tests/typing-modes/modes.ml | 16 +++++++++ testsuite/tests/typing-modes/yielding.ml | 6 ++-- testsuite/tests/typing-unique/unique.ml | 2 ++ 19 files changed, 99 insertions(+), 72 deletions(-) diff --git a/testsuite/tests/lib-array/test_iarray.ml b/testsuite/tests/lib-array/test_iarray.ml index 35daae39718..55d931f03c4 100644 --- a/testsuite/tests/lib-array/test_iarray.ml +++ b/testsuite/tests/lib-array/test_iarray.ml @@ -32,6 +32,20 @@ let rec list_map_local_input (local_ f) (local_ list) = module Iarray = Stdlib_stable.Iarray external ( .:() ) : 'a iarray -> int -> 'a = "%array_safe_get" val iarray : int iarray = [:1; 2; 3; 4; 5:] +val iarray_local : unit -> local_ int iarray @ unyielding = +val ifarray : float iarray = [:1.5; 2.5; 3.5; 4.5; 5.5:] +val ifarray_local : unit -> local_ float iarray @ unyielding = +val marray : int array = [|1; 2; 3; 4; 5|] +val mfarray : float array = [|1.5; 2.5; 3.5; 4.5; 5.5|] +external globalize_float : local_ float -> float = "%obj_dup" +external globalize_string : local_ string -> string = "%obj_dup" +val globalize_int_iarray : local_ int iarray -> int iarray = +val list_map_local_input : + local_ (local_ 'a -> 'b) -> local_ 'a list -> 'b list = +|}, Principal{| +module Iarray = Stdlib_stable.Iarray +external ( .:() ) : 'a iarray -> int -> 'a = "%array_safe_get" +val iarray : int iarray = [:1; 2; 3; 4; 5:] val iarray_local : unit -> local_ int iarray = val ifarray : float iarray = [:1.5; 2.5; 3.5; 4.5; 5.5:] val ifarray_local : unit -> local_ float iarray = diff --git a/testsuite/tests/typing-jkind-bounds/basics.ml b/testsuite/tests/typing-jkind-bounds/basics.ml index bfbe352a3d8..b011541f76e 100644 --- a/testsuite/tests/typing-jkind-bounds/basics.ml +++ b/testsuite/tests/typing-jkind-bounds/basics.ml @@ -990,7 +990,7 @@ type ('a : immediate) t : value mod global = { mutable x : 'a } Line 1, characters 0-63: 1 | type ('a : immediate) t : value mod global = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ many unyielding +Error: The kind of type "t" is mutable_data with 'a @@ unyielding many because it's a boxed record type. But the kind of type "t" must be a subkind of value mod global because of the annotation on the declaration of the type t. @@ -1004,7 +1004,7 @@ type ('a : immediate) t : value mod aliased = { mutable x : 'a } Line 1, characters 0-64: 1 | type ('a : immediate) t : value mod aliased = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ many unyielding +Error: The kind of type "t" is mutable_data with 'a @@ unyielding many because it's a boxed record type. But the kind of type "t" must be a subkind of value mod aliased because of the annotation on the declaration of the type t. @@ -1018,7 +1018,7 @@ type ('a : immediate) t : value mod contended = { mutable x : 'a } Line 1, characters 0-66: 1 | type ('a : immediate) t : value mod contended = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ many unyielding +Error: The kind of type "t" is mutable_data with 'a @@ unyielding many because it's a boxed record type. But the kind of type "t" must be a subkind of value mod contended because of the annotation on the declaration of the type t. @@ -1032,7 +1032,7 @@ type ('a : immediate) t : value mod external_ = { mutable x : 'a } Line 1, characters 0-66: 1 | type ('a : immediate) t : value mod external_ = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ many unyielding +Error: The kind of type "t" is mutable_data with 'a @@ unyielding many because it's a boxed record type. But the kind of type "t" must be a subkind of value mod external_ because of the annotation on the declaration of the type t. @@ -1046,7 +1046,7 @@ type ('a : immediate) t : value mod external64 = { mutable x : 'a } Line 1, characters 0-67: 1 | type ('a : immediate) t : value mod external64 = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ many unyielding +Error: The kind of type "t" is mutable_data with 'a @@ unyielding many because it's a boxed record type. But the kind of type "t" must be a subkind of value mod external64 because of the annotation on the declaration of the type t. @@ -1157,15 +1157,7 @@ Error: The kind of type "t" is value type 'a t : value mod global portable contended many aliased unyielding = { x : 'a @@ global portable contended many aliased } [@@unboxed] [%%expect {| -Lines 1-2, characters 0-66: -1 | type 'a t : value mod global portable contended many aliased unyielding = -2 | { x : 'a @@ global portable contended many aliased } [@@unboxed] -Error: The kind of type "t" is value mod global aliased many contended portable - because it instantiates an unannotated type parameter of t, - chosen to have kind value mod global aliased many contended portable. - But the kind of type "t" must be a subkind of - immutable_data mod global aliased - because of the annotation on the declaration of the type t. +type 'a t = { global_ x : 'a @@ many portable aliased contended; } [@@unboxed] |}] (* CR layouts v2.8: this could be accepted, if we infer ('a : value mod unyielding). We do not currently do this, because we finish inference of the @@ -1191,7 +1183,7 @@ Error: The kind of type "t" is value because it instantiates an unannotated type parameter of t, chosen to have kind value. But the kind of type "t" must be a subkind of - immutable_data mod global aliased + immutable_data mod global yielding aliased because of the annotation on the declaration of the type t. |}] (* CR layouts v2.8: this should be accepted *) @@ -1264,10 +1256,13 @@ type 'a t : value mod global = { x : 'a @@ global } Line 1, characters 0-51: 1 | type 'a t : value mod global = { x : 'a @@ global } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is immutable_data with 'a +Error: The kind of type "t" is immutable_data with 'a @@ unyielding because it's a boxed record type. But the kind of type "t" must be a subkind of value mod global because of the annotation on the declaration of the type t. + + The first mode-crosses less than the second along: + locality: mod local ≰ mod global |}] (*****************************) @@ -1443,7 +1438,7 @@ Line 1, characters 41-51: ^^^^^^^^^^ Error: This expression has type "< >" but an expression was expected of type "('a : value mod aliased)" - The kind of < > is value mod global many unyielding + The kind of < > is value mod global many because it's the type of an object. But the kind of < > must be a subkind of value mod aliased because of the annotation on the wildcard _ at line 1, characters 19-36. @@ -1456,7 +1451,7 @@ Line 1, characters 42-52: ^^^^^^^^^^ Error: This expression has type "< >" but an expression was expected of type "('a : value mod portable)" - The kind of < > is value mod global many unyielding + The kind of < > is value mod global many because it's the type of an object. But the kind of < > must be a subkind of value mod portable because of the annotation on the wildcard _ at line 1, characters 19-37. @@ -1469,7 +1464,7 @@ Line 1, characters 43-53: ^^^^^^^^^^ Error: This expression has type "< >" but an expression was expected of type "('a : value mod contended)" - The kind of < > is value mod global many unyielding + The kind of < > is value mod global many because it's the type of an object. But the kind of < > must be a subkind of value mod contended because of the annotation on the wildcard _ at line 1, characters 19-38. @@ -1482,7 +1477,7 @@ Line 1, characters 43-53: ^^^^^^^^^^ Error: This expression has type "< >" but an expression was expected of type "('a : value mod external_)" - The kind of < > is value mod global many unyielding + The kind of < > is value mod global many because it's the type of an object. But the kind of < > must be a subkind of value mod external_ because of the annotation on the wildcard _ at line 1, characters 19-38. diff --git a/testsuite/tests/typing-jkind-bounds/composite.ml b/testsuite/tests/typing-jkind-bounds/composite.ml index 0a187aad2c8..7f425c1229f 100644 --- a/testsuite/tests/typing-jkind-bounds/composite.ml +++ b/testsuite/tests/typing-jkind-bounds/composite.ml @@ -189,7 +189,7 @@ Line 1, characters 13-20: 1 | let foo (t : int ref t @@ contended) = use_uncontended t ^^^^^^^ Error: This type "int ref" should be an instance of type "('a : immutable_data)" - The kind of int ref is mutable_data with int @@ many unyielding. + The kind of int ref is mutable_data with int @@ unyielding many. But the kind of int ref must be a subkind of immutable_data because of the definition of t at line 1, characters 0-46. @@ -339,7 +339,7 @@ Line 1, characters 13-20: 1 | let foo (t : int ref t @@ contended) = use_uncontended t ^^^^^^^ Error: This type "int ref" should be an instance of type "('a : immutable_data)" - The kind of int ref is mutable_data with int @@ many unyielding. + The kind of int ref is mutable_data with int @@ unyielding many. But the kind of int ref must be a subkind of immutable_data because of the definition of t at line 1, characters 0-73. diff --git a/testsuite/tests/typing-jkind-bounds/predef.ml b/testsuite/tests/typing-jkind-bounds/predef.ml index af9f1121145..fc250e0f2f7 100644 --- a/testsuite/tests/typing-jkind-bounds/predef.ml +++ b/testsuite/tests/typing-jkind-bounds/predef.ml @@ -176,7 +176,7 @@ type 'a t : mutable_data = 'a ref Line 1, characters 0-33: 1 | type 'a t : mutable_data = 'a ref ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "'a ref" is mutable_data with 'a @@ many unyielding. +Error: The kind of type "'a ref" is mutable_data with 'a @@ unyielding many. But the kind of type "'a ref" must be a subkind of mutable_data because of the definition of t at line 1, characters 0-33. @@ -198,7 +198,7 @@ Line 1, characters 14-21: ^^^^^^^ Error: This type "int ref" should be an instance of type "('a : value mod portable)" - The kind of int ref is mutable_data with int @@ many unyielding. + The kind of int ref is mutable_data with int @@ unyielding many. But the kind of int ref must be a subkind of value mod portable because of the definition of require_portable at line 10, characters 0-47. @@ -222,7 +222,7 @@ Line 1, characters 14-21: ^^^^^^^ Error: This type "int ref" should be an instance of type "('a : value mod contended)" - The kind of int ref is mutable_data with int @@ many unyielding. + The kind of int ref is mutable_data with int @@ unyielding many. But the kind of int ref must be a subkind of value mod contended because of the definition of require_contended at line 9, characters 0-49. diff --git a/testsuite/tests/typing-jkind-bounds/printing.ml b/testsuite/tests/typing-jkind-bounds/printing.ml index cf80f3d8c6e..676fc8d93a8 100644 --- a/testsuite/tests/typing-jkind-bounds/printing.ml +++ b/testsuite/tests/typing-jkind-bounds/printing.ml @@ -175,7 +175,7 @@ Line 3, characters 11-12: ^ Error: This type "a" = "int ref" should be an instance of type "('a : immutable_data)" - The kind of a is mutable_data with int @@ many unyielding. + The kind of a is mutable_data with int @@ unyielding many. But the kind of a must be a subkind of immutable_data because of the definition of t at line 2, characters 0-28. @@ -335,15 +335,15 @@ Error: Signature mismatch: Modules do not match: sig type 'a t : mutable_data with 'a end is not included in - sig type 'a t : mutable_data with 'a @@ many unyielding end + sig type 'a t : mutable_data with 'a @@ unyielding many end Type declarations do not match: type 'a t : mutable_data with 'a is not included in - type 'a t : mutable_data with 'a @@ many unyielding + type 'a t : mutable_data with 'a @@ unyielding many The kind of the first is mutable_data with 'a because of the definition of t at line 4, characters 2-34. But the kind of the first must be a subkind of mutable_data - with 'a @@ many unyielding + with 'a @@ unyielding many because of the definition of t at line 2, characters 2-40. The first mode-crosses less than the second along: @@ -415,14 +415,14 @@ Lines 3-5, characters 6-3: 5 | end Error: Signature mismatch: Modules do not match: - sig type 'a t : mutable_data with 'a @@ many unyielding end + sig type 'a t : mutable_data with 'a @@ unyielding many end is not included in sig type 'a t : immutable_data with 'a end Type declarations do not match: - type 'a t : mutable_data with 'a @@ many unyielding + type 'a t : mutable_data with 'a @@ unyielding many is not included in type 'a t : immutable_data with 'a - The kind of the first is mutable_data with 'a @@ many unyielding + The kind of the first is mutable_data with 'a @@ unyielding many because of the definition of t at line 4, characters 2-40. But the kind of the first must be a subkind of immutable_data with 'a because of the definition of t at line 2, characters 2-56. diff --git a/testsuite/tests/typing-jkind-bounds/records.ml b/testsuite/tests/typing-jkind-bounds/records.ml index 2de8a1175ad..57fce9a7efb 100644 --- a/testsuite/tests/typing-jkind-bounds/records.ml +++ b/testsuite/tests/typing-jkind-bounds/records.ml @@ -128,7 +128,7 @@ type 'a t : immutable_data = { mutable x : 'a } Line 1, characters 0-47: 1 | type 'a t : immutable_data = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ many unyielding +Error: The kind of type "t" is mutable_data with 'a @@ unyielding many because it's a boxed record type. But the kind of type "t" must be a subkind of immutable_data because of the annotation on the declaration of the type t. @@ -268,7 +268,7 @@ type 'a t : immutable_data with 'a = { mutable x : 'a } Line 1, characters 0-55: 1 | type 'a t : immutable_data with 'a = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ many unyielding +Error: The kind of type "t" is mutable_data with 'a @@ unyielding many because it's a boxed record type. But the kind of type "t" must be a subkind of immutable_data with 'a because of the annotation on the declaration of the type t. diff --git a/testsuite/tests/typing-jkind-bounds/subsumption/basics.ml b/testsuite/tests/typing-jkind-bounds/subsumption/basics.ml index 75b8bbdcd91..0571e281735 100644 --- a/testsuite/tests/typing-jkind-bounds/subsumption/basics.ml +++ b/testsuite/tests/typing-jkind-bounds/subsumption/basics.ml @@ -176,15 +176,15 @@ Error: Signature mismatch: Modules do not match: sig type 'a t : mutable_data with 'a end is not included in - sig type 'a t : mutable_data with 'a @@ many unyielding end + sig type 'a t : mutable_data with 'a @@ unyielding many end Type declarations do not match: type 'a t : mutable_data with 'a is not included in - type 'a t : mutable_data with 'a @@ many unyielding + type 'a t : mutable_data with 'a @@ unyielding many The kind of the first is mutable_data with 'a because of the definition of t at line 4, characters 2-34. But the kind of the first must be a subkind of mutable_data - with 'a @@ many unyielding + with 'a @@ unyielding many because of the definition of t at line 2, characters 2-40. The first mode-crosses less than the second along: @@ -198,7 +198,7 @@ end = struct type 'a t : mutable_data with 'a @@ many unyielding end [%%expect {| -module M : sig type 'a t : mutable_data with 'a @@ many unyielding end +module M : sig type 'a t : mutable_data with 'a @@ unyielding many end |}] (* CR layouts v2.8: 'a u's kind should get normalized to just immutable_data *) diff --git a/testsuite/tests/typing-jkind-bounds/subsumption/constraint.ml b/testsuite/tests/typing-jkind-bounds/subsumption/constraint.ml index ff578233184..9e9b1e06f4d 100644 --- a/testsuite/tests/typing-jkind-bounds/subsumption/constraint.ml +++ b/testsuite/tests/typing-jkind-bounds/subsumption/constraint.ml @@ -141,7 +141,7 @@ Error: Signature mismatch: type 'a t = Foo of 'a constraint 'a = 'b ref is not included in type 'a t : immutable_data with 'b constraint 'a = 'b ref - The kind of the first is mutable_data with 'b @@ many unyielding + The kind of the first is mutable_data with 'b @@ unyielding many because of the definition of t at line 4, characters 2-46. But the kind of the first must be a subkind of immutable_data with 'b because of the definition of t at line 2, characters 2-59. diff --git a/testsuite/tests/typing-jkind-bounds/subsumption/functors.ml b/testsuite/tests/typing-jkind-bounds/subsumption/functors.ml index a4f07323ad9..3ee184249c5 100644 --- a/testsuite/tests/typing-jkind-bounds/subsumption/functors.ml +++ b/testsuite/tests/typing-jkind-bounds/subsumption/functors.ml @@ -59,7 +59,7 @@ Line 4, characters 0-48: 4 | type 'a t : immutable_data with 'a = 'a F(Ref).t ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The kind of type "'a F(Ref).t" is mutable_data - with 'a @@ many unyielding + with 'a @@ unyielding many because of the definition of t at line 2, characters 2-40. But the kind of type "'a F(Ref).t" must be a subkind of immutable_data with 'a @@ -79,7 +79,7 @@ Line 4, characters 0-38: 4 | type 'a t : mutable_data = 'a F(Ref).t ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The kind of type "'a F(Ref).t" is mutable_data - with 'a @@ many unyielding + with 'a @@ unyielding many because of the definition of t at line 2, characters 2-40. But the kind of type "'a F(Ref).t" must be a subkind of mutable_data because of the definition of t at line 4, characters 0-38. diff --git a/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml b/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml index ee08dc78feb..85b20082731 100644 --- a/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml +++ b/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml @@ -124,8 +124,7 @@ end = struct type 'a t : immediate with 'a @@ aliased many contended global portable end [%%expect {| -module M : - sig type 'a t : value mod global aliased many contended portable end +module M : sig type 'a t : immutable_data mod global yielding aliased end |}] module M : sig diff --git a/testsuite/tests/typing-jkind-bounds/variants.ml b/testsuite/tests/typing-jkind-bounds/variants.ml index 1dd06dc4f4f..5c7d4531aaa 100644 --- a/testsuite/tests/typing-jkind-bounds/variants.ml +++ b/testsuite/tests/typing-jkind-bounds/variants.ml @@ -132,7 +132,7 @@ type 'a t : immutable_data = Foo of { mutable x : 'a } Line 1, characters 0-54: 1 | type 'a t : immutable_data = Foo of { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ many unyielding +Error: The kind of type "t" is mutable_data with 'a @@ unyielding many because it's a boxed variant type. But the kind of type "t" must be a subkind of immutable_data because of the annotation on the declaration of the type t. @@ -272,7 +272,7 @@ type 'a t : immutable_data with 'a = Foo of { mutable x : 'a } Line 1, characters 0-62: 1 | type 'a t : immutable_data with 'a = Foo of { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ many unyielding +Error: The kind of type "t" is mutable_data with 'a @@ unyielding many because it's a boxed variant type. But the kind of type "t" must be a subkind of immutable_data with 'a because of the annotation on the declaration of the type t. diff --git a/testsuite/tests/typing-layouts-products/basics_alpha.ml b/testsuite/tests/typing-layouts-products/basics_alpha.ml index ecab40ae64e..4c0e1a68484 100644 --- a/testsuite/tests/typing-layouts-products/basics_alpha.ml +++ b/testsuite/tests/typing-layouts-products/basics_alpha.ml @@ -67,11 +67,9 @@ Line 3, characters 0-39: 3 | type t3 : any mod non_null = #(t1 * t2);; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The kind of type "#(t1 * t2)" is - any_non_null mod global aliased many contended portable unyielding - external_ + any_non_null mod global aliased many contended portable external_ with t1 with t2 - & any_non_null mod global aliased many contended portable unyielding - external_ + & any_non_null mod global aliased many contended portable external_ with t1 with t2 because it is an unboxed tuple. But the kind of type "#(t1 * t2)" must be a subkind of any_non_null @@ -88,11 +86,9 @@ Line 3, characters 0-45: 3 | type t3 : any & any mod non_null = #(t1 * t2);; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The kind of type "#(t1 * t2)" is - any_non_null mod global aliased many contended portable unyielding - external_ + any_non_null mod global aliased many contended portable external_ with t1 with t2 - & any_non_null mod global aliased many contended portable unyielding - external_ + & any_non_null mod global aliased many contended portable external_ with t1 with t2 because it is an unboxed tuple. But the kind of type "#(t1 * t2)" must be a subkind of @@ -110,11 +106,9 @@ Line 3, characters 0-62: 3 | type t3 : (any mod non_null) & (any mod non_null) = #(t1 * t2);; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The kind of type "#(t1 * t2)" is - any_non_null mod global aliased many contended portable unyielding - external_ + any_non_null mod global aliased many contended portable external_ with t1 with t2 - & any_non_null mod global aliased many contended portable unyielding - external_ + & any_non_null mod global aliased many contended portable external_ with t1 with t2 because it is an unboxed tuple. But the kind of type "#(t1 * t2)" must be a subkind of diff --git a/testsuite/tests/typing-layouts/allow_any.ml b/testsuite/tests/typing-layouts/allow_any.ml index 62c31a943f3..a652f616ab3 100644 --- a/testsuite/tests/typing-layouts/allow_any.ml +++ b/testsuite/tests/typing-layouts/allow_any.ml @@ -313,7 +313,7 @@ module B = struct let a t = t.a end [%%expect{| -module A : sig type t : mutable_data mod global external_ end +module A : sig type t : mutable_data mod global yielding external_ end module B : sig type t : value mod contended portable = { a : A.t; } diff --git a/testsuite/tests/typing-local/exclave.ml b/testsuite/tests/typing-local/exclave.ml index 6f41c8d3246..443eba967d6 100644 --- a/testsuite/tests/typing-local/exclave.ml +++ b/testsuite/tests/typing-local/exclave.ml @@ -19,7 +19,7 @@ let foo () = let local_ y = Some 42 in y [%%expect{| -val foo : unit -> local_ int option = +val foo : unit -> local_ int option @ unyielding = |}] (* sidenote: in the above, y escapes the function even though local_ @@ -140,6 +140,9 @@ let foo (local_ x) = [%%expect{| type t = { x : int option; } +val foo : local_ int option -> local_ int option @ unyielding = +|}, Principal{| +type t = { x : int option; } val foo : local_ int option -> local_ int option = |}] diff --git a/testsuite/tests/typing-local/local.ml b/testsuite/tests/typing-local/local.ml index cb0366fa27d..d08e292e064 100644 --- a/testsuite/tests/typing-local/local.ml +++ b/testsuite/tests/typing-local/local.ml @@ -378,7 +378,9 @@ val foo : ?x:local_ 'a -> unit -> local_ 'a option = let foo ?(local_ x = "hello") () = x;; [%%expect{| -val foo : ?x:local_ string -> unit -> local_ string @ unyielding = +val foo : + ?x:local_ string -> local_ + (unit -> local_ string @ unyielding) @ unyielding = |}, Principal{| val foo : ?x:local_ string -> unit -> local_ string = |}] @@ -966,7 +968,7 @@ let foo x = exclave_ let r = local_ { contents = x } in r [%%expect{| -val foo : 'a -> local_ 'a ref = +val foo : 'a -> local_ 'a ref @ unyielding = |}] let foo p x = exclave_ @@ -974,7 +976,7 @@ let foo p x = exclave_ if p then r else r [%%expect{| -val foo : bool -> 'a -> local_ 'a ref = +val foo : bool -> 'a -> local_ 'a ref @ unyielding = |}] (* Non-local regional values can be passed to tail calls *) @@ -1899,7 +1901,7 @@ let testbool1 f = let local_ r = ref 42 in (f r || false) && true let testbool2 f = let local_ r = ref 42 in true && (false || f r) [%%expect{| -val testbool1 : (local_ int ref -> bool) -> bool = +val testbool1 : (local_ int ref @ unyielding -> bool) -> bool = Line 3, characters 63-64: 3 | let testbool2 f = let local_ r = ref 42 in true && (false || f r) ^ @@ -1986,14 +1988,15 @@ let f g n = () let z : (int list -> unit) -> int -> unit = f [%%expect{| -val f : (local_ int list -> unit) -> int -> unit = +val f : (local_ int list @ unyielding -> unit) -> int -> unit = Line 5, characters 44-45: 5 | let z : (int list -> unit) -> int -> unit = f ^ -Error: This expression has type "(local_ int list -> unit) -> int -> unit" +Error: This expression has type + "(local_ int list @ unyielding -> unit) -> int -> unit" but an expression was expected of type "(int list -> unit) -> int -> unit" - Type "local_ int list -> unit" is not compatible with type + Type "local_ int list @ unyielding -> unit" is not compatible with type "int list -> unit" |}] @@ -2008,10 +2011,11 @@ end Line 6, characters 46-47: 6 | let z : (int list -> unit) -> int -> unit = f ^ -Error: This expression has type "(local_ int list -> unit) -> int -> unit" +Error: This expression has type + "(local_ int list @ unyielding -> unit) -> int -> unit" but an expression was expected of type "(int list -> unit) -> int -> unit" - Type "local_ int list -> unit" is not compatible with type + Type "local_ int list @ unyielding -> unit" is not compatible with type "int list -> unit" |}] diff --git a/testsuite/tests/typing-modal-kinds/basics.ml b/testsuite/tests/typing-modal-kinds/basics.ml index 7afe5dc325d..2dcc40c97eb 100644 --- a/testsuite/tests/typing-modal-kinds/basics.ml +++ b/testsuite/tests/typing-modal-kinds/basics.ml @@ -940,7 +940,7 @@ Line 1, characters 10-19: ^^^^^^^^^ Error: This type "int t ref" should be an instance of type "('a : value mod contended)" - The kind of int t ref is mutable_data with int t @@ many unyielding. + The kind of int t ref is mutable_data with int t @@ unyielding many. But the kind of int t ref must be a subkind of value mod contended because of the definition of require_contended at line 1, characters 0-49. diff --git a/testsuite/tests/typing-modes/modes.ml b/testsuite/tests/typing-modes/modes.ml index 199e843825a..e7ec1c53a5f 100644 --- a/testsuite/tests/typing-modes/modes.ml +++ b/testsuite/tests/typing-modes/modes.ml @@ -394,11 +394,19 @@ type r = { mutable x : string; } let foo ?(local_ x @ unique once = 42) () = () [%%expect{| +val foo : + ?x:local_ int @ once unique -> local_ (unit -> unit) @ once unyielding = + +|}, Principal{| val foo : ?x:local_ int @ once unique -> unit -> unit = |}] let foo ?(local_ x : _ @@ unique once = 42) () = () [%%expect{| +val foo : + ?x:local_ int @ once unique -> local_ (unit -> unit) @ once unyielding = + +|}, Principal{| val foo : ?x:local_ int @ once unique -> unit -> unit = |}] @@ -412,11 +420,19 @@ Error: Optional parameters cannot be polymorphic let foo ?x:(local_ (x,y) @ unique once = (42, 42)) () = () [%%expect{| +val foo : + ?x:local_ int * int @ once unique -> local_ (unit -> unit) @ once + unyielding = +|}, Principal{| val foo : ?x:local_ int * int @ once unique -> unit -> unit = |}] let foo ?x:(local_ (x,y) : _ @@ unique once = (42, 42)) () = () [%%expect{| +val foo : + ?x:local_ int * int @ once unique -> local_ (unit -> unit) @ once + unyielding = +|}, Principal{| val foo : ?x:local_ int * int @ once unique -> unit -> unit = |}] diff --git a/testsuite/tests/typing-modes/yielding.ml b/testsuite/tests/typing-modes/yielding.ml index a9a25e54a69..56f2053ebf5 100644 --- a/testsuite/tests/typing-modes/yielding.ml +++ b/testsuite/tests/typing-modes/yielding.ml @@ -155,8 +155,8 @@ type w2 : value mod global unyielding [%%expect{| type ('a : value mod global) u1 -type ('a : value mod global) u2 -type w1 : value mod global +type ('a : value mod global yielding) u2 +type w1 : value mod global yielding type w2 : value mod global |}] @@ -167,7 +167,7 @@ Line 1, characters 11-13: 1 | type _z1 = w1 u1 ^^ Error: This type "w1" should be an instance of type "('a : value mod global)" - The kind of w1 is value mod global + The kind of w1 is value mod global yielding because of the definition of w1 at line 5, characters 0-35. But the kind of w1 must be a subkind of value mod global because of the definition of u1 at line 1, characters 0-31. diff --git a/testsuite/tests/typing-unique/unique.ml b/testsuite/tests/typing-unique/unique.ml index f4ee08f1b43..6d3f2da81ae 100644 --- a/testsuite/tests/typing-unique/unique.ml +++ b/testsuite/tests/typing-unique/unique.ml @@ -385,6 +385,8 @@ let rec bar = | Some () -> () | None -> bar (local_ Some ()) [@nontail] [%%expect{| +val bar : local_ unit option @ unique unyielding -> unit = +|}, Principal{| val bar : local_ unit option @ unique -> unit = |}] From 2f09d676d9600176f2ef38ed10cc1da45772bc50 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 28 Feb 2025 18:46:25 -0500 Subject: [PATCH 10/20] fix the issue with `instance_prim` --- typing/ctype.ml | 8 ++++---- typing/ctype.mli | 3 ++- typing/includecore.ml | 44 +++++++++++++++++++++---------------------- typing/typecore.ml | 2 +- 4 files changed, 29 insertions(+), 28 deletions(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index a554b706dca..ea89baad3c5 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1816,14 +1816,14 @@ let instance_prim_mode (desc : Primitive.description) ty = let finalret = prim_mode (Some mode_l) (Some mode_y) desc.prim_native_repr_res in instance_prim_locals desc.prim_native_repr_args mode_l mode_y (Alloc.disallow_right Alloc.legacy) finalret ty, - Some mode_l + Some mode_l, Some mode_y else - ty, None + ty, None, None let instance_prim (desc : Primitive.description) ty = let ty, sort = instance_prim_layout desc ty in - let ty, mode = instance_prim_mode desc ty in - ty, mode, sort + let ty, mode_l, mode_y = instance_prim_mode desc ty in + ty, mode_l, mode_y, sort (**** Instantiation with parameter substitution ****) diff --git a/typing/ctype.mli b/typing/ctype.mli index a8daf25658c..3fb5311e572 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -229,7 +229,8 @@ val prim_mode : * (Mode.allowed * 'r) Mode.Yielding.t val instance_prim: Primitive.description -> type_expr -> - type_expr * Mode.Locality.lr option * Jkind.Sort.t option + type_expr * Mode.Locality.lr option + * Mode.Yielding.lr option * Jkind.Sort.t option (** Given (a @ m1 -> b -> c) @ m0, where [m0] and [m1] are modes expressed by user-syntax, [curry_mode m0 m1] gives the mode we implicitly interpret b->c diff --git a/typing/includecore.ml b/typing/includecore.ml index 58dee660b85..71b7265b846 100644 --- a/typing/includecore.ml +++ b/typing/includecore.ml @@ -146,37 +146,37 @@ let value_descriptions ~loc env name | Val_prim p1 -> begin match vd2.val_kind with | Val_prim p2 -> begin - let ty1_global, _, _ = Ctype.instance_prim p1 vd1.val_type in - let ty2_global = - let ty2, mode2, _ = Ctype.instance_prim p2 vd2.val_type in - Option.iter - (fun m -> Mode.Locality.submode_exn m Mode.Locality.global) - mode2; - ty2 - in - (try Ctype.moregeneral env true ty1_global ty2_global - with Ctype.Moregen err -> raise (Dont_match (Type err))); - let ty1_local, _, _ = Ctype.instance_prim p1 vd1.val_type in - let ty2_local = - let ty2, mode2, _ = Ctype.instance_prim p2 vd2.val_type in - Option.iter - (fun m -> Mode.Locality.submode_exn Mode.Locality.local m) - mode2; - ty2 - in - (try Ctype.moregeneral env true ty1_local ty2_local - with Ctype.Moregen err -> raise (Dont_match (Type err))); + let restrict_locality = [ + (fun m -> Mode.Locality.submode_exn m Mode.Locality.global); + (fun m -> Mode.Locality.submode_exn Mode.Locality.local m) + ] in + let restrict_yielding = [ + (fun m -> Mode.Yielding.submode_exn m Mode.Yielding.unyielding); + (fun m -> Mode.Yielding.submode_exn Mode.Yielding.yielding m) + ] in + List.iter (fun restrict_loc -> + List.iter (fun restrict_yield -> + let ty1, _, _, _ = Ctype.instance_prim p1 vd1.val_type in + let ty2, mode_l2, mode_y2, _ = Ctype.instance_prim p2 vd2.val_type in + Option.iter restrict_loc mode_l2; + Option.iter restrict_yield mode_y2; + try + Ctype.moregeneral env true ty1 ty2 + with Ctype.Moregen err -> + raise (Dont_match (Type err)) + ) restrict_yielding + ) restrict_locality; match primitive_descriptions p1 p2 with | None -> Tcoerce_none | Some err -> raise (Dont_match (Primitive_mismatch err)) end | _ -> - let ty1, mode1, sort1 = Ctype.instance_prim p1 vd1.val_type in + let ty1, mode_l1, _, sort1 = Ctype.instance_prim p1 vd1.val_type in (try Ctype.moregeneral env true ty1 vd2.val_type with Ctype.Moregen err -> raise (Dont_match (Type err))); let pc = {pc_desc = p1; pc_type = vd2.Types.val_type; - pc_poly_mode = Option.map Mode.Locality.disallow_right mode1; + pc_poly_mode = Option.map Mode.Locality.disallow_right mode_l1; pc_poly_sort=sort1; pc_env = env; pc_loc = vd1.Types.val_loc; } in Tcoerce_primitive pc diff --git a/typing/typecore.ml b/typing/typecore.ml index 5cfc2c5e094..9a92ede7bc5 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -7083,7 +7083,7 @@ and type_ident env ?(recarg=Rejected) lid = let val_type, kind = match desc.val_kind with | Val_prim prim -> - let ty, mode, sort = instance_prim prim desc.val_type in + let ty, mode, _, sort = instance_prim prim desc.val_type in let ty = instance ty in begin match prim.prim_native_repr_res, mode with (* if the locality of returned value of the primitive is poly From c454e35496eec53ba7002c26911cfc9c4a3ca090 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Thu, 27 Mar 2025 11:59:01 -0400 Subject: [PATCH 11/20] Only vary `yielding` with `[@local_opt]` --- testsuite/tests/typing-modes/yielding.ml | 44 ++++++++++++++++++++++++ typing/ctype.ml | 8 ++--- 2 files changed, 47 insertions(+), 5 deletions(-) diff --git a/testsuite/tests/typing-modes/yielding.ml b/testsuite/tests/typing-modes/yielding.ml index 56f2053ebf5..1e1a1f60584 100644 --- a/testsuite/tests/typing-modes/yielding.ml +++ b/testsuite/tests/typing-modes/yielding.ml @@ -126,6 +126,50 @@ let _ = with_global_effect (fun k -> let _ = Mk4 k in ()) - : unit = () |}] +(* Externals and [yielding]: *) + +external ok_yielding : 'a @ local -> unit = "%ignore" + +let _ = ok_yielding 4 + +let _ = ok_yielding (stack_ (Some "local string")) + +let _ = with_global_effect (fun k -> ok_yielding k) + +[%%expect{| +external ok_yielding : local_ 'a -> unit = "%ignore" +- : unit = () +- : unit = () +- : unit = () +|}] + +external requires_unyielding : 'a @ local unyielding -> unit = "%ignore" + +let _ = requires_unyielding 4 + +let _ = requires_unyielding (stack_ (Some "local string")) + +let _ = with_global_effect (fun k -> requires_unyielding k) + +[%%expect{| +external requires_unyielding : local_ 'a @ unyielding -> unit = "%ignore" +- : unit = () +- : unit = () +Line 7, characters 57-58: +7 | let _ = with_global_effect (fun k -> requires_unyielding k) + ^ +Error: This value is "yielding" but expected to be "unyielding". +|}] + +external returns_unyielding : 'a -> 'a @ local unyielding = "%identity" + +let _ = requires_unyielding (returns_unyielding "some string") + +[%%expect{| +external returns_unyielding : 'a -> local_ 'a @ unyielding = "%identity" +- : unit = () +|}] + (* [@local_opt] and [yielding]: *) external id : ('a[@local_opt]) -> ('a[@local_opt]) = "%identity" diff --git a/typing/ctype.ml b/typing/ctype.ml index ea89baad3c5..9999c04b960 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1663,14 +1663,12 @@ let instance_label ~fixed lbl = ) (* CR dkalinichenko: we must vary yieldingness together with locality to get - sane behavior around defaults. Remove once we have mode polymorphism. *) + sane behavior around [@local_opt]. Remove once we have mode polymorphism. *) let prim_mode mvar mvar' = function | Primitive.Prim_global, _ -> - Locality.allow_right Locality.global, - Yielding.allow_right Yielding.unyielding + Locality.allow_right Locality.global, Yielding.newvar () | Primitive.Prim_local, _ -> - Locality.allow_right Locality.local, - Yielding.allow_right Yielding.yielding + Locality.allow_right Locality.local, Yielding.newvar () | Primitive.Prim_poly, _ -> match mvar, mvar' with | Some mvar, Some mvar' -> mvar, mvar' From bfbb05cf0aa0f10c8666704bc310d843d7b97927 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 28 Mar 2025 20:02:27 -0400 Subject: [PATCH 12/20] fixes --- typing/includecore.ml | 22 ++++++++-------------- typing/jkind.ml | 8 +------- typing/mode.ml | 10 ++++++++-- 3 files changed, 17 insertions(+), 23 deletions(-) diff --git a/typing/includecore.ml b/typing/includecore.ml index 71b7265b846..31a9a417034 100644 --- a/typing/includecore.ml +++ b/typing/includecore.ml @@ -146,26 +146,20 @@ let value_descriptions ~loc env name | Val_prim p1 -> begin match vd2.val_kind with | Val_prim p2 -> begin - let restrict_locality = [ - (fun m -> Mode.Locality.submode_exn m Mode.Locality.global); - (fun m -> Mode.Locality.submode_exn Mode.Locality.local m) - ] in - let restrict_yielding = [ - (fun m -> Mode.Yielding.submode_exn m Mode.Yielding.unyielding); - (fun m -> Mode.Yielding.submode_exn Mode.Yielding.yielding m) - ] in - List.iter (fun restrict_loc -> - List.iter (fun restrict_yield -> + let locality = [ Mode.Locality.global; Mode.Locality.local ] in + let yielding = [ Mode.Yielding.unyielding; Mode.Yielding.yielding ] in + List.iter (fun loc -> + List.iter (fun yield -> let ty1, _, _, _ = Ctype.instance_prim p1 vd1.val_type in let ty2, mode_l2, mode_y2, _ = Ctype.instance_prim p2 vd2.val_type in - Option.iter restrict_loc mode_l2; - Option.iter restrict_yield mode_y2; + Option.iter (Mode.Locality.equate_exn loc) mode_l2; + Option.iter (Mode.Yielding.equate_exn yield) mode_y2; try Ctype.moregeneral env true ty1 ty2 with Ctype.Moregen err -> raise (Dont_match (Type err)) - ) restrict_yielding - ) restrict_locality; + ) yielding + ) locality; match primitive_descriptions p1 p2 with | None -> Tcoerce_none | Some err -> raise (Dont_match (Primitive_mismatch err)) diff --git a/typing/jkind.ml b/typing/jkind.ml index bcfbcbeab78..bc12f3a8807 100644 --- a/typing/jkind.ml +++ b/typing/jkind.ml @@ -1451,13 +1451,7 @@ module Const = struct Some (List.filter (fun m -> m <> "unyielding") modes) | true, false -> (* Otherwise, print [mod global yielding] to indicate [yielding]. *) - let rec insert_after_global acc = function - | [] -> List.rev acc - | "global" :: rest -> - List.rev_append acc ["global"; "yielding"] @ rest - | x :: rest -> insert_after_global (x :: acc) rest - in - Some (insert_after_global [] modes) + Some (modes @ ["yielding"]) | _, _ -> Some modes) let modality_to_ignore_axes axes_to_ignore = diff --git a/typing/mode.ml b/typing/mode.ml index ca7a92c1b6e..dc41d9da10c 100644 --- a/typing/mode.ml +++ b/typing/mode.ml @@ -1721,7 +1721,12 @@ module Yielding = struct let legacy = of_const Const.legacy - let zap_to_legacy = zap_to_floor + (* [unyielding] is the default for [global]s and [yielding] for [local] + or [regional] values, so we vary [zap_to_legacy] accordingly. *) + let zap_to_legacy ~global = + match global with + | true -> zap_to_floor + | false -> zap_to_ceil end let regional_to_local m = @@ -1810,7 +1815,8 @@ module Comonadic_with (Areality : Areality) = struct let areality = proj Areality m |> Areality.zap_to_legacy in let linearity = proj Linearity m |> Linearity.zap_to_legacy in let portability = proj Portability m |> Portability.zap_to_legacy in - let yielding = proj Yielding m |> Yielding.zap_to_legacy in + let global = Areality.Const.(equal areality legacy) in + let yielding = proj Yielding m |> Yielding.zap_to_legacy ~global in { areality; linearity; portability; yielding } let imply c m = From 13234f238aaef2c3b3f25aeed480873ea33bfeef Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 28 Mar 2025 20:02:30 -0400 Subject: [PATCH 13/20] tests --- testsuite/tests/lib-array/test_iarray.ml | 14 --- .../tests/parsetree/source_jane_street.ml | 29 +---- testsuite/tests/typing-jkind-bounds/basics.ml | 2 +- .../subsumption/modalities.ml | 2 +- testsuite/tests/typing-layouts/allow_any.ml | 2 +- testsuite/tests/typing-local/exclave.ml | 15 +-- testsuite/tests/typing-local/local-layouts.ml | 4 +- testsuite/tests/typing-local/local.ml | 106 ++++++------------ testsuite/tests/typing-modes/crossing.ml | 8 +- testsuite/tests/typing-modes/modes.ml | 33 +----- testsuite/tests/typing-modes/stack.ml | 2 +- testsuite/tests/typing-modes/yielding.ml | 2 +- testsuite/tests/typing-unique/unique.ml | 4 +- 13 files changed, 60 insertions(+), 163 deletions(-) diff --git a/testsuite/tests/lib-array/test_iarray.ml b/testsuite/tests/lib-array/test_iarray.ml index 55d931f03c4..35daae39718 100644 --- a/testsuite/tests/lib-array/test_iarray.ml +++ b/testsuite/tests/lib-array/test_iarray.ml @@ -32,20 +32,6 @@ let rec list_map_local_input (local_ f) (local_ list) = module Iarray = Stdlib_stable.Iarray external ( .:() ) : 'a iarray -> int -> 'a = "%array_safe_get" val iarray : int iarray = [:1; 2; 3; 4; 5:] -val iarray_local : unit -> local_ int iarray @ unyielding = -val ifarray : float iarray = [:1.5; 2.5; 3.5; 4.5; 5.5:] -val ifarray_local : unit -> local_ float iarray @ unyielding = -val marray : int array = [|1; 2; 3; 4; 5|] -val mfarray : float array = [|1.5; 2.5; 3.5; 4.5; 5.5|] -external globalize_float : local_ float -> float = "%obj_dup" -external globalize_string : local_ string -> string = "%obj_dup" -val globalize_int_iarray : local_ int iarray -> int iarray = -val list_map_local_input : - local_ (local_ 'a -> 'b) -> local_ 'a list -> 'b list = -|}, Principal{| -module Iarray = Stdlib_stable.Iarray -external ( .:() ) : 'a iarray -> int -> 'a = "%array_safe_get" -val iarray : int iarray = [:1; 2; 3; 4; 5:] val iarray_local : unit -> local_ int iarray = val ifarray : float iarray = [:1.5; 2.5; 3.5; 4.5; 5.5:] val ifarray_local : unit -> local_ float iarray = diff --git a/testsuite/tests/parsetree/source_jane_street.ml b/testsuite/tests/parsetree/source_jane_street.ml index cb9837f3093..9d125e71d73 100644 --- a/testsuite/tests/parsetree/source_jane_street.ml +++ b/testsuite/tests/parsetree/source_jane_street.ml @@ -492,22 +492,6 @@ let f ~(x1 @ many) stack_ (x1, x2, x3, x4, x5, x9, x10, x11, (* x12, *) x13, x14, x15) [%%expect{| -val f : - x1:'b -> - x2:local_ string -> local_ - (x3:local_ (string -> string) -> - x4:local_ ('a. 'a -> 'a) -> - x5:local_ 'c -> - x6:local_ bool -> - x7:local_ bool -> - x8:local_ unit -> - string -> - local_ 'd -> local_ - 'b * string * (string -> string) * ('e -> 'e) * 'c * string * string * - int array * string * (int -> local_ (int -> int) @ unyielding) * - (int -> local_ (int -> int) @ unyielding) @ contended) @ unyielding = - -|}, Principal{| val f : x1:'b -> x2:local_ string -> @@ -520,8 +504,8 @@ val f : string -> local_ 'd -> local_ 'b * string * (string -> string) * ('e -> 'e) * 'c * string * string * - int array * string * (int -> local_ (int -> int) @ unyielding) * - (int -> local_ (int -> int) @ unyielding) @ contended = + int array * string * (int -> local_ (int -> int)) * + (int -> local_ (int -> int)) @ contended = |}] let f1 (_ @ local) = () @@ -601,14 +585,7 @@ Error: This value escapes its region. let f2 (x @ local) (f @ once) : t2 = exclave_ { x; f } [%%expect{| -val f2 : - local_ float -> local_ - ((float -> float) @ once -> local_ t2 @ once unyielding) @ unyielding = - -|}, Principal{| -val f2 : - local_ float -> (float -> float) @ once -> local_ t2 @ once unyielding = - +val f2 : local_ float -> (float -> float) @ once -> local_ t2 @ once = |}] diff --git a/testsuite/tests/typing-jkind-bounds/basics.ml b/testsuite/tests/typing-jkind-bounds/basics.ml index b011541f76e..797defe8a46 100644 --- a/testsuite/tests/typing-jkind-bounds/basics.ml +++ b/testsuite/tests/typing-jkind-bounds/basics.ml @@ -1183,7 +1183,7 @@ Error: The kind of type "t" is value because it instantiates an unannotated type parameter of t, chosen to have kind value. But the kind of type "t" must be a subkind of - immutable_data mod global yielding aliased + immutable_data mod global aliased yielding because of the annotation on the declaration of the type t. |}] (* CR layouts v2.8: this should be accepted *) diff --git a/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml b/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml index 85b20082731..542067d7984 100644 --- a/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml +++ b/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml @@ -124,7 +124,7 @@ end = struct type 'a t : immediate with 'a @@ aliased many contended global portable end [%%expect {| -module M : sig type 'a t : immutable_data mod global yielding aliased end +module M : sig type 'a t : immutable_data mod global aliased yielding end |}] module M : sig diff --git a/testsuite/tests/typing-layouts/allow_any.ml b/testsuite/tests/typing-layouts/allow_any.ml index a652f616ab3..25b4fd0ff9c 100644 --- a/testsuite/tests/typing-layouts/allow_any.ml +++ b/testsuite/tests/typing-layouts/allow_any.ml @@ -313,7 +313,7 @@ module B = struct let a t = t.a end [%%expect{| -module A : sig type t : mutable_data mod global yielding external_ end +module A : sig type t : mutable_data mod global external_ yielding end module B : sig type t : value mod contended portable = { a : A.t; } diff --git a/testsuite/tests/typing-local/exclave.ml b/testsuite/tests/typing-local/exclave.ml index 443eba967d6..f4948e33919 100644 --- a/testsuite/tests/typing-local/exclave.ml +++ b/testsuite/tests/typing-local/exclave.ml @@ -19,7 +19,7 @@ let foo () = let local_ y = Some 42 in y [%%expect{| -val foo : unit -> local_ int option @ unyielding = +val foo : unit -> local_ int option = |}] (* sidenote: in the above, y escapes the function even though local_ @@ -36,7 +36,7 @@ let foo () = let _ = escape x in x [%%expect{| -val foo : unit -> local_ int option @ unyielding = +val foo : unit -> local_ int option = |}] (* this still applies even when the exclave doesn't allocate in outer region at all, @@ -48,7 +48,7 @@ let foo x = let _ = escape x in x [%%expect{| -val foo : 'a -> local_ int option @ unyielding = +val foo : 'a -> local_ int option = |}] @@ -140,9 +140,6 @@ let foo (local_ x) = [%%expect{| type t = { x : int option; } -val foo : local_ int option -> local_ int option @ unyielding = -|}, Principal{| -type t = { x : int option; } val foo : local_ int option -> local_ int option = |}] @@ -199,8 +196,8 @@ let f () = f ();; [%%expect{| type 'a glob = Glob of global_ 'a -val return_local : 'a -> local_ 'a glob @ unyielding = -val f : unit -> local_ unit @ unyielding = +val return_local : 'a -> local_ 'a glob = +val f : unit -> local_ unit = - : unit = () |}] @@ -236,7 +233,7 @@ let f () = (fun x -> fun y -> ()) : (string -> string -> unit) ) [%%expect{| -val f : unit -> local_ (string -> (string -> unit)) @ unyielding = +val f : unit -> local_ (string -> (string -> unit)) = |}] let f : local_ string -> string = diff --git a/testsuite/tests/typing-local/local-layouts.ml b/testsuite/tests/typing-local/local-layouts.ml index 45a4786cdf7..b07f65b5699 100644 --- a/testsuite/tests/typing-local/local-layouts.ml +++ b/testsuite/tests/typing-local/local-layouts.ml @@ -6,6 +6,6 @@ let foo _t (type a) = exclave_ 1 let bar _t (type a : value) = exclave_ 2 [%%expect{| -val foo : 'a -> local_ int @ unyielding = -val bar : 'a -> local_ int @ unyielding = +val foo : 'a -> local_ int = +val bar : 'a -> local_ int = |}] diff --git a/testsuite/tests/typing-local/local.ml b/testsuite/tests/typing-local/local.ml index d08e292e064..b186d0e488e 100644 --- a/testsuite/tests/typing-local/local.ml +++ b/testsuite/tests/typing-local/local.ml @@ -378,10 +378,6 @@ val foo : ?x:local_ 'a -> unit -> local_ 'a option = let foo ?(local_ x = "hello") () = x;; [%%expect{| -val foo : - ?x:local_ string -> local_ - (unit -> local_ string @ unyielding) @ unyielding = -|}, Principal{| val foo : ?x:local_ string -> unit -> local_ string = |}] @@ -901,7 +897,7 @@ let foo x = exclave_ let r = local_ { contents = x } in print r [%%expect{| -val foo : string -> local_ unit @ unyielding = +val foo : string -> local_ unit = |}] (* Can pass local values to calls explicitly marked as nontail *) @@ -948,7 +944,7 @@ let foo x = exclave_ let local_ foo () = r.contents in foo () [%%expect{| -val foo : 'a -> local_ 'a @ unyielding = +val foo : 'a -> local_ 'a = |}] (* Cannot return local values without annotations on all exits *) @@ -968,7 +964,7 @@ let foo x = exclave_ let r = local_ { contents = x } in r [%%expect{| -val foo : 'a -> local_ 'a ref @ unyielding = +val foo : 'a -> local_ 'a ref = |}] let foo p x = exclave_ @@ -976,7 +972,7 @@ let foo p x = exclave_ if p then r else r [%%expect{| -val foo : bool -> 'a -> local_ 'a ref @ unyielding = +val foo : bool -> 'a -> local_ 'a ref = |}] (* Non-local regional values can be passed to tail calls *) @@ -1008,14 +1004,14 @@ let foo () = exclave_ let _ = local_ (52, 24) in 42 [%%expect{| -val foo : unit -> local_ int @ unyielding = +val foo : unit -> local_ int = |}] let bar () = let _x = 52 in foo () [%%expect{| -val bar : unit -> local_ int @ unyielding = +val bar : unit -> local_ int = |}] (* if not at tail, then not affected *) @@ -1750,25 +1746,17 @@ Line 2, characters 2-32: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Signature mismatch: Modules do not match: - sig - val add : - local_ int32 @ unyielding -> - local_ int32 @ unyielding -> local_ int32 @ unyielding - end + sig val add : local_ int32 -> local_ int32 -> local_ int32 end is not included in sig val add : local_ int32 -> local_ int32 -> int32 end Values do not match: - val add : - local_ int32 @ unyielding -> - local_ int32 @ unyielding -> local_ int32 @ unyielding + val add : local_ int32 -> local_ int32 -> local_ int32 is not included in val add : local_ int32 -> local_ int32 -> int32 - The type - "local_ int32 @ unyielding -> - local_ int32 @ unyielding -> local_ int32 @ unyielding" + The type "local_ int32 -> local_ int32 -> local_ int32" is not compatible with the type "local_ int32 -> local_ int32 -> int32" - Type "local_ int32 @ unyielding -> local_ int32 @ unyielding" - is not compatible with type "local_ int32 -> int32" + Type "local_ int32 -> local_ int32" is not compatible with type + "local_ int32 -> int32" |}] module Opt32 : sig external add : (int32[@local_opt]) -> (int32[@local_opt]) -> (int32[@local_opt]) = "%int32_add" end = Int32 module Bad32_2 : sig val add : local_ int32 -> local_ int32 -> int32 end = @@ -1798,12 +1786,10 @@ Error: Signature mismatch: (int32 [@local_opt]) -> (int32 [@local_opt]) = "%int32_add" is not included in val add : local_ int32 -> local_ int32 -> int32 - The type - "local_ int32 @ unyielding -> - local_ int32 @ unyielding -> local_ int32 @ unyielding" + The type "local_ int32 -> local_ int32 -> local_ int32" is not compatible with the type "local_ int32 -> local_ int32 -> int32" - Type "local_ int32 @ unyielding -> local_ int32 @ unyielding" - is not compatible with type "local_ int32 -> int32" + Type "local_ int32 -> local_ int32" is not compatible with type + "local_ int32 -> int32" |}] module Contravariant_instantiation : sig @@ -1839,25 +1825,11 @@ let nativeint (local_ x) (local_ y) = exclave_ let float (local_ x) (local_ y) = exclave_ (x +. y *. x -. 42.) [%%expect{| -val int32 : - local_ int32 -> local_ - (local_ int32 -> local_ int32 @ unyielding) @ unyielding = -val int64 : - local_ int64 -> local_ - (local_ int64 -> local_ int64 @ unyielding) @ unyielding = -val nativeint : - local_ nativeint -> local_ - (local_ nativeint -> local_ nativeint @ unyielding) @ unyielding = -val float : - local_ float -> local_ - (local_ float -> local_ float @ unyielding) @ unyielding = -|}, Principal{| -val int32 : local_ int32 -> local_ int32 -> local_ int32 @ unyielding = -val int64 : local_ int64 -> local_ int64 -> local_ int64 @ unyielding = -val nativeint : - local_ nativeint -> local_ nativeint -> local_ nativeint @ unyielding = +val int32 : local_ int32 -> local_ int32 -> local_ int32 = +val int64 : local_ int64 -> local_ int64 -> local_ int64 = +val nativeint : local_ nativeint -> local_ nativeint -> local_ nativeint = -val float : local_ float -> local_ float -> local_ float @ unyielding = +val float : local_ float -> local_ float -> local_ float = |}] let etapair (local_ x) = exclave_ (fst x, snd x) @@ -1901,7 +1873,7 @@ let testbool1 f = let local_ r = ref 42 in (f r || false) && true let testbool2 f = let local_ r = ref 42 in true && (false || f r) [%%expect{| -val testbool1 : (local_ int ref @ unyielding -> bool) -> bool = +val testbool1 : (local_ int ref -> bool) -> bool = Line 3, characters 63-64: 3 | let testbool2 f = let local_ r = ref 42 in true && (false || f r) ^ @@ -1915,8 +1887,8 @@ Error: This value escapes its region. let foo () = exclave_ let local_ _x = "hello" in true let testboo3 () = true && (foo ()) [%%expect{| -val foo : unit -> local_ bool @ unyielding = -val testboo3 : unit -> local_ bool @ unyielding = +val foo : unit -> local_ bool = +val testboo3 : unit -> local_ bool = |}] (* Test from Nathanaëlle Courant. @@ -1988,15 +1960,14 @@ let f g n = () let z : (int list -> unit) -> int -> unit = f [%%expect{| -val f : (local_ int list @ unyielding -> unit) -> int -> unit = +val f : (local_ int list -> unit) -> int -> unit = Line 5, characters 44-45: 5 | let z : (int list -> unit) -> int -> unit = f ^ -Error: This expression has type - "(local_ int list @ unyielding -> unit) -> int -> unit" +Error: This expression has type "(local_ int list -> unit) -> int -> unit" but an expression was expected of type "(int list -> unit) -> int -> unit" - Type "local_ int list @ unyielding -> unit" is not compatible with type + Type "local_ int list -> unit" is not compatible with type "int list -> unit" |}] @@ -2011,11 +1982,10 @@ end Line 6, characters 46-47: 6 | let z : (int list -> unit) -> int -> unit = f ^ -Error: This expression has type - "(local_ int list @ unyielding -> unit) -> int -> unit" +Error: This expression has type "(local_ int list -> unit) -> int -> unit" but an expression was expected of type "(int list -> unit) -> int -> unit" - Type "local_ int list @ unyielding -> unit" is not compatible with type + Type "local_ int list -> unit" is not compatible with type "int list -> unit" |}] @@ -2470,7 +2440,7 @@ Error: This value escapes its region. (* constructing local iarray from local elements is fine *) let f (local_ x : string) = exclave_ [:x; "foo":] [%%expect{| -val f : local_ string -> local_ string iarray @ unyielding = +val f : local_ string -> local_ string iarray = |}] (* constructing global iarray from global elements is fine *) @@ -2509,7 +2479,7 @@ let f (local_ a : string iarray) = | [: x; _ :] -> x | _ -> "foo" [%%expect{| -val f : local_ string iarray -> local_ string @ unyielding = +val f : local_ string iarray -> local_ string = |}] (* projecting out of global iarray gives global elements *) @@ -2536,7 +2506,7 @@ Error: This value escapes its region. (* constructing local array from global elements is allowed *) let f (x : string) = exclave_ [| x |] [%%expect{| -val f : string -> local_ string array @ unyielding = +val f : string -> local_ string array = |}] (* projecting out of local array gives global elements *) @@ -2590,18 +2560,16 @@ Lines 3-6, characters 6-3: Error: Signature mismatch: Modules do not match: sig - val g : 'a -> 'b -> local_ string @ unyielding - val f : - 'a -> local_ ('b -> local_ string @ unyielding) @ unyielding + val g : 'a -> 'b -> local_ string + val f : 'a -> local_ ('b -> local_ string) end is not included in sig val f : string -> string -> local_ string end Values do not match: - val f : 'a -> local_ ('b -> local_ string @ unyielding) @ unyielding + val f : 'a -> local_ ('b -> local_ string) is not included in val f : string -> string -> local_ string - The type - "string -> local_ (string -> local_ string @ unyielding) @ unyielding" + The type "string -> local_ (string -> local_ string)" is not compatible with the type "string -> string -> local_ string" |}] @@ -2673,13 +2641,13 @@ val f : unit -> local_ string -> (string -> string) = let f () = exclave_ ((fun x -> fun y -> x + y) : (_ -> _));; [%%expect{| -val f : unit -> local_ (int -> (int -> int)) @ unyielding = +val f : unit -> local_ (int -> (int -> int)) = |}];; (* ok if curried *) let f () = exclave_ ((fun x -> (fun y -> x + y) [@extension.curry]) : (_ -> _));; [%%expect{| -val f : unit -> local_ (int -> (int -> int)) @ unyielding = +val f : unit -> local_ (int -> (int -> int)) = |}];; (* Type annotations on a [local_] binding are interpreted in a local context, @@ -2769,12 +2737,12 @@ val _ret : unit -> M.t -> unit = let _ret () : M.t -> unit = exclave_ (fun M_constructor -> ()) [%%expect{| -val _ret : unit -> local_ (M.t -> unit) @ unyielding = +val _ret : unit -> local_ (M.t -> unit) = |}] let _ret () : M.t -> unit = exclave_ (fun M_constructor -> ()) [%%expect{| -val _ret : unit -> local_ (M.t -> unit) @ unyielding = +val _ret : unit -> local_ (M.t -> unit) = |}] type r = {global_ x : string; y : string} diff --git a/testsuite/tests/typing-modes/crossing.ml b/testsuite/tests/typing-modes/crossing.ml index 20ad39423b3..51b9d9f3f4a 100644 --- a/testsuite/tests/typing-modes/crossing.ml +++ b/testsuite/tests/typing-modes/crossing.ml @@ -68,15 +68,15 @@ Lines 3-5, characters 6-3: 5 | end Error: Signature mismatch: Modules do not match: - sig val f : unit -> local_ int @ unyielding end + sig val f : unit -> local_ int end is not included in sig val f : unit -> int end Values do not match: - val f : unit -> local_ int @ unyielding + val f : unit -> local_ int is not included in val f : unit -> int - The type "unit -> local_ int @ unyielding" - is not compatible with the type "unit -> int" + The type "unit -> local_ int" is not compatible with the type + "unit -> int" |}] module M : sig diff --git a/testsuite/tests/typing-modes/modes.ml b/testsuite/tests/typing-modes/modes.ml index e7ec1c53a5f..39d880861f3 100644 --- a/testsuite/tests/typing-modes/modes.ml +++ b/testsuite/tests/typing-modes/modes.ml @@ -394,19 +394,11 @@ type r = { mutable x : string; } let foo ?(local_ x @ unique once = 42) () = () [%%expect{| -val foo : - ?x:local_ int @ once unique -> local_ (unit -> unit) @ once unyielding = - -|}, Principal{| val foo : ?x:local_ int @ once unique -> unit -> unit = |}] let foo ?(local_ x : _ @@ unique once = 42) () = () [%%expect{| -val foo : - ?x:local_ int @ once unique -> local_ (unit -> unit) @ once unyielding = - -|}, Principal{| val foo : ?x:local_ int @ once unique -> unit -> unit = |}] @@ -420,19 +412,11 @@ Error: Optional parameters cannot be polymorphic let foo ?x:(local_ (x,y) @ unique once = (42, 42)) () = () [%%expect{| -val foo : - ?x:local_ int * int @ once unique -> local_ (unit -> unit) @ once - unyielding = -|}, Principal{| val foo : ?x:local_ int * int @ once unique -> unit -> unit = |}] let foo ?x:(local_ (x,y) : _ @@ unique once = (42, 42)) () = () [%%expect{| -val foo : - ?x:local_ int * int @ once unique -> local_ (unit -> unit) @ once - unyielding = -|}, Principal{| val foo : ?x:local_ int * int @ once unique -> unit -> unit = |}] @@ -498,11 +482,11 @@ let local_ret a = exclave_ (Some a) let bad_use = use_global_ret local_ret "hello" [%%expect{| val use_global_ret : ('a -> 'b) -> 'a -> 'b lazy_t = -val local_ret : 'a -> local_ 'a option @ unyielding = +val local_ret : 'a -> local_ 'a option = Line 3, characters 29-38: 3 | let bad_use = use_global_ret local_ret "hello" ^^^^^^^^^ -Error: This expression has type "'a -> local_ 'a option @ unyielding" +Error: This expression has type "'a -> local_ 'a option" but an expression was expected of type "'b -> 'c" |}] @@ -575,12 +559,6 @@ let result = use_local foo 1. 2. val use_local : local_ ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = val use_global : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = val foo : float -> float -> float = -val bar : local_ float -> local_ (local_ float -> unit) @ unyielding = -val result : float = 3. -|}, Principal{| -val use_local : local_ ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = -val use_global : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = -val foo : float -> float -> float = val bar : local_ float -> local_ float -> unit = val result : float = 3. |}] @@ -598,13 +576,6 @@ val result : float = 3. let result = use_global bar 1. 2. [%%expect{| Line 1, characters 24-27: -1 | let result = use_global bar 1. 2. - ^^^ -Error: This expression has type - "local_ float -> local_ (local_ float -> unit) @ unyielding" - but an expression was expected of type "local_ 'a -> ('b -> 'c)" -|}, Principal{| -Line 1, characters 24-27: 1 | let result = use_global bar 1. 2. ^^^ Error: This expression has type "local_ float -> local_ float -> unit" diff --git a/testsuite/tests/typing-modes/stack.ml b/testsuite/tests/typing-modes/stack.ml index 6477d0ff8f5..062b70e3225 100644 --- a/testsuite/tests/typing-modes/stack.ml +++ b/testsuite/tests/typing-modes/stack.ml @@ -202,7 +202,7 @@ Error: This value escapes its region. let f () = exclave_ stack_ (3, 5) [%%expect{| -val f : unit -> local_ int * int @ unyielding = +val f : unit -> local_ int * int = |}] let f () = diff --git a/testsuite/tests/typing-modes/yielding.ml b/testsuite/tests/typing-modes/yielding.ml index 1e1a1f60584..ab5ed931a55 100644 --- a/testsuite/tests/typing-modes/yielding.ml +++ b/testsuite/tests/typing-modes/yielding.ml @@ -184,7 +184,7 @@ external id : ('a [@local_opt]) -> ('a [@local_opt]) = "%identity" val f1 : 'a -> 'a = val f2 : local_ 'a -> local_ 'a = val f3 : 'a @ yielding -> 'a @ yielding = -val f4 : local_ 'a @ unyielding -> local_ 'a @ unyielding = +val f4 : local_ 'a @ unyielding -> local_ 'a = |}] (* [mod global] implies [mod unyielding] by default. *) diff --git a/testsuite/tests/typing-unique/unique.ml b/testsuite/tests/typing-unique/unique.ml index 6d3f2da81ae..2ae43cc457f 100644 --- a/testsuite/tests/typing-unique/unique.ml +++ b/testsuite/tests/typing-unique/unique.ml @@ -367,7 +367,7 @@ val ul : local_ 'a @ unique -> local_ 'a = let ul_ret x = exclave_ unique_ x [%%expect{| -val ul_ret : 'a @ unique -> local_ 'a @ unyielding = +val ul_ret : 'a @ unique -> local_ 'a = |}] let rec foo = @@ -385,8 +385,6 @@ let rec bar = | Some () -> () | None -> bar (local_ Some ()) [@nontail] [%%expect{| -val bar : local_ unit option @ unique unyielding -> unit = -|}, Principal{| val bar : local_ unit option @ unique -> unit = |}] From 2cbe9f03d3e2df45302583c9d9d362999260e28d Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 28 Mar 2025 20:32:18 -0400 Subject: [PATCH 14/20] fix lazy --- testsuite/tests/typing-modes/lazy.ml | 12 +++++++++++- typing/typecore.ml | 5 ++++- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/testsuite/tests/typing-modes/lazy.ml b/testsuite/tests/typing-modes/lazy.ml index 2b1eaecc6eb..27f7993ee57 100644 --- a/testsuite/tests/typing-modes/lazy.ml +++ b/testsuite/tests/typing-modes/lazy.ml @@ -28,6 +28,16 @@ Line 2, characters 18-19: Error: The value "x" is local, so cannot be used inside a lazy expression. |}] +(* For simplicity, we also require them to be [unyielding]. *) +let foo (x @ yielding) = + lazy (let _ = x in ()) +[%%expect{| +Line 2, characters 18-19: +2 | lazy (let _ = x in ()) + ^ +Error: The value "x" is yielding, so cannot be used inside a lazy expression that may not yield. +|}] + (* lazy expression is constructed as global *) let foo () = lazy ("hello") @@ -40,7 +50,7 @@ let foo (x @ local) = match x with | lazy y -> y [%%expect{| -val foo : local_ 'a lazy_t -> 'a @ yielding = +val foo : local_ 'a lazy_t -> 'a = |}] (* one can construct [portable] lazy only if the result is [portable] *) diff --git a/typing/typecore.ml b/typing/typecore.ml index 9a92ede7bc5..1889eeea99e 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -543,7 +543,9 @@ let mode_coerce mode expected_mode = let mode_lazy expected_mode = let expected_mode = - mode_coerce (Value.max_with (Comonadic Areality) Regionality.global) + mode_coerce ( + Value.max_with (Comonadic Areality) Regionality.global + |> Value.meet_with (Comonadic Yielding) Yielding.Const.Unyielding) expected_mode in let closure_mode = @@ -652,6 +654,7 @@ let tuple_pat_mode mode tuple_modes = let global_pat_mode {mode; _}= let mode = Value.meet_with (Comonadic Areality) Regionality.Const.Global mode + |> Value.meet_with (Comonadic Yielding) Yielding.Const.Unyielding in simple_pat_mode mode From 40231d9e6504a14e029defbe7e8351a31067dbbd Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Fri, 28 Mar 2025 20:33:00 -0400 Subject: [PATCH 15/20] format --- typing/mode.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/typing/mode.ml b/typing/mode.ml index dc41d9da10c..28de5e8e31e 100644 --- a/typing/mode.ml +++ b/typing/mode.ml @@ -1724,9 +1724,7 @@ module Yielding = struct (* [unyielding] is the default for [global]s and [yielding] for [local] or [regional] values, so we vary [zap_to_legacy] accordingly. *) let zap_to_legacy ~global = - match global with - | true -> zap_to_floor - | false -> zap_to_ceil + match global with true -> zap_to_floor | false -> zap_to_ceil end let regional_to_local m = From 386463db424ce8b32312a4507674dc2e24f1f8e8 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Mon, 31 Mar 2025 14:38:15 -0400 Subject: [PATCH 16/20] keep order --- testsuite/tests/typing-jkind-bounds/basics.ml | 10 +++++----- .../tests/typing-jkind-bounds/composite.ml | 4 ++-- testsuite/tests/typing-jkind-bounds/predef.ml | 6 +++--- .../tests/typing-jkind-bounds/printing.ml | 14 +++++++------- .../tests/typing-jkind-bounds/records.ml | 4 ++-- .../typing-jkind-bounds/subsumption/basics.ml | 8 ++++---- .../subsumption/constraint.ml | 2 +- .../subsumption/functors.ml | 4 ++-- .../tests/typing-jkind-bounds/variants.ml | 4 ++-- testsuite/tests/typing-modal-kinds/basics.ml | 2 +- typing/typemode.ml | 19 ++++++++++--------- 11 files changed, 39 insertions(+), 38 deletions(-) diff --git a/testsuite/tests/typing-jkind-bounds/basics.ml b/testsuite/tests/typing-jkind-bounds/basics.ml index 797defe8a46..6398f5a0e0e 100644 --- a/testsuite/tests/typing-jkind-bounds/basics.ml +++ b/testsuite/tests/typing-jkind-bounds/basics.ml @@ -990,7 +990,7 @@ type ('a : immediate) t : value mod global = { mutable x : 'a } Line 1, characters 0-63: 1 | type ('a : immediate) t : value mod global = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ unyielding many +Error: The kind of type "t" is mutable_data with 'a @@ many unyielding because it's a boxed record type. But the kind of type "t" must be a subkind of value mod global because of the annotation on the declaration of the type t. @@ -1004,7 +1004,7 @@ type ('a : immediate) t : value mod aliased = { mutable x : 'a } Line 1, characters 0-64: 1 | type ('a : immediate) t : value mod aliased = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ unyielding many +Error: The kind of type "t" is mutable_data with 'a @@ many unyielding because it's a boxed record type. But the kind of type "t" must be a subkind of value mod aliased because of the annotation on the declaration of the type t. @@ -1018,7 +1018,7 @@ type ('a : immediate) t : value mod contended = { mutable x : 'a } Line 1, characters 0-66: 1 | type ('a : immediate) t : value mod contended = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ unyielding many +Error: The kind of type "t" is mutable_data with 'a @@ many unyielding because it's a boxed record type. But the kind of type "t" must be a subkind of value mod contended because of the annotation on the declaration of the type t. @@ -1032,7 +1032,7 @@ type ('a : immediate) t : value mod external_ = { mutable x : 'a } Line 1, characters 0-66: 1 | type ('a : immediate) t : value mod external_ = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ unyielding many +Error: The kind of type "t" is mutable_data with 'a @@ many unyielding because it's a boxed record type. But the kind of type "t" must be a subkind of value mod external_ because of the annotation on the declaration of the type t. @@ -1046,7 +1046,7 @@ type ('a : immediate) t : value mod external64 = { mutable x : 'a } Line 1, characters 0-67: 1 | type ('a : immediate) t : value mod external64 = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ unyielding many +Error: The kind of type "t" is mutable_data with 'a @@ many unyielding because it's a boxed record type. But the kind of type "t" must be a subkind of value mod external64 because of the annotation on the declaration of the type t. diff --git a/testsuite/tests/typing-jkind-bounds/composite.ml b/testsuite/tests/typing-jkind-bounds/composite.ml index 7f425c1229f..0a187aad2c8 100644 --- a/testsuite/tests/typing-jkind-bounds/composite.ml +++ b/testsuite/tests/typing-jkind-bounds/composite.ml @@ -189,7 +189,7 @@ Line 1, characters 13-20: 1 | let foo (t : int ref t @@ contended) = use_uncontended t ^^^^^^^ Error: This type "int ref" should be an instance of type "('a : immutable_data)" - The kind of int ref is mutable_data with int @@ unyielding many. + The kind of int ref is mutable_data with int @@ many unyielding. But the kind of int ref must be a subkind of immutable_data because of the definition of t at line 1, characters 0-46. @@ -339,7 +339,7 @@ Line 1, characters 13-20: 1 | let foo (t : int ref t @@ contended) = use_uncontended t ^^^^^^^ Error: This type "int ref" should be an instance of type "('a : immutable_data)" - The kind of int ref is mutable_data with int @@ unyielding many. + The kind of int ref is mutable_data with int @@ many unyielding. But the kind of int ref must be a subkind of immutable_data because of the definition of t at line 1, characters 0-73. diff --git a/testsuite/tests/typing-jkind-bounds/predef.ml b/testsuite/tests/typing-jkind-bounds/predef.ml index fc250e0f2f7..af9f1121145 100644 --- a/testsuite/tests/typing-jkind-bounds/predef.ml +++ b/testsuite/tests/typing-jkind-bounds/predef.ml @@ -176,7 +176,7 @@ type 'a t : mutable_data = 'a ref Line 1, characters 0-33: 1 | type 'a t : mutable_data = 'a ref ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "'a ref" is mutable_data with 'a @@ unyielding many. +Error: The kind of type "'a ref" is mutable_data with 'a @@ many unyielding. But the kind of type "'a ref" must be a subkind of mutable_data because of the definition of t at line 1, characters 0-33. @@ -198,7 +198,7 @@ Line 1, characters 14-21: ^^^^^^^ Error: This type "int ref" should be an instance of type "('a : value mod portable)" - The kind of int ref is mutable_data with int @@ unyielding many. + The kind of int ref is mutable_data with int @@ many unyielding. But the kind of int ref must be a subkind of value mod portable because of the definition of require_portable at line 10, characters 0-47. @@ -222,7 +222,7 @@ Line 1, characters 14-21: ^^^^^^^ Error: This type "int ref" should be an instance of type "('a : value mod contended)" - The kind of int ref is mutable_data with int @@ unyielding many. + The kind of int ref is mutable_data with int @@ many unyielding. But the kind of int ref must be a subkind of value mod contended because of the definition of require_contended at line 9, characters 0-49. diff --git a/testsuite/tests/typing-jkind-bounds/printing.ml b/testsuite/tests/typing-jkind-bounds/printing.ml index 676fc8d93a8..cf80f3d8c6e 100644 --- a/testsuite/tests/typing-jkind-bounds/printing.ml +++ b/testsuite/tests/typing-jkind-bounds/printing.ml @@ -175,7 +175,7 @@ Line 3, characters 11-12: ^ Error: This type "a" = "int ref" should be an instance of type "('a : immutable_data)" - The kind of a is mutable_data with int @@ unyielding many. + The kind of a is mutable_data with int @@ many unyielding. But the kind of a must be a subkind of immutable_data because of the definition of t at line 2, characters 0-28. @@ -335,15 +335,15 @@ Error: Signature mismatch: Modules do not match: sig type 'a t : mutable_data with 'a end is not included in - sig type 'a t : mutable_data with 'a @@ unyielding many end + sig type 'a t : mutable_data with 'a @@ many unyielding end Type declarations do not match: type 'a t : mutable_data with 'a is not included in - type 'a t : mutable_data with 'a @@ unyielding many + type 'a t : mutable_data with 'a @@ many unyielding The kind of the first is mutable_data with 'a because of the definition of t at line 4, characters 2-34. But the kind of the first must be a subkind of mutable_data - with 'a @@ unyielding many + with 'a @@ many unyielding because of the definition of t at line 2, characters 2-40. The first mode-crosses less than the second along: @@ -415,14 +415,14 @@ Lines 3-5, characters 6-3: 5 | end Error: Signature mismatch: Modules do not match: - sig type 'a t : mutable_data with 'a @@ unyielding many end + sig type 'a t : mutable_data with 'a @@ many unyielding end is not included in sig type 'a t : immutable_data with 'a end Type declarations do not match: - type 'a t : mutable_data with 'a @@ unyielding many + type 'a t : mutable_data with 'a @@ many unyielding is not included in type 'a t : immutable_data with 'a - The kind of the first is mutable_data with 'a @@ unyielding many + The kind of the first is mutable_data with 'a @@ many unyielding because of the definition of t at line 4, characters 2-40. But the kind of the first must be a subkind of immutable_data with 'a because of the definition of t at line 2, characters 2-56. diff --git a/testsuite/tests/typing-jkind-bounds/records.ml b/testsuite/tests/typing-jkind-bounds/records.ml index 57fce9a7efb..2de8a1175ad 100644 --- a/testsuite/tests/typing-jkind-bounds/records.ml +++ b/testsuite/tests/typing-jkind-bounds/records.ml @@ -128,7 +128,7 @@ type 'a t : immutable_data = { mutable x : 'a } Line 1, characters 0-47: 1 | type 'a t : immutable_data = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ unyielding many +Error: The kind of type "t" is mutable_data with 'a @@ many unyielding because it's a boxed record type. But the kind of type "t" must be a subkind of immutable_data because of the annotation on the declaration of the type t. @@ -268,7 +268,7 @@ type 'a t : immutable_data with 'a = { mutable x : 'a } Line 1, characters 0-55: 1 | type 'a t : immutable_data with 'a = { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ unyielding many +Error: The kind of type "t" is mutable_data with 'a @@ many unyielding because it's a boxed record type. But the kind of type "t" must be a subkind of immutable_data with 'a because of the annotation on the declaration of the type t. diff --git a/testsuite/tests/typing-jkind-bounds/subsumption/basics.ml b/testsuite/tests/typing-jkind-bounds/subsumption/basics.ml index 0571e281735..75b8bbdcd91 100644 --- a/testsuite/tests/typing-jkind-bounds/subsumption/basics.ml +++ b/testsuite/tests/typing-jkind-bounds/subsumption/basics.ml @@ -176,15 +176,15 @@ Error: Signature mismatch: Modules do not match: sig type 'a t : mutable_data with 'a end is not included in - sig type 'a t : mutable_data with 'a @@ unyielding many end + sig type 'a t : mutable_data with 'a @@ many unyielding end Type declarations do not match: type 'a t : mutable_data with 'a is not included in - type 'a t : mutable_data with 'a @@ unyielding many + type 'a t : mutable_data with 'a @@ many unyielding The kind of the first is mutable_data with 'a because of the definition of t at line 4, characters 2-34. But the kind of the first must be a subkind of mutable_data - with 'a @@ unyielding many + with 'a @@ many unyielding because of the definition of t at line 2, characters 2-40. The first mode-crosses less than the second along: @@ -198,7 +198,7 @@ end = struct type 'a t : mutable_data with 'a @@ many unyielding end [%%expect {| -module M : sig type 'a t : mutable_data with 'a @@ unyielding many end +module M : sig type 'a t : mutable_data with 'a @@ many unyielding end |}] (* CR layouts v2.8: 'a u's kind should get normalized to just immutable_data *) diff --git a/testsuite/tests/typing-jkind-bounds/subsumption/constraint.ml b/testsuite/tests/typing-jkind-bounds/subsumption/constraint.ml index 9e9b1e06f4d..ff578233184 100644 --- a/testsuite/tests/typing-jkind-bounds/subsumption/constraint.ml +++ b/testsuite/tests/typing-jkind-bounds/subsumption/constraint.ml @@ -141,7 +141,7 @@ Error: Signature mismatch: type 'a t = Foo of 'a constraint 'a = 'b ref is not included in type 'a t : immutable_data with 'b constraint 'a = 'b ref - The kind of the first is mutable_data with 'b @@ unyielding many + The kind of the first is mutable_data with 'b @@ many unyielding because of the definition of t at line 4, characters 2-46. But the kind of the first must be a subkind of immutable_data with 'b because of the definition of t at line 2, characters 2-59. diff --git a/testsuite/tests/typing-jkind-bounds/subsumption/functors.ml b/testsuite/tests/typing-jkind-bounds/subsumption/functors.ml index 3ee184249c5..a4f07323ad9 100644 --- a/testsuite/tests/typing-jkind-bounds/subsumption/functors.ml +++ b/testsuite/tests/typing-jkind-bounds/subsumption/functors.ml @@ -59,7 +59,7 @@ Line 4, characters 0-48: 4 | type 'a t : immutable_data with 'a = 'a F(Ref).t ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The kind of type "'a F(Ref).t" is mutable_data - with 'a @@ unyielding many + with 'a @@ many unyielding because of the definition of t at line 2, characters 2-40. But the kind of type "'a F(Ref).t" must be a subkind of immutable_data with 'a @@ -79,7 +79,7 @@ Line 4, characters 0-38: 4 | type 'a t : mutable_data = 'a F(Ref).t ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The kind of type "'a F(Ref).t" is mutable_data - with 'a @@ unyielding many + with 'a @@ many unyielding because of the definition of t at line 2, characters 2-40. But the kind of type "'a F(Ref).t" must be a subkind of mutable_data because of the definition of t at line 4, characters 0-38. diff --git a/testsuite/tests/typing-jkind-bounds/variants.ml b/testsuite/tests/typing-jkind-bounds/variants.ml index 5c7d4531aaa..1dd06dc4f4f 100644 --- a/testsuite/tests/typing-jkind-bounds/variants.ml +++ b/testsuite/tests/typing-jkind-bounds/variants.ml @@ -132,7 +132,7 @@ type 'a t : immutable_data = Foo of { mutable x : 'a } Line 1, characters 0-54: 1 | type 'a t : immutable_data = Foo of { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ unyielding many +Error: The kind of type "t" is mutable_data with 'a @@ many unyielding because it's a boxed variant type. But the kind of type "t" must be a subkind of immutable_data because of the annotation on the declaration of the type t. @@ -272,7 +272,7 @@ type 'a t : immutable_data with 'a = Foo of { mutable x : 'a } Line 1, characters 0-62: 1 | type 'a t : immutable_data with 'a = Foo of { mutable x : 'a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is mutable_data with 'a @@ unyielding many +Error: The kind of type "t" is mutable_data with 'a @@ many unyielding because it's a boxed variant type. But the kind of type "t" must be a subkind of immutable_data with 'a because of the annotation on the declaration of the type t. diff --git a/testsuite/tests/typing-modal-kinds/basics.ml b/testsuite/tests/typing-modal-kinds/basics.ml index 2dcc40c97eb..7afe5dc325d 100644 --- a/testsuite/tests/typing-modal-kinds/basics.ml +++ b/testsuite/tests/typing-modal-kinds/basics.ml @@ -940,7 +940,7 @@ Line 1, characters 10-19: ^^^^^^^^^ Error: This type "int t ref" should be an instance of type "('a : value mod contended)" - The kind of int t ref is mutable_data with int t @@ unyielding many. + The kind of int t ref is mutable_data with int t @@ many unyielding. But the kind of int t ref must be a subkind of value mod contended because of the definition of require_contended at line 1, characters 0-49. diff --git a/typing/typemode.ml b/typing/typemode.ml index e514114777d..dc5a880b592 100644 --- a/typing/typemode.ml +++ b/typing/typemode.ml @@ -361,19 +361,20 @@ let untransl_yielding l = l in match areality, yielding with - | Some Global, Some Unyielding | Some Local, Some Yielding -> [] - | _, Some yld -> [Modality.Atom (Comonadic Yielding, Meet_with yld)] - | _, None -> [] + | Some Global, Some Unyielding | Some Local, Some Yielding -> None + | _, Some yld -> Some (Modality.Atom (Comonadic Yielding, Meet_with yld)) + | _, None -> None let untransl_modalities mut attrs t = let l = Modality.Value.Const.to_list t in let l = - untransl_yielding l - @ List.filter - (function - | Modality.Atom (Comonadic Yielding, _) -> false - | a -> not (Modality.is_id a)) - l + (* [filter_map] instead of [filter] + [append] to preserve order. *) + List.filter_map + (function + | Modality.Atom (Comonadic Yielding, _) -> untransl_yielding l + | a when Modality.is_id a -> None + | a -> Some a) + l in let mut_modalities = mutable_implied_modalities mut attrs in (* polymorphic equality suffices for now. *) From 80a329c2a034e141a43979e59bd5152e26ef55c7 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Mon, 31 Mar 2025 14:56:25 -0400 Subject: [PATCH 17/20] fix mixed mode annots --- lambda/translcore.ml | 5 +--- testsuite/tests/typing-modes/yielding.ml | 32 ++++++++++++++++++++++++ typing/ctype.ml | 23 +++++++++++------ typing/ctype.mli | 2 -- 4 files changed, 48 insertions(+), 14 deletions(-) diff --git a/lambda/translcore.ml b/lambda/translcore.ml index dce17c944d8..00cdb6ffa4a 100644 --- a/lambda/translcore.ml +++ b/lambda/translcore.ml @@ -325,10 +325,7 @@ let can_apply_primitive p pmode pos args = else if nargs < p.prim_arity then false else if pos <> Typedtree.Tail then true else begin - let return_mode, _ = - Ctype.prim_mode - pmode (Some (Mode.Yielding.newvar ())) p.prim_native_repr_res - in + let return_mode = Ctype.prim_mode pmode p.prim_native_repr_res in is_heap_mode (transl_locality_mode_l return_mode) end end diff --git a/testsuite/tests/typing-modes/yielding.ml b/testsuite/tests/typing-modes/yielding.ml index ab5ed931a55..08e9b5b8f47 100644 --- a/testsuite/tests/typing-modes/yielding.ml +++ b/testsuite/tests/typing-modes/yielding.ml @@ -187,6 +187,38 @@ val f3 : 'a @ yielding -> 'a @ yielding = val f4 : local_ 'a @ unyielding -> local_ 'a = |}] +(* Test [instance_prim] + mixed mode annots. *) +external requires_unyielding : 'a @ local unyielding -> (unit [@local_opt]) = "%ignore" + +let f1 x = requires_unyielding x +[%%expect{| +external requires_unyielding : local_ 'a @ unyielding -> (unit [@local_opt]) + = "%ignore" +val f1 : 'a -> unit = +|}] + +let f2 (x @ local) = exclave_ requires_unyielding x + +[%%expect{| +Line 1, characters 50-51: +1 | let f2 (x @ local) = exclave_ requires_unyielding x + ^ +Error: This value is "yielding" but expected to be "unyielding". +|}] + +let f3 (x @ yielding) = requires_unyielding x +[%%expect{| +Line 1, characters 44-45: +1 | let f3 (x @ yielding) = requires_unyielding x + ^ +Error: This value is "yielding" but expected to be "unyielding". +|}] + +let f4 (x @ local unyielding) = exclave_ requires_unyielding x +[%%expect{| +val f4 : local_ 'a @ unyielding -> local_ unit = +|}] + (* [mod global] implies [mod unyielding] by default. *) type ('a : value mod global) u1 diff --git a/typing/ctype.ml b/typing/ctype.ml index 9999c04b960..e7c88881c1a 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1664,15 +1664,19 @@ let instance_label ~fixed lbl = (* CR dkalinichenko: we must vary yieldingness together with locality to get sane behavior around [@local_opt]. Remove once we have mode polymorphism. *) -let prim_mode mvar mvar' = function +let prim_mode' mvar mvar' = function | Primitive.Prim_global, _ -> - Locality.allow_right Locality.global, Yielding.newvar () + Locality.allow_right Locality.global, None | Primitive.Prim_local, _ -> - Locality.allow_right Locality.local, Yielding.newvar () + Locality.allow_right Locality.local, None | Primitive.Prim_poly, _ -> - match mvar, mvar' with - | Some mvar, Some mvar' -> mvar, mvar' - | None, _ | _, None -> assert false + match mvar with + | Some mvar -> mvar, mvar' + | None -> assert false + +(* Exported version. *) +let prim_mode mvar prim = + fst (prim_mode' mvar (Some (Yielding.newvar ())) prim) (** Returns a new mode variable whose locality is the given locality and whose yieldingness is the given yieldingness, while all other axes are @@ -1680,6 +1684,9 @@ let prim_mode mvar mvar' = function let with_locality_and_yielding (locality, yielding) m = let m' = Alloc.newvar () in Locality.equate_exn (Alloc.proj (Comonadic Areality) m') locality; + let yielding = + Option.value ~default:(Alloc.proj (Comonadic Yielding) m) yielding + in Yielding.equate_exn (Alloc.proj (Comonadic Yielding) m') yielding; Alloc.submode_exn m' (Alloc.join_const { Alloc.Const.min with @@ -1716,7 +1723,7 @@ let rec instance_prim_locals locals mvar_l mvar_y macc (loc, yld) ty = match locals, get_desc ty with | l :: locals, Tarrow ((lbl,marg,mret),arg,ret,commu) -> let marg = with_locality_and_yielding - (prim_mode (Some mvar_l) (Some mvar_y) l) marg + (prim_mode' (Some mvar_l) (Some mvar_y) l) marg in let macc = Alloc.join [ @@ -1811,7 +1818,7 @@ let instance_prim_mode (desc : Primitive.description) ty = List.exists is_poly desc.prim_native_repr_args then let mode_l = Locality.newvar () in let mode_y = Yielding.newvar () in - let finalret = prim_mode (Some mode_l) (Some mode_y) desc.prim_native_repr_res in + let finalret = prim_mode' (Some mode_l) (Some mode_y) desc.prim_native_repr_res in instance_prim_locals desc.prim_native_repr_args mode_l mode_y (Alloc.disallow_right Alloc.legacy) finalret ty, Some mode_l, Some mode_y diff --git a/typing/ctype.mli b/typing/ctype.mli index 3fb5311e572..b8786be6d5a 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -223,10 +223,8 @@ val instance_label: (* Same, for a label *) val prim_mode : (Mode.allowed * 'r) Mode.Locality.t option - -> (Mode.allowed * 'r) Mode.Yielding.t option -> (Primitive.mode * Primitive.native_repr) -> (Mode.allowed * 'r) Mode.Locality.t - * (Mode.allowed * 'r) Mode.Yielding.t val instance_prim: Primitive.description -> type_expr -> type_expr * Mode.Locality.lr option From 3ca826af34a34a94905455e7d9f2aaeee20a77c1 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Tue, 1 Apr 2025 11:12:23 -0400 Subject: [PATCH 18/20] fixes --- testsuite/tests/typing-modes/yielding.ml | 10 ++++++++++ typing/ctype.ml | 6 +++--- typing/ctype.mli | 3 +-- 3 files changed, 14 insertions(+), 5 deletions(-) diff --git a/testsuite/tests/typing-modes/yielding.ml b/testsuite/tests/typing-modes/yielding.ml index 08e9b5b8f47..e4daa9206e7 100644 --- a/testsuite/tests/typing-modes/yielding.ml +++ b/testsuite/tests/typing-modes/yielding.ml @@ -219,6 +219,16 @@ let f4 (x @ local unyielding) = exclave_ requires_unyielding x val f4 : local_ 'a @ unyielding -> local_ unit = |}] +(* [@local_opt] overrides annotations. *) +external overridden: ('a[@local_opt]) @ local unyielding -> unit = "%ignore" + +let succeeds (x @ local) = overridden x +[%%expect{| +external overridden : local_ ('a [@local_opt]) @ unyielding -> unit + = "%ignore" +val succeeds : local_ 'a -> unit = +|}] + (* [mod global] implies [mod unyielding] by default. *) type ('a : value mod global) u1 diff --git a/typing/ctype.ml b/typing/ctype.ml index e7c88881c1a..b4cbdb74463 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1670,9 +1670,9 @@ let prim_mode' mvar mvar' = function | Primitive.Prim_local, _ -> Locality.allow_right Locality.local, None | Primitive.Prim_poly, _ -> - match mvar with - | Some mvar -> mvar, mvar' - | None -> assert false + match mvar, mvar' with + | Some mvar, Some mvar' -> mvar, Some mvar' + | None, _ | _, None -> assert false (* Exported version. *) let prim_mode mvar prim = diff --git a/typing/ctype.mli b/typing/ctype.mli index b8786be6d5a..6a821525e54 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -222,8 +222,7 @@ val instance_label: _ gen_label_description -> type_expr list * type_expr * type_expr (* Same, for a label *) val prim_mode : - (Mode.allowed * 'r) Mode.Locality.t option - -> (Primitive.mode * Primitive.native_repr) + (Mode.allowed * 'r) Mode.Locality.t option -> (Primitive.mode * Primitive.native_repr) -> (Mode.allowed * 'r) Mode.Locality.t val instance_prim: Primitive.description -> type_expr -> From 017e6f486ef5ef11a5dbee6922b6daf4695ee353 Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Tue, 1 Apr 2025 11:19:11 -0400 Subject: [PATCH 19/20] fix --- typing/ctype.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index b4cbdb74463..5c13de8551e 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1664,19 +1664,20 @@ let instance_label ~fixed lbl = (* CR dkalinichenko: we must vary yieldingness together with locality to get sane behavior around [@local_opt]. Remove once we have mode polymorphism. *) -let prim_mode' mvar mvar' = function +let prim_mode' mvars = function | Primitive.Prim_global, _ -> Locality.allow_right Locality.global, None | Primitive.Prim_local, _ -> Locality.allow_right Locality.local, None | Primitive.Prim_poly, _ -> - match mvar, mvar' with - | Some mvar, Some mvar' -> mvar, Some mvar' - | None, _ | _, None -> assert false + match mvars with + | Some (mvar_l, mvar_y) -> mvar_l, Some mvar_y + | None -> assert false (* Exported version. *) let prim_mode mvar prim = - fst (prim_mode' mvar (Some (Yielding.newvar ())) prim) + let mvars = Option.map (fun mvar_l -> mvar_l, Yielding.newvar ()) mvar in + fst (prim_mode' mvars prim) (** Returns a new mode variable whose locality is the given locality and whose yieldingness is the given yieldingness, while all other axes are @@ -1723,7 +1724,7 @@ let rec instance_prim_locals locals mvar_l mvar_y macc (loc, yld) ty = match locals, get_desc ty with | l :: locals, Tarrow ((lbl,marg,mret),arg,ret,commu) -> let marg = with_locality_and_yielding - (prim_mode' (Some mvar_l) (Some mvar_y) l) marg + (prim_mode' (Some (mvar_l, mvar_y)) l) marg in let macc = Alloc.join [ @@ -1818,7 +1819,7 @@ let instance_prim_mode (desc : Primitive.description) ty = List.exists is_poly desc.prim_native_repr_args then let mode_l = Locality.newvar () in let mode_y = Yielding.newvar () in - let finalret = prim_mode' (Some mode_l) (Some mode_y) desc.prim_native_repr_res in + let finalret = prim_mode' (Some (mode_l, mode_y)) desc.prim_native_repr_res in instance_prim_locals desc.prim_native_repr_args mode_l mode_y (Alloc.disallow_right Alloc.legacy) finalret ty, Some mode_l, Some mode_y From 1bc5a6019cc131b22337417774a32d5f77cf748e Mon Sep 17 00:00:00 2001 From: Diana Kalinichenko Date: Tue, 1 Apr 2025 11:56:04 -0400 Subject: [PATCH 20/20] rebase + accept --- testsuite/tests/typing-layouts/hash_types.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/testsuite/tests/typing-layouts/hash_types.ml b/testsuite/tests/typing-layouts/hash_types.ml index 92ce2dabe16..d2d45261a2a 100644 --- a/testsuite/tests/typing-layouts/hash_types.ml +++ b/testsuite/tests/typing-layouts/hash_types.ml @@ -217,7 +217,7 @@ type r = { i : int ; mutable s : string } type u = r# = #{ i : int ; s : string @@ global many aliased unyielding } [%%expect{| type r = { i : int; mutable s : string; } -type u = r# = #{ i : int; global_ s : string @@ many unyielding aliased; } +type u = r# = #{ i : int; global_ s : string @@ many aliased; } |}] (*******************)