diff --git a/parsing/ast_helper.ml b/parsing/ast_helper.ml index 458c71f2a8a..ed0b340b41a 100644 --- a/parsing/ast_helper.ml +++ b/parsing/ast_helper.ml @@ -142,7 +142,7 @@ module Typ = struct | Default as x -> x | Abbreviation _ as x -> x | Mod (jkind, modes) -> Mod (loop_jkind jkind, modes) - | With (jkind, typ) -> With (loop_jkind jkind, loop typ) + | With (jkind, typ, modalities) -> With (loop_jkind jkind, loop typ, modalities) | Kind_of typ -> Kind_of (loop typ) | Product jkinds -> Product (List.map loop_jkind jkinds) in diff --git a/parsing/ast_iterator.ml b/parsing/ast_iterator.ml index c1ca9b78b48..7311e25864d 100644 --- a/parsing/ast_iterator.ml +++ b/parsing/ast_iterator.ml @@ -842,9 +842,10 @@ let default_iterator = | Mod (t, mode_list) -> this.jkind_annotation this t; this.modes this mode_list - | With (t, ty) -> + | With (t, ty, modalities) -> this.jkind_annotation this t; - this.typ this ty + this.typ this ty; + this.modalities this modalities | Kind_of ty -> this.typ this ty | Product ts -> List.iter (this.jkind_annotation this) ts); diff --git a/parsing/ast_mapper.ml b/parsing/ast_mapper.ml index 0eb886cde2f..b6c25579843 100644 --- a/parsing/ast_mapper.ml +++ b/parsing/ast_mapper.ml @@ -946,8 +946,8 @@ let default_mapper = | Abbreviation (s : string) -> Abbreviation s | Mod (t, mode_list) -> Mod (this.jkind_annotation this t, this.modes this mode_list) - | With (t, ty) -> - With (this.jkind_annotation this t, this.typ this ty) + | With (t, ty, modalities) -> + With (this.jkind_annotation this t, this.typ this ty, this.modalities this modalities) | Kind_of ty -> Kind_of (this.typ this ty) | Product ts -> Product (List.map (this.jkind_annotation this) ts) in diff --git a/parsing/depend.ml b/parsing/depend.ml index be505a8ea9c..ad6a73af9b2 100644 --- a/parsing/depend.ml +++ b/parsing/depend.ml @@ -139,9 +139,9 @@ and add_jkind bv (jkind : jkind_annotation) = | Default -> () | Abbreviation _ -> () | Mod (jkind, (_ : modes)) -> add_jkind bv jkind - | With (jkind, typ) -> + | With (jkind, typ, (_ : modalities)) -> add_jkind bv jkind; - add_type bv typ + add_type bv typ; | Kind_of typ -> add_type bv typ | Product jkinds -> diff --git a/parsing/parser.mly b/parsing/parser.mly index 2201d9f6176..89fbe3c2ea4 100644 --- a/parsing/parser.mly +++ b/parsing/parser.mly @@ -3980,9 +3980,8 @@ jkind_desc: in Mod ($1, modes) } - (* CR layouts v2.8: The types should be separated by AND, not WITH *) - | jkind_annotation WITH core_type { - With ($1, $3) + | jkind_annotation WITH core_type optional_atat_modalities_expr { + With ($1, $3, $4) } | ident { Abbreviation $1 diff --git a/parsing/parsetree.mli b/parsing/parsetree.mli index 90586701508..b3b6958df21 100644 --- a/parsing/parsetree.mli +++ b/parsing/parsetree.mli @@ -1299,7 +1299,7 @@ and jkind_annotation_desc = (* CR layouts v2.8: [mod] can have only layouts on the left, not full kind annotations. We may want to narrow this type some. *) | Mod of jkind_annotation * modes - | With of jkind_annotation * core_type + | With of jkind_annotation * core_type * modalities | Kind_of of core_type | Product of jkind_annotation list diff --git a/parsing/pprintast.ml b/parsing/pprintast.ml index 29d28928904..11777bed4f5 100644 --- a/parsing/pprintast.ml +++ b/parsing/pprintast.ml @@ -463,11 +463,13 @@ and jkind_annotation ?(nested = false) ctxt f k = match k.pjkind_desc with (pp_print_list ~pp_sep:pp_print_space mode) modes ) f (t, modes) end - | With (t, ty) -> - Misc.pp_parens_if nested (fun f (t, ty) -> - pp f "%a with %a" (jkind_annotation ~nested:true ctxt) t (core_type ctxt) - ty - ) f (t, ty) + | With (t, ty, modalities) -> + Misc.pp_parens_if nested (fun f (t, ty, modalities) -> + pp f "%a with %a%a" + (jkind_annotation ~nested:true ctxt) t + (core_type ctxt) ty + optional_space_atat_modalities modalities; + ) f (t, ty, modalities) | Kind_of ty -> pp f "kind_of_ %a" (core_type ctxt) ty | Product ts -> Misc.pp_parens_if nested (fun f ts -> diff --git a/parsing/printast.ml b/parsing/printast.ml index 30caf4f7e23..cb4f26d8d3b 100644 --- a/parsing/printast.ml +++ b/parsing/printast.ml @@ -506,10 +506,11 @@ and jkind_annotation i ppf (jkind : jkind_annotation) = line i ppf "Mod\n"; jkind_annotation (i+1) ppf jkind; modes (i+1) ppf m - | With (jkind, type_) -> + | With (jkind, type_, modalities_) -> line i ppf "With\n"; jkind_annotation (i+1) ppf jkind; - core_type (i+1) ppf type_ + core_type (i+1) ppf type_; + modalities (i+1) ppf modalities_ | Kind_of type_ -> line i ppf "Kind_of\n"; core_type (i+1) ppf type_ diff --git a/printer/printast_with_mappings.ml b/printer/printast_with_mappings.ml index 4ac6d4e0941..d809ef0e4c1 100644 --- a/printer/printast_with_mappings.ml +++ b/printer/printast_with_mappings.ml @@ -532,10 +532,11 @@ and jkind_annotation i ppf (jkind : jkind_annotation) = line i ppf "Mod\n"; jkind_annotation (i+1) ppf jkind; modes (i+1) ppf m - | With (jkind, type_) -> + | With (jkind, type_, modalities) -> line i ppf "With\n"; jkind_annotation (i+1) ppf jkind; - core_type (i+1) ppf type_ + core_type (i+1) ppf type_; + list i modality ppf modalities | Kind_of type_ -> line i ppf "Kind_of\n"; core_type (i+1) ppf type_ diff --git a/testsuite/tests/language-extensions/pprintast_unconditional.ml b/testsuite/tests/language-extensions/pprintast_unconditional.ml index b484b48f615..6818946187f 100644 --- a/testsuite/tests/language-extensions/pprintast_unconditional.ml +++ b/testsuite/tests/language-extensions/pprintast_unconditional.ml @@ -17,6 +17,7 @@ let () = Language_extension.set_universe_and_enable_all module Example = struct open Parsetree open Parse + open Asttypes open struct let loc = Location.none let located = Location.mknoloc @@ -31,6 +32,10 @@ module Example = struct let structure = parse implementation "include functor F" let module_expr = parse module_expr "struct include functor F end" let toplevel_phrase = parse toplevel_phrase "#2.17;;" + let modality = { txt = Modality "uncontended" + ; loc + } + let modalities = [ modality ] let class_field = { pcf_desc = Pcf_initializer expression ; pcf_loc = loc ; pcf_attributes = [] @@ -98,7 +103,9 @@ module Example = struct ( { pjkind_loc = loc; pjkind_desc = Abbreviation "value"; } - , core_type ); + , core_type + , modalities + ); } let mode = { Location.txt = (Parsetree.Mode "global"); loc } diff --git a/testsuite/tests/language-extensions/pprintast_unconditional.reference b/testsuite/tests/language-extensions/pprintast_unconditional.reference index 59b382542f2..9216435dc9f 100644 --- a/testsuite/tests/language-extensions/pprintast_unconditional.reference +++ b/testsuite/tests/language-extensions/pprintast_unconditional.reference @@ -57,7 +57,7 @@ tyvar_of_name: 'no_tyvars_require_extensions tyvar: 'no_tyvars_require_extensions -jkind: value with local_ ('a : value) -> unit +jkind: value with local_ ('a : value) -> unit @@ uncontended mode: global @@ -122,7 +122,7 @@ tyvar_of_name: 'no_tyvars_require_extensions tyvar: 'no_tyvars_require_extensions -jkind: value with local_ ('a : value) -> unit +jkind: value with local_ ('a : value) -> unit @@ uncontended mode: global diff --git a/testsuite/tests/parsetree/source_jane_street.ml b/testsuite/tests/parsetree/source_jane_street.ml index e97e84f6dab..7435421b81f 100644 --- a/testsuite/tests/parsetree/source_jane_street.ml +++ b/testsuite/tests/parsetree/source_jane_street.ml @@ -1109,9 +1109,31 @@ val inc : 'a with_idx -> 'a with_idx = (***************) (* Modal kinds *) +(* supported *) +type 'a list : immutable_data with 'a +type ('a, 'b) either : immutable_data with 'a * 'b +type 'a contended : immutable_data with 'a @@ contended +type 'a contended_with_int : immutable_data with 'a @@ contended with int + +[%%expect{| +type 'a list + : value mod many with 'a uncontended with 'a portable with 'a + unyielding with 'a +type ('a, 'b) either + : value mod many with 'a * 'b uncontended with 'a * 'b + portable with 'a * 'b unyielding with 'a * 'b +type 'a contended + : value mod many with 'a uncontended portable with 'a unyielding with 'a +type 'a contended_with_int + : value mod many with int +'a uncontended with int portable with int +'a + unyielding with int +'a +|}] + +(* not yet supported *) module _ : sig - type 'a list : immutable_data with 'a - type ('a, 'b) either : immutable_data with 'a * 'b type 'a gel : kind_of_ 'a mod global type 'a t : _ kind_abbrev_ immediate = value mod global unique many sync uncontended @@ -1119,8 +1141,6 @@ module _ : sig kind_abbrev_ immutable = value mod uncontended kind_abbrev_ data = value mod sync many end = struct - type 'a list : immutable_data with 'a - type ('a, 'b) either : immutable_data with 'a * 'b type 'a gel : kind_of_ 'a mod global type 'a t : _ kind_abbrev_ immediate = value mod global unique many sync uncontended @@ -1133,9 +1153,9 @@ end supported. *) [%%expect{| -Line 13, characters 16-27: -13 | type 'a gel : kind_of_ 'a mod global - ^^^^^^^^^^^ +Line 9, characters 16-27: +9 | type 'a gel : kind_of_ 'a mod global + ^^^^^^^^^^^ Error: Unimplemented kind syntax |}] diff --git a/testsuite/tests/typing-jkind-bounds/basics.ml b/testsuite/tests/typing-jkind-bounds/basics.ml index c2273f8b5a6..bec24c2cb64 100644 --- a/testsuite/tests/typing-jkind-bounds/basics.ml +++ b/testsuite/tests/typing-jkind-bounds/basics.ml @@ -1212,16 +1212,21 @@ Error: The kind of type "t" is value mod external_ (* CR layouts v2.8: this should be accepted *) type 'a t : value mod many = { x : 'a @@ many } -type 'a t : value mod uncontended = { x : 'a @@ uncontended } +type 'a t : value mod uncontended = { x : 'a @@ contended } type 'a t : value mod portable = { x : 'a @@ portable } [%%expect {| -Line 1, characters 0-47: -1 | type 'a t : value mod many = { x : 'a @@ many } - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The kind of type "t" is immutable_data - because it's a boxed record type. - But the kind of type "t" must be a subkind of value mod many - because of the annotation on the declaration of the type t. +type 'a t = { x : 'a @@ many; } +type 'a t = { x : 'a @@ contended; } +type 'a t = { x : 'a @@ portable; } +|}] + +type 'a t : immutable_data with 'a @@ many = { x : 'a @@ many } +type 'a t : immutable_data with 'a @@ contended = { x : 'a @@ contended } +type 'a t : immutable_data with 'a @@ portable = { x : 'a @@ portable } +[%%expect{| +type 'a t = { x : 'a @@ many; } +type 'a t = { x : 'a @@ contended; } +type 'a t = { x : 'a @@ portable; } |}] type 'a t : value mod unique = { x : 'a @@ unique } diff --git a/testsuite/tests/typing-jkind-bounds/modalities.ml b/testsuite/tests/typing-jkind-bounds/modalities.ml new file mode 100644 index 00000000000..44671c9f519 --- /dev/null +++ b/testsuite/tests/typing-jkind-bounds/modalities.ml @@ -0,0 +1,187 @@ +(* TEST + flags = "-extension layouts_alpha -infer-with-bounds"; + expect; +*) +let use_uncontended : 'a @ uncontended -> unit = fun _ -> () +let use_portable : 'a @ portable -> unit = fun _ -> () +let cross_uncontended : ('a : value mod uncontended) -> unit = fun _ -> () +type ('a : value mod uncontended) require_uncontended +[%%expect{| +val use_uncontended : 'a -> unit = +val use_portable : 'a @ portable -> unit = +val cross_uncontended : ('a : value mod uncontended). 'a -> unit = +type ('a : value mod uncontended) require_uncontended +|}] + +type 'a t = { contended : 'a @@ contended } +[%%expect{| +type 'a t = { contended : 'a @@ contended; } +|}] + +type t_test = int t require_uncontended +type t_test = int ref t require_uncontended +[%%expect{| +type t_test = int t require_uncontended +type t_test = int ref t require_uncontended +|}] + +let foo (t : int ref t @@ contended) = use_uncontended t +[%%expect{| +val foo : int ref t @ contended -> unit = +|}] + +let foo (t : int ref t @@ contended) = use_uncontended t.contended +[%%expect{| +Line 1, characters 55-66: +1 | let foo (t : int ref t @@ contended) = use_uncontended t.contended + ^^^^^^^^^^^ +Error: This value is "contended" but expected to be "uncontended". +|}] + +let foo (t : int ref t @@ contended) = cross_uncontended t +[%%expect{| +val foo : int ref t @ contended -> unit = +|}] + +let foo (t : int t @@ nonportable) = use_portable t +[%%expect{| +val foo : int t -> unit = +|}] + +let foo (t : _ t @@ nonportable) = use_portable t +[%%expect{| +Line 1, characters 48-49: +1 | let foo (t : _ t @@ nonportable) = use_portable t + ^ +Error: This value is "nonportable" but expected to be "portable". +|}] + +type 'a t : immutable_data with 'a @@ many = { x : 'a @@ many } +type 'a t : immutable_data with 'a @@ contended = { x : 'a @@ contended } +type 'a t : immutable_data with 'a @@ portable = { x : 'a @@ portable } +[%%expect{| +type 'a t = { x : 'a @@ many; } +type 'a t = { x : 'a @@ contended; } +type 'a t = { x : 'a @@ portable; } +|}] + +let use_global : ('a : value & value). 'a @ global -> unit = fun _ -> () +let cross_global : ('a : value & value mod global). 'a -> unit = fun _ -> () +let use_portable : ('a : value & value). 'a @ portable -> unit = fun _ -> () +type 'a t = #{ x : 'a @@ global; y : 'a @@ global } + +[%%expect{| +val use_global : ('a : value & value). 'a -> unit = +val cross_global : ('a : value mod global & value mod global). 'a -> unit = + +val use_portable : ('a : value & value). 'a @ portable -> unit = +type 'a t = #{ global_ x : 'a; global_ y : 'a; } +|}] + +let foo (t : string t @@ local) = use_global t + +[%%expect{| +val foo : local_ string t -> unit = +|}] + +let foo (t : string t @@ local) = cross_global t + +[%%expect{| +val foo : local_ string t -> unit = +|}, Principal{| +Line 1, characters 47-48: +1 | let foo (t : string t @@ local) = cross_global t + ^ +Error: This expression has type "string t" + but an expression was expected of type + "('a : value mod global & value mod global)" + The kind of string t is + value_or_null mod global unique with string +string + many with string +string + uncontended with string +string + portable with string +string + unyielding with string +string + external_ with string +string + non_null with string +string + & value_or_null mod global unique with string +string + many with string +string + uncontended with string +string + portable with string +string + unyielding with string +string + external_ with string +string + non_null with string +string + because of the definition of t at line 4, characters 0-51. + But the kind of string t must be a subkind of + value mod global & value mod global + because of the definition of cross_global at line 2, characters 4-16. +|}] + +let foo (t : string t @@ nonportable) = use_portable t + +[%%expect{| +val foo : string t -> unit = +|}] + +let foo (t : (string -> string) t @@ nonportable) = use_portable t + +[%%expect{| +Line 1, characters 65-66: +1 | let foo (t : (string -> string) t @@ nonportable) = use_portable t + ^ +Error: This value is "nonportable" but expected to be "portable". +|}, Principal{| +Line 1, characters 65-66: +1 | let foo (t : (string -> string) t @@ nonportable) = use_portable t + ^ +Error: This expression has type "(string -> string) t" + but an expression was expected of type "('a : value & value)" + The kind of (string -> string) t is + value_or_null mod global + unique with string -> string +string -> string + many with string -> string +string -> string + uncontended with string -> string +string -> string + portable with string -> string +string -> string + unyielding with string -> string +string -> string + external_ with string -> string +string -> string + non_null with string -> string +string -> string + & value_or_null mod global + unique with string -> string +string -> string + many with string -> string +string -> string + uncontended with string -> string +string -> string + portable with string -> string +string -> string + unyielding with string -> string +string -> string + external_ with string -> string +string -> string + non_null with string -> string +string -> string + because of the definition of t at line 4, characters 0-51. + But the kind of (string -> string) t must be a subkind of + value & value + because of the definition of use_portable at line 3, characters 4-16. +|}] diff --git a/testsuite/tests/typing-jkind-bounds/predef.ml b/testsuite/tests/typing-jkind-bounds/predef.ml index 2854e5e5630..508462c94a3 100644 --- a/testsuite/tests/typing-jkind-bounds/predef.ml +++ b/testsuite/tests/typing-jkind-bounds/predef.ml @@ -133,7 +133,7 @@ Error: This value escapes its region. (* ref *) type t : mutable_data = int ref -type 'a t : mutable_data with 'a = 'a ref +type 'a t : mutable_data with 'a @@ global many = 'a ref type ('a : mutable_data) t : mutable_data = 'a list [%%expect {| type t = int ref diff --git a/testsuite/tests/typing-jkind-bounds/with_basics.ml b/testsuite/tests/typing-jkind-bounds/with_basics.ml index 2988b925169..d86ba5a14a0 100644 --- a/testsuite/tests/typing-jkind-bounds/with_basics.ml +++ b/testsuite/tests/typing-jkind-bounds/with_basics.ml @@ -155,7 +155,7 @@ Line 2, characters 15-16: Error: This value is "nonportable" but expected to be "portable". |}] -let foo (t : ('a -> 'a) ref option @@ once) = +let foo (t : ('a -> 'a ref) option @@ once) = use_many t [%%expect{| @@ -427,7 +427,7 @@ Line 2, characters 15-16: Error: This value is "nonportable" but expected to be "portable". |}] -let foo (t : ('a -> 'a) ref list @@ once) = +let foo (t : ('a -> 'a ref) list @@ once) = use_many t [%%expect{| diff --git a/testsuite/tests/typing-modes/portable-contend.ml b/testsuite/tests/typing-modes/portable-contend.ml index 58889a57977..8b7aedc6bcb 100644 --- a/testsuite/tests/typing-modes/portable-contend.ml +++ b/testsuite/tests/typing-modes/portable-contend.ml @@ -364,13 +364,16 @@ val foo : int @ shared -> unit = (* TESTING immutable array *) module Iarray = Stdlib_stable.Iarray -let foo (r @ contended) = Iarray.get r 42 -(* CR zqian: The following should pass; the modal kind system should mode cross -iarray depending on the type of its element. *) +let foo (r : int iarray @@ contended) = Iarray.get r 42 [%%expect{| module Iarray = Stdlib_stable.Iarray -Line 3, characters 37-38: -3 | let foo (r @ contended) = Iarray.get r 42 +val foo : int iarray @ contended -> int = +|}] + +let foo (r @ contended) = Iarray.get r 42 +[%%expect{| +Line 1, characters 37-38: +1 | let foo (r @ contended) = Iarray.get r 42 ^ Error: This value is "contended" but expected to be "uncontended". |}] diff --git a/typing/ctype.ml b/typing/ctype.ml index e803275fdd6..748ae5468f1 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -2200,10 +2200,17 @@ let rec estimate_type_jkind ~expand_component env ty = | Tarrow _ -> Jkind.for_arrow | Ttuple _ -> Jkind.Builtin.value ~why:Tuple | Tunboxed_tuple ltys -> - let tys = List.map (fun (_, ty) -> expand_component ty) ltys in + let tys_modalities = + List.map (fun (_, ty) -> expand_component ty, + Mode.Modality.Value.Const.id) ltys + in (* CR layouts v2.8: This pretty ridiculous use of [estimate_type_jkind] just to throw most of it away will go away once we get [layout_of]. *) - let jkinds = List.map (estimate_type_jkind ~expand_component env) tys in + let jkinds = + List.map + (fun (ty, _) -> estimate_type_jkind ~expand_component env ty) + tys_modalities + in let layouts = List.map Jkind.extract_layout jkinds in Jkind.Builtin.product ~jkind_of_type:(estimate_type_jkind ~expand_component env) @@ -2213,7 +2220,7 @@ let rec estimate_type_jkind ~expand_component env ty = | _ -> Misc.fatal_error "Ctype.estimate_type_jkind: use of jkind_of_first_type \ with more than 1 type") - ~why:Unboxed_tuple tys layouts + ~why:Unboxed_tuple tys_modalities layouts | Tconstr (p, args, _) -> begin try let type_decl = Env.find_type p env in let jkind = type_decl.type_jkind in diff --git a/typing/jkind.ml b/typing/jkind.ml index be21a88c670..e67c4d7424c 100644 --- a/typing/jkind.ml +++ b/typing/jkind.ml @@ -630,12 +630,13 @@ module Bounds = struct } ~combine:Misc.Le_result.combine bounds1 bounds2 - let add_baggage ~deep_only ~baggage bounds = + let add_baggage ~modality ~deep_only ~baggage bounds = (* Add the type as a baggage type along all deep axes *) Map.f { f = (fun ~axis (bound : _ Bound.t) : _ Bound.t -> - if Axis.is_modal axis || not deep_only + if (not (Jkind_axis.Axis.modality_is_const_for_axis axis modality)) + && (Axis.is_modal axis || not deep_only) then Bound.add_baggage bound ~axis baggage else bound) } @@ -1094,15 +1095,19 @@ module Const = struct List.map (of_user_written_annotation_unchecked_level context) ts in jkind_of_product_annotations jkinds - | With (base, type_) -> ( + | With (base, type_, modalities) -> ( let base = of_user_written_annotation_unchecked_level context base in match context with | Right_jkind _ -> raise ~loc:type_.ptyp_loc With_on_right | Left_jkind (transl_type, _) -> let type_ = transl_type type_ in + let modality = + Typemode.transl_modalities ~maturity:Stable Immutable [] modalities + in { layout = base.layout; upper_bounds = - Bounds.add_baggage ~deep_only:true ~baggage:type_ base.upper_bounds + Bounds.add_baggage ~modality ~deep_only:true ~baggage:type_ + base.upper_bounds }) | Default | Kind_of _ -> raise ~loc:jkind.pjkind_loc Unimplemented_syntax @@ -1180,9 +1185,10 @@ module Jkind_desc = struct let unsafely_set_upper_bounds t ~from = { t with upper_bounds = from.upper_bounds } - let add_baggage ~deep_only ~baggage t = + let add_baggage ~deep_only ~baggage ~modality t = { t with - upper_bounds = Bounds.add_baggage ~deep_only ~baggage t.upper_bounds + upper_bounds = + Bounds.add_baggage ~deep_only ~baggage ~modality t.upper_bounds } let max = of_const Const.max @@ -1227,7 +1233,7 @@ module Jkind_desc = struct let immediate = of_const Const.Builtin.immediate.jkind end - let product ~jkind_of_first_type ~jkind_of_type tys layouts = + let product ~jkind_of_first_type ~jkind_of_type tys_modalities layouts = (* CR layouts v2.8: We can probably drop this special case once we have proper subsumption. The general algorithm gets the right jkind, but the subsumption check fails because it can't recognize @@ -1240,14 +1246,14 @@ module Jkind_desc = struct let layout = Layout.product layouts in let upper_bounds = List.fold_right - (fun ty bounds -> - Bounds.add_baggage ~deep_only:false ~baggage:ty bounds) - tys + (fun (ty, modality) bounds -> + Bounds.add_baggage ~deep_only:false ~baggage:ty bounds ~modality) + tys_modalities (Bounds.min |> Bounds.disallow_right) in { layout; upper_bounds } else - let folder (layouts, bounds) ty = + let folder (layouts, bounds) (ty, _) = let { jkind = { layout; upper_bounds }; annotation = _; history = _; @@ -1258,7 +1264,9 @@ module Jkind_desc = struct layout :: layouts, Bounds.join bounds upper_bounds in let layouts, upper_bounds = - List.fold_left folder ([], Bounds.min |> Bounds.disallow_right) tys + List.fold_left folder + ([], Bounds.min |> Bounds.disallow_right) + tys_modalities in let layouts = List.rev layouts in { layout = Layout.Product layouts; @@ -1338,9 +1346,10 @@ module Builtin = struct fresh_jkind Jkind_desc.Builtin.immediate ~annotation:(mk_annot "immediate") ~why:(Immediate_creation why) - let product ~jkind_of_first_type ~jkind_of_type ~why tys layouts = + let product ~jkind_of_first_type ~jkind_of_type ~why tys_modalities layouts = let desc = - Jkind_desc.product ~jkind_of_first_type ~jkind_of_type tys layouts + Jkind_desc.product ~jkind_of_first_type ~jkind_of_type tys_modalities + layouts in fresh_jkind_poly desc ~annotation:None ~why:(Product_creation why) @@ -1363,8 +1372,10 @@ let unsafely_set_upper_bounds ~from t = jkind = Jkind_desc.unsafely_set_upper_bounds t.jkind ~from:from.jkind } -let add_baggage ~baggage t = - { t with jkind = Jkind_desc.add_baggage ~deep_only:true ~baggage t.jkind } +let add_baggage ~modality ~baggage t = + { t with + jkind = Jkind_desc.add_baggage ~deep_only:true ~baggage ~modality t.jkind + } let has_baggage t = Bounds.has_baggage t.jkind.upper_bounds @@ -1455,10 +1466,10 @@ let all_void_labels lbls = let add_labels_as_baggage lbls jkind = List.fold_right - (fun (lbl : Types.label_declaration) -> add_baggage ~baggage:lbl.ld_type) + (fun (lbl : Types.label_declaration) -> + add_baggage ~baggage:lbl.ld_type ~modality:lbl.ld_modalities) lbls jkind -(* CR layouts v2.8: This should take modalities into account. *) let for_boxed_record lbls = if all_void_labels lbls then Builtin.immediate ~why:Empty_record @@ -1472,17 +1483,18 @@ let for_boxed_record lbls = add_labels_as_baggage lbls base else Builtin.value ~why:Boxed_record -(* CR layouts v2.8: This should take modalities into account. *) let for_unboxed_record ~jkind_of_first_type ~jkind_of_type lbls = let open Types in - let tys = List.map (fun lbl -> lbl.ld_type) lbls in + let tys_modalities = + List.map (fun lbl -> lbl.ld_type, lbl.ld_modalities) lbls + in let layouts = List.map (fun lbl -> lbl.ld_sort |> Layout.Const.of_sort_const |> Layout.of_const) lbls in - Builtin.product ~jkind_of_first_type ~jkind_of_type ~why:Unboxed_record tys - layouts + Builtin.product ~jkind_of_first_type ~jkind_of_type ~why:Unboxed_record + tys_modalities layouts (* CR layouts v2.8: This should take modalities into account. *) let for_boxed_variant cstrs = @@ -1524,7 +1536,8 @@ let for_boxed_variant cstrs = match cstr.cd_args with | Cstr_tuple args -> List.fold_right - (fun arg -> add_baggage ~baggage:arg.ca_type) + (fun arg -> + add_baggage ~modality:arg.ca_modalities ~baggage:arg.ca_type) args jkind | Cstr_record lbls -> add_labels_as_baggage lbls jkind in @@ -1598,22 +1611,22 @@ let extract_layout jk = jk.jkind.layout let get_modal_upper_bounds ~type_equal ~jkind_of_type jk : Alloc.Const.t = let bounds = jk.jkind.upper_bounds in { areality = - Bound.reduce ~axis:(Modal Locality) ~type_equal ~jkind_of_type + Bound.reduce ~axis:(Modal (Comonadic Areality)) ~type_equal ~jkind_of_type bounds.locality; linearity = - Bound.reduce ~axis:(Modal Linearity) ~type_equal ~jkind_of_type - bounds.linearity; + Bound.reduce ~axis:(Modal (Comonadic Linearity)) ~type_equal + ~jkind_of_type bounds.linearity; uniqueness = - Bound.reduce ~axis:(Modal Uniqueness) ~type_equal ~jkind_of_type + Bound.reduce ~axis:(Modal (Monadic Uniqueness)) ~type_equal ~jkind_of_type bounds.uniqueness; portability = - Bound.reduce ~axis:(Modal Portability) ~type_equal ~jkind_of_type - bounds.portability; + Bound.reduce ~axis:(Modal (Comonadic Portability)) ~type_equal + ~jkind_of_type bounds.portability; contention = - Bound.reduce ~axis:(Modal Contention) ~type_equal ~jkind_of_type + Bound.reduce ~axis:(Modal (Monadic Contention)) ~type_equal ~jkind_of_type bounds.contention; yielding = - Bound.reduce ~axis:(Modal Yielding) ~type_equal ~jkind_of_type + Bound.reduce ~axis:(Modal (Comonadic Yielding)) ~type_equal ~jkind_of_type bounds.yielding } diff --git a/typing/jkind.mli b/typing/jkind.mli index 5f92885303a..bb01a81138a 100644 --- a/typing/jkind.mli +++ b/typing/jkind.mli @@ -316,7 +316,7 @@ module Builtin : sig jkind_of_first_type:(unit -> jkind_l) -> jkind_of_type:(Types.type_expr -> jkind_l) -> why:History.product_creation_reason -> - Types.type_expr list -> + (Types.type_expr * Mode.Modality.Value.Const.t) list -> Sort.t Layout.t list -> jkind_l @@ -333,8 +333,12 @@ val add_nullability_crossing : 'd t -> 'd t [from]. *) val unsafely_set_upper_bounds : from:'d t -> 'd t -> 'd t -(** Take an existing [t] and add some baggage. *) -val add_baggage : baggage:Types.type_expr -> jkind_l -> jkind_l +(** Take an existing [jkind_l] and add some baggage. *) +val add_baggage : + modality:Mode.Modality.Value.Const.t -> + baggage:Types.type_expr -> + jkind_l -> + jkind_l (** Does this jkind have baggage? *) val has_baggage : jkind_l -> bool diff --git a/typing/jkind_axis.ml b/typing/jkind_axis.ml index efce3cb455f..9f8dfe52b38 100644 --- a/typing/jkind_axis.ml +++ b/typing/jkind_axis.ml @@ -115,16 +115,6 @@ module Nullability = struct end module Axis = struct - module Modal = struct - type 'a t = - | Locality : Mode.Locality.Const.t t - | Linearity : Mode.Linearity.Const.t t - | Uniqueness : Mode.Uniqueness.Const.t t - | Portability : Mode.Portability.Const.t t - | Contention : Mode.Contention.Const.t t - | Yielding : Mode.Yielding.Const.t t - end - module Nonmodal = struct type 'a t = | Externality : Externality.t t @@ -132,60 +122,70 @@ module Axis = struct end type 'a t = - | Modal of 'a Modal.t - | Nonmodal of 'a Nonmodal.t + | Modal : ('m, 'a, 'd) Mode.Alloc.axis -> 'a t + | Nonmodal : 'a Nonmodal.t -> 'a t type packed = Pack : 'a t -> packed - module Accent_lattice (M : Mode_intf.Lattice) : Axis_ops with type t = M.t = - struct + module Accent_lattice (M : Mode_intf.Lattice) = struct (* A functor to add some convenient functions to modal axes *) include M - let less_or_equal a b = Misc.Le_result.less_or_equal ~le a b + let less_or_equal a b : Misc.Le_result.t = + match le a b, le b a with + | true, true -> Equal + | true, false -> Less + | false, _ -> Not_le - let equal a b = Misc.Le_result.equal ~le a b + let equal a b = Misc.Le_result.is_equal (less_or_equal a b) end let get (type a) : a t -> (module Axis_ops with type t = a) = function - | Modal Locality -> (module Accent_lattice (Mode.Locality.Const)) - | Modal Linearity -> (module Accent_lattice (Mode.Linearity.Const)) - | Modal Uniqueness -> (module Accent_lattice (Mode.Uniqueness.Const)) - | Modal Portability -> (module Accent_lattice (Mode.Portability.Const)) - | Modal Contention -> (module Accent_lattice (Mode.Contention.Const)) - | Modal Yielding -> (module Accent_lattice (Mode.Yielding.Const)) + | Modal axis -> + (module Accent_lattice ((val Mode.Alloc.lattice_of_axis axis))) | Nonmodal Externality -> (module Externality) | Nonmodal Nullability -> (module Nullability) let all = - [ Pack (Modal Locality); - Pack (Modal Uniqueness); - Pack (Modal Linearity); - Pack (Modal Contention); - Pack (Modal Portability); - Pack (Modal Yielding); + [ Pack (Modal (Comonadic Areality)); + Pack (Modal (Monadic Uniqueness)); + Pack (Modal (Comonadic Linearity)); + Pack (Modal (Monadic Contention)); + Pack (Modal (Comonadic Portability)); + Pack (Modal (Comonadic Yielding)); Pack (Nonmodal Externality); Pack (Nonmodal Nullability) ] let name (type a) : a t -> string = function - | Modal Locality -> "locality" - | Modal Linearity -> "linearity" - | Modal Uniqueness -> "uniqueness" - | Modal Portability -> "portability" - | Modal Contention -> "contention" - | Modal Yielding -> "yielding" + | Modal axis -> Format.asprintf "%a" Mode.Alloc.print_axis axis | Nonmodal Externality -> "externality" | Nonmodal Nullability -> "nullability" let is_modal (type a) : a t -> bool = function - | Modal Locality -> true - | Modal Linearity -> true - | Modal Uniqueness -> true - | Modal Portability -> true - | Modal Contention -> true - | Modal Yielding -> true + | Modal (Comonadic Areality) -> true + | Modal (Comonadic Linearity) -> true + | Modal (Monadic Uniqueness) -> true + | Modal (Comonadic Portability) -> true + | Modal (Monadic Contention) -> true + | Modal (Comonadic Yielding) -> true | Nonmodal Externality -> true | Nonmodal Nullability -> false + + let modality_is_const_for_axis (type a) (t : a t) + (modality : Mode.Modality.Value.Const.t) = + match t with + | Nonmodal Nullability | Nonmodal Externality -> false + | Modal axis -> + let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in + let modality = Mode.Modality.Value.Const.proj axis modality in + if Mode.Modality.is_constant modality + then true + else if Mode.Modality.is_id modality + then false + else + Misc.fatal_error + "Don't yet know how to interpret non-constant, non-identity \ + modalities" end module type Axed = sig @@ -207,23 +207,23 @@ module Axis_collection (T : Axed) = struct let get (type a) ~(axis : a Axis.t) values : (_, _, a) T.t = match axis with - | Modal Locality -> values.locality - | Modal Linearity -> values.linearity - | Modal Uniqueness -> values.uniqueness - | Modal Portability -> values.portability - | Modal Contention -> values.contention - | Modal Yielding -> values.yielding + | Modal (Comonadic Areality) -> values.locality + | Modal (Comonadic Linearity) -> values.linearity + | Modal (Monadic Uniqueness) -> values.uniqueness + | Modal (Comonadic Portability) -> values.portability + | Modal (Monadic Contention) -> values.contention + | Modal (Comonadic Yielding) -> values.yielding | Nonmodal Externality -> values.externality | Nonmodal Nullability -> values.nullability let set (type a) ~(axis : a Axis.t) values (value : (_, _, a) T.t) = match axis with - | Modal Locality -> { values with locality = value } - | Modal Linearity -> { values with linearity = value } - | Modal Uniqueness -> { values with uniqueness = value } - | Modal Portability -> { values with portability = value } - | Modal Contention -> { values with contention = value } - | Modal Yielding -> { values with yielding = value } + | Modal (Comonadic Areality) -> { values with locality = value } + | Modal (Comonadic Linearity) -> { values with linearity = value } + | Modal (Monadic Uniqueness) -> { values with uniqueness = value } + | Modal (Comonadic Portability) -> { values with portability = value } + | Modal (Monadic Contention) -> { values with contention = value } + | Modal (Comonadic Yielding) -> { values with yielding = value } | Nonmodal Externality -> { values with externality = value } | Nonmodal Nullability -> { values with nullability = value } @@ -237,12 +237,12 @@ module Axis_collection (T : Axed) = struct let[@inline] f { f } = let open M.Syntax in - let* locality = f ~axis:Axis.(Modal Locality) in - let* uniqueness = f ~axis:Axis.(Modal Uniqueness) in - let* linearity = f ~axis:Axis.(Modal Linearity) in - let* contention = f ~axis:Axis.(Modal Contention) in - let* portability = f ~axis:Axis.(Modal Portability) in - let* yielding = f ~axis:Axis.(Modal Yielding) in + let* locality = f ~axis:Axis.(Modal (Comonadic Areality)) in + let* uniqueness = f ~axis:Axis.(Modal (Monadic Uniqueness)) in + let* linearity = f ~axis:Axis.(Modal (Comonadic Linearity)) in + let* contention = f ~axis:Axis.(Modal (Monadic Contention)) in + let* portability = f ~axis:Axis.(Modal (Comonadic Portability)) in + let* yielding = f ~axis:Axis.(Modal (Comonadic Yielding)) in let* externality = f ~axis:Axis.(Nonmodal Externality) in let* nullability = f ~axis:Axis.(Nonmodal Nullability) in M.return @@ -333,12 +333,12 @@ module Axis_collection (T : Axed) = struct externality; nullability } ~combine = - combine (f ~axis:Axis.(Modal Locality) locality) - @@ combine (f ~axis:Axis.(Modal Uniqueness) uniqueness) - @@ combine (f ~axis:Axis.(Modal Linearity) linearity) - @@ combine (f ~axis:Axis.(Modal Contention) contention) - @@ combine (f ~axis:Axis.(Modal Portability) portability) - @@ combine (f ~axis:Axis.(Modal Yielding) yielding) + combine (f ~axis:Axis.(Modal (Comonadic Areality)) locality) + @@ combine (f ~axis:Axis.(Modal (Monadic Uniqueness)) uniqueness) + @@ combine (f ~axis:Axis.(Modal (Comonadic Linearity)) linearity) + @@ combine (f ~axis:Axis.(Modal (Monadic Contention)) contention) + @@ combine (f ~axis:Axis.(Modal (Comonadic Portability)) portability) + @@ combine (f ~axis:Axis.(Modal (Comonadic Yielding)) yielding) @@ combine (f ~axis:Axis.(Nonmodal Externality) externality) @@ f ~axis:Axis.(Nonmodal Nullability) nullability end @@ -373,12 +373,12 @@ module Axis_collection (T : Axed) = struct externality = ext2; nullability = nul2 } ~combine = - combine (f ~axis:Axis.(Modal Locality) loc1 loc2) - @@ combine (f ~axis:Axis.(Modal Uniqueness) uni1 uni2) - @@ combine (f ~axis:Axis.(Modal Linearity) lin1 lin2) - @@ combine (f ~axis:Axis.(Modal Contention) con1 con2) - @@ combine (f ~axis:Axis.(Modal Portability) por1 por2) - @@ combine (f ~axis:Axis.(Modal Yielding) yie1 yie2) + combine (f ~axis:Axis.(Modal (Comonadic Areality)) loc1 loc2) + @@ combine (f ~axis:Axis.(Modal (Monadic Uniqueness)) uni1 uni2) + @@ combine (f ~axis:Axis.(Modal (Comonadic Linearity)) lin1 lin2) + @@ combine (f ~axis:Axis.(Modal (Monadic Contention)) con1 con2) + @@ combine (f ~axis:Axis.(Modal (Comonadic Portability)) por1 por2) + @@ combine (f ~axis:Axis.(Modal (Comonadic Yielding)) yie1 yie2) @@ combine (f ~axis:Axis.(Nonmodal Externality) ext1 ext2) @@ f ~axis:Axis.(Nonmodal Nullability) nul1 nul2 end diff --git a/typing/jkind_axis.mli b/typing/jkind_axis.mli index e3c50c9dc34..fb6036f527b 100644 --- a/typing/jkind_axis.mli +++ b/typing/jkind_axis.mli @@ -41,17 +41,6 @@ module Nullability : sig end module Axis : sig - (* CR zqian: remove this and use [Mode.Alloc.axis] instead *) - module Modal : sig - type 'a t = - | Locality : Mode.Locality.Const.t t - | Linearity : Mode.Linearity.Const.t t - | Uniqueness : Mode.Uniqueness.Const.t t - | Portability : Mode.Portability.Const.t t - | Contention : Mode.Contention.Const.t t - | Yielding : Mode.Yielding.Const.t t - end - module Nonmodal : sig type 'a t = | Externality : Externality.t t @@ -60,8 +49,8 @@ module Axis : sig (** Represents an axis of a jkind *) type 'a t = - | Modal of 'a Modal.t - | Nonmodal of 'a Nonmodal.t + | Modal : ('m, 'a, 'd) Mode.Alloc.axis -> 'a t + | Nonmodal : 'a Nonmodal.t -> 'a t type packed = Pack : 'a t -> packed @@ -77,6 +66,10 @@ module Axis : sig (** Is this a modal axis? Includes externality, because that will one day be modal (it is a deep property). *) val is_modal : _ t -> bool + + (* CR layouts v2.8: Not sure this belongs here, but there's not another obvious spot. Once this + file is more aligned with axis treatment in mode.ml, possibly re-home this. *) + val modality_is_const_for_axis : _ t -> Mode.Modality.Value.Const.t -> bool end (** [Axed] describes a type that is parameterized by axis. *) diff --git a/typing/mode.ml b/typing/mode.ml index 1f6030eb508..71a318ab694 100644 --- a/typing/mode.ml +++ b/typing/mode.ml @@ -607,7 +607,7 @@ module Lattices_mono = struct let print : type p r. _ -> (p, r) t -> unit = fun ppf -> function - | Areality -> Format.fprintf ppf "areality" + | Areality -> Format.fprintf ppf "locality" | Linearity -> Format.fprintf ppf "linearity" | Portability -> Format.fprintf ppf "portability" | Uniqueness -> Format.fprintf ppf "uniqueness" @@ -1631,6 +1631,14 @@ module Comonadic_with (Areality : Areality) = struct let print_axis ax ppf a = let obj = proj_obj ax in C.print obj ppf a + + let lattice_of_axis (type a) (axis : (t, a) Axis.t) : + (module Lattice with type t = a) = + match axis with + | Areality -> (module Areality.Const) + | Linearity -> (module Linearity.Const) + | Portability -> (module Portability.Const) + | Yielding -> (module Yielding.Const) end let proj ax m = Solver.via_monotone (proj_obj ax) (Proj (Obj.obj, ax)) m @@ -1729,6 +1737,12 @@ module Monadic = struct let le_axis ax a b = let obj = proj_obj ax in C.le obj b a + + let lattice_of_axis (type a) (axis : (t, a) Axis.t) : + (module Lattice with type t = a) = + match axis with + | Uniqueness -> (module Uniqueness.Const) + | Contention -> (module Contention.Const) end let proj ax m = Solver.via_monotone (proj_obj ax) (Proj (Obj.obj, ax)) m @@ -1805,6 +1819,19 @@ module Value_with (Areality : Areality) = struct (Comonadic.Const.t, 'a) Axis.t -> (('a, 'd) mode_comonadic, 'a, 'd) axis + type 'd axis_packed = P : ('m, 'a, 'd) axis -> 'd axis_packed + + let print_axis (type m a d) ppf (axis : (m, a, d) axis) = + match axis with + | Monadic ax -> Axis.print ppf ax + | Comonadic ax -> Axis.print ppf ax + + let lattice_of_axis (type m a d) (axis : (m, a, d) axis) : + (module Lattice with type t = a) = + match axis with + | Comonadic ax -> Comonadic.Const.lattice_of_axis ax + | Monadic ax -> Monadic.Const.lattice_of_axis ax + let proj_obj : type m a d. (m, a, d) axis -> a C.obj = function | Monadic ax -> Monadic.proj_obj ax | Comonadic ax -> Comonadic.proj_obj ax @@ -1992,6 +2019,12 @@ module Value_with (Areality : Areality) = struct | Comonadic ax -> Comonadic.max_axis ax | Monadic ax -> Monadic.max_axis ax + let is_max : type m a d. (m, a, d) axis -> a -> bool = + fun ax m -> le_axis ax (max_axis ax) m + + let is_min : type m a d. (m, a, d) axis -> a -> bool = + fun ax m -> le_axis ax m (min_axis ax) + let split = split let merge = merge @@ -2250,6 +2283,17 @@ module Const = struct let areality = C.locality_as_regionality areality in { areality; linearity; portability; uniqueness; contention; yielding } + module Axis = struct + let alloc_as_value : type d. d Alloc.axis_packed -> d Value.axis_packed = + function + | P (Comonadic Areality) -> P (Comonadic Areality) + | P (Comonadic Linearity) -> P (Comonadic Linearity) + | P (Comonadic Portability) -> P (Comonadic Portability) + | P (Comonadic Yielding) -> P (Comonadic Yielding) + | P (Monadic Uniqueness) -> P (Monadic Uniqueness) + | P (Monadic Contention) -> P (Monadic Contention) + end + let locality_as_regionality = C.locality_as_regionality end @@ -2295,8 +2339,13 @@ module Modality = struct let is_id (Atom (ax, a)) = match a with - | Join_with c -> Value.Const.le_axis ax c (Value.Const.min_axis ax) - | Meet_with c -> Value.Const.le_axis ax (Value.Const.max_axis ax) c + | Join_with c -> Value.Const.is_min ax c + | Meet_with c -> Value.Const.is_max ax c + + let is_constant (Atom (ax, a)) = + match a with + | Join_with c -> Value.Const.is_max ax c + | Meet_with c -> Value.Const.is_min ax c let print ppf = function | Atom (ax, Join_with c) -> @@ -2355,6 +2404,9 @@ module Modality = struct (let ax : _ Axis.t = Contention in Atom (Monadic ax, Join_with (Axis.proj ax c))) ] + let proj ax = function + | Join_const c -> Atom (Monadic ax, Join_with (Axis.proj ax c)) + let print ppf = function | Join_const c -> Format.fprintf ppf "join_const(%a)" Mode.Const.print c end @@ -2499,6 +2551,9 @@ module Modality = struct (let ax : _ Axis.t = Portability in Atom (Comonadic ax, Meet_with (Axis.proj ax c))) ] + let proj ax = function + | Meet_const c -> Atom (Comonadic ax, Meet_with (Axis.proj ax c)) + let print ppf = function | Meet_const c -> Format.fprintf ppf "meet_const(%a)" Mode.Const.print c end @@ -2641,6 +2696,11 @@ module Modality = struct let to_list { monadic; comonadic } = Comonadic.to_list comonadic @ Monadic.to_list monadic + + let proj (type m a d) (ax : (m, a, d) Value.axis) { monadic; comonadic } = + match ax with + | Monadic ax -> Monadic.proj ax monadic + | Comonadic ax -> Comonadic.proj ax comonadic end type t = (Monadic.t, Comonadic.t) monadic_comonadic diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli index 3bbd185fe56..6dcd47fadfc 100644 --- a/typing/mode_intf.mli +++ b/typing/mode_intf.mli @@ -298,6 +298,8 @@ module type S = sig | Contention : (monadic, Contention.Const.t) t val print : Format.formatter -> ('p, 'r) t -> unit + + val eq : ('p, 'r0) t -> ('p, 'r1) t -> ('r0, 'r1) Misc.eq option end module type Mode := sig @@ -337,6 +339,12 @@ module type S = sig (Comonadic.Const.t, 'a) Axis.t -> (('a, 'd) mode_comonadic, 'a, 'd) axis + type 'd axis_packed = P : ('m, 'a, 'd) axis -> 'd axis_packed + + val print_axis : Format.formatter -> ('m, 'a, 'd) axis -> unit + + val lattice_of_axis : ('m, 'a, 'd) axis -> (module Lattice with type t = 'a) + type ('a, 'b, 'c, 'd, 'e, 'f) modes = { areality : 'a; linearity : 'b; @@ -455,6 +463,10 @@ module type S = sig module Const : sig val alloc_as_value : Alloc.Const.t -> Value.Const.t + module Axis : sig + val alloc_as_value : 'd Alloc.axis_packed -> 'd Value.axis_packed + end + val locality_as_regionality : Locality.Const.t -> Regionality.Const.t end @@ -494,6 +506,9 @@ module type S = sig (** Test if the given modality is the identity modality. *) val is_id : t -> bool + (** Test if the given modality is a constant modality. *) + val is_constant : t -> bool + (** Printing for debugging *) val print : Format.formatter -> t -> unit @@ -542,9 +557,13 @@ module type S = sig val singleton : atom -> t (** Returns the list of [atom] in the given modality. The list is - commutative. *) + commutative. Post-condition: each axis is represented in the + output list exactly once. *) val to_list : t -> atom list + (** Project out the [atom] for the given axis in the given modality. *) + val proj : ('m, 'a, 'd) Value.axis -> t -> atom + (** [equate t0 t1] checks that [t0 = t1]. Definition: [t0 = t1] iff [t0 <= t1] and [t1 <= t0]. *) val equate : t -> t -> (unit, equate_error) Result.t diff --git a/typing/predef.ml b/typing/predef.ml index 52c09a691c8..822e7bce93b 100644 --- a/typing/predef.ml +++ b/typing/predef.ml @@ -220,8 +220,12 @@ let option_argument_jkind = Jkind.Builtin.value ~why:( (* CR layouts v2.8: Simplify this once we have a real subsumption check. *) let list_jkind param = - Jkind.add_baggage ~baggage:param - (Jkind.add_baggage ~baggage:(type_list param) + Jkind.add_baggage + ~modality:Mode.Modality.Value.Const.id + ~baggage:param + (Jkind.add_baggage + ~modality:Mode.Modality.Value.Const.id + ~baggage:(type_list param) (Jkind.Builtin.immutable_data ~why:Boxed_variant)) let list_sort = Jkind.Sort.Const.value @@ -362,7 +366,9 @@ let build_initial_env add_type add_extension empty_env = ~param_jkind:(Jkind.add_nullability_crossing (Jkind.Builtin.any ~why:Array_type_argument)) ~jkind:(fun param -> - Jkind.add_baggage ~baggage:param + Jkind.add_baggage + ~modality:Mode.Modality.Value.Const.id + ~baggage:param (Jkind.Builtin.mutable_data ~why:(Primitive ident_array))) |> add_type1 ident_iarray ~variance:Variance.covariant @@ -370,7 +376,9 @@ let build_initial_env add_type add_extension empty_env = ~param_jkind:(Jkind.add_nullability_crossing (Jkind.Builtin.any ~why:Array_type_argument)) ~jkind:(fun param -> - Jkind.add_baggage ~baggage:param + Jkind.add_baggage + ~modality:Mode.Modality.Value.Const.id + ~baggage:param (Jkind.Builtin.immutable_data ~why:(Primitive ident_iarray))) |> add_type ident_bool ~kind:(variant [ cstr ident_false []; cstr ident_true []]) @@ -409,7 +417,9 @@ let build_initial_env add_type add_extension empty_env = variant [cstr ident_none []; cstr ident_some [unrestricted tvar option_argument_sort]]) ~jkind:(fun param -> - Jkind.add_baggage ~baggage:param + Jkind.add_baggage + ~modality:Mode.Modality.Value.Const.id + ~baggage:param (Jkind.Builtin.immutable_data ~why:Boxed_variant)) |> add_type_with_jkind ident_lexing_position ~kind:( @@ -443,10 +453,10 @@ let build_initial_env add_type add_extension empty_env = ~jkind:Jkind.( of_builtin Const.Builtin.immutable_data ~why:(Primitive ident_lexing_position) |> - add_baggage ~baggage:type_int |> - add_baggage ~baggage:type_int |> - add_baggage ~baggage:type_int |> - add_baggage ~baggage:type_string) + add_baggage ~modality:Mode.Modality.Value.Const.id ~baggage:type_int |> + add_baggage ~modality:Mode.Modality.Value.Const.id ~baggage:type_int |> + add_baggage ~modality:Mode.Modality.Value.Const.id ~baggage:type_int |> + add_baggage ~modality:Mode.Modality.Value.Const.id ~baggage:type_string) |> add_type ident_string ~jkind:Jkind.Const.Builtin.immutable_data |> add_type ident_unboxed_float ~jkind:Jkind.Const.Builtin.float64 |> add_type ident_unboxed_nativeint ~jkind:Jkind.Const.Builtin.word diff --git a/typing/typemode.ml b/typing/typemode.ml index d461fcd33ad..a1a3010f8ce 100644 --- a/typing/typemode.ml +++ b/typing/typemode.ml @@ -25,25 +25,32 @@ exception Error of Location.t * error module Axis_pair = struct type 'm t = - | Modal_axis_pair : 'a Axis.Modal.t * 'a -> modal t + | Modal_axis_pair : ('m, 'a, 'd) Mode.Alloc.axis * 'a -> modal t | Any_axis_pair : 'a Axis.t * 'a -> maybe_nonmodal t let of_string s = let open Mode in match s with - | "local" -> Any_axis_pair (Modal Locality, Locality.Const.Local) - | "global" -> Any_axis_pair (Modal Locality, Locality.Const.Global) - | "unique" -> Any_axis_pair (Modal Uniqueness, Uniqueness.Const.Unique) - | "aliased" -> Any_axis_pair (Modal Uniqueness, Uniqueness.Const.Aliased) - | "once" -> Any_axis_pair (Modal Linearity, Linearity.Const.Once) - | "many" -> Any_axis_pair (Modal Linearity, Linearity.Const.Many) + | "local" -> Any_axis_pair (Modal (Comonadic Areality), Locality.Const.Local) + | "global" -> + Any_axis_pair (Modal (Comonadic Areality), Locality.Const.Global) + | "unique" -> + Any_axis_pair (Modal (Monadic Uniqueness), Uniqueness.Const.Unique) + | "aliased" -> + Any_axis_pair (Modal (Monadic Uniqueness), Uniqueness.Const.Aliased) + | "once" -> Any_axis_pair (Modal (Comonadic Linearity), Linearity.Const.Once) + | "many" -> Any_axis_pair (Modal (Comonadic Linearity), Linearity.Const.Many) | "nonportable" -> - Any_axis_pair (Modal Portability, Portability.Const.Nonportable) - | "portable" -> Any_axis_pair (Modal Portability, Portability.Const.Portable) - | "contended" -> Any_axis_pair (Modal Contention, Contention.Const.Contended) - | "shared" -> Any_axis_pair (Modal Contention, Contention.Const.Shared) + Any_axis_pair + (Modal (Comonadic Portability), Portability.Const.Nonportable) + | "portable" -> + Any_axis_pair (Modal (Comonadic Portability), Portability.Const.Portable) + | "contended" -> + Any_axis_pair (Modal (Monadic Contention), Contention.Const.Contended) + | "shared" -> + Any_axis_pair (Modal (Monadic Contention), Contention.Const.Shared) | "uncontended" -> - Any_axis_pair (Modal Contention, Contention.Const.Uncontended) + Any_axis_pair (Modal (Monadic Contention), Contention.Const.Uncontended) | "maybe_null" -> Any_axis_pair (Nonmodal Nullability, Nullability.Maybe_null) | "non_null" -> Any_axis_pair (Nonmodal Nullability, Nullability.Non_null) @@ -51,8 +58,10 @@ module Axis_pair = struct | "external64" -> Any_axis_pair (Nonmodal Externality, Externality.External64) | "external_" -> Any_axis_pair (Nonmodal Externality, Externality.External) - | "yielding" -> Any_axis_pair (Modal Yielding, Yielding.Const.Yielding) - | "unyielding" -> Any_axis_pair (Modal Yielding, Yielding.Const.Unyielding) + | "yielding" -> + Any_axis_pair (Modal (Comonadic Yielding), Yielding.Const.Yielding) + | "unyielding" -> + Any_axis_pair (Modal (Comonadic Yielding), Yielding.Const.Unyielding) | _ -> raise Not_found end @@ -111,7 +120,9 @@ let transl_modifier_annots annots = let transl_mode_annots annots : Alloc.Const.Option.t = let step modifiers_so_far annot = - let { txt = Modal_axis_pair (type a) ((axis, mode) : a Axis.Modal.t * a); + let { txt = + Modal_axis_pair (type m a d) + ((axis, mode) : (m, a, d) Mode.Alloc.axis * a); loc } = transl_annot ~annot_type:Mode ~required_mode_maturity:(Some Stable) @@ -160,18 +171,18 @@ let transl_modality ~maturity { txt = Parsetree.Modality modality; loc } = { txt = modality; loc } in match axis_pair.txt with - | Modal_axis_pair (Locality, mode) -> + | Modal_axis_pair (Comonadic Areality, mode) -> Modality.Atom (Comonadic Areality, Meet_with (Const.locality_as_regionality mode)) - | Modal_axis_pair (Linearity, mode) -> + | Modal_axis_pair (Comonadic Linearity, mode) -> Modality.Atom (Comonadic Linearity, Meet_with mode) - | Modal_axis_pair (Uniqueness, mode) -> - Modality.Atom (Monadic Uniqueness, Join_with mode) - | Modal_axis_pair (Portability, mode) -> + | Modal_axis_pair (Comonadic Portability, mode) -> Modality.Atom (Comonadic Portability, Meet_with mode) - | Modal_axis_pair (Contention, mode) -> + | Modal_axis_pair (Monadic Uniqueness, mode) -> + Modality.Atom (Monadic Uniqueness, Join_with mode) + | Modal_axis_pair (Monadic Contention, mode) -> Modality.Atom (Monadic Contention, Join_with mode) - | Modal_axis_pair (Yielding, mode) -> + | Modal_axis_pair (Comonadic Yielding, mode) -> Modality.Atom (Comonadic Yielding, Meet_with mode) let untransl_modality (a : Modality.t) : Parsetree.modality loc =