diff --git a/.github/workflows/ocamlformat.yml b/.github/workflows/ocamlformat.yml index 6436fb783b9..e4e2a479d95 100644 --- a/.github/workflows/ocamlformat.yml +++ b/.github/workflows/ocamlformat.yml @@ -21,7 +21,7 @@ jobs: path: 'flambda_backend' - name: Setup OCaml ${{ matrix.ocaml-compiler }} - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} diff --git a/testsuite/tests/parsetree/source_jane_street.ml b/testsuite/tests/parsetree/source_jane_street.ml index 1c23c5d2566..5e80e901932 100644 --- a/testsuite/tests/parsetree/source_jane_street.ml +++ b/testsuite/tests/parsetree/source_jane_street.ml @@ -1066,14 +1066,10 @@ 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 uncontended portable with 'a -type ('a, 'b) either : value mod many uncontended portable with 'a * 'b -type 'a contended : value mod many uncontended portable with 'a @@ contended -type 'a contended_with_int - : value mod many uncontended portable - with 'a @@ contended - - with int +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 |}] (* not yet supported *) diff --git a/testsuite/tests/typing-jkind-bounds/allow_illegal_crossing.ml b/testsuite/tests/typing-jkind-bounds/allow_illegal_crossing.ml index aff5d874aae..abfd77d0767 100644 --- a/testsuite/tests/typing-jkind-bounds/allow_illegal_crossing.ml +++ b/testsuite/tests/typing-jkind-bounds/allow_illegal_crossing.ml @@ -12,21 +12,21 @@ type a type b : value mod portable = { a : int; b : int } [%%expect {| type a -type b = { a : int; b : int; } +type b : immutable_data = { a : int; b : int; } |}] type a type b : value mod uncontended = Foo of int [%%expect {| type a -type b = Foo of int +type b : immutable_data = Foo of int |}] type a type b : value mod uncontended portable = Foo of int | Bar of int [%%expect {| type a -type b = Foo of int | Bar of int +type b : immutable_data = Foo of int | Bar of int |}] type a @@ -59,7 +59,7 @@ Error: The kind of type "a" is value type t : value mod portable uncontended = { a : int; b : int } [%%expect {| -type t = { a : int; b : int; } +type t : immutable_data = { a : int; b : int; } |}] type ('a, 'b) t : value mod portable uncontended = { a : 'a; b : 'b } @@ -69,40 +69,40 @@ type ('a, 'b) t : immutable_data = { a : 'a; b : 'b; } type t : value mod portable = private { foo : string } [%%expect {| -type t = private { foo : string; } +type t : immutable_data = private { foo : string; } |}] type a : value mod portable = { foo : string } type b : value mod portable = a = { foo : string } [%%expect {| -type a = { foo : string; } -type b = a = { foo : string; } +type a : immutable_data = { foo : string; } +type b = a : immutable_data = { foo : string; } |}] type a : value mod uncontended = private { foo : string } type b : value mod uncontended = a = private { foo : string } [%%expect {| -type a = private { foo : string; } -type b = a = private { foo : string; } +type a : immutable_data = private { foo : string; } +type b = a : immutable_data = private { foo : string; } |}] type t : value mod uncontended = private Foo of int | Bar [%%expect {| -type t = private Foo of int | Bar +type t : immutable_data = private Foo of int | Bar |}] type a : value mod uncontended = Foo of int | Bar type b : value mod uncontended = a = Foo of int | Bar [%%expect {| -type a = Foo of int | Bar -type b = a = Foo of int | Bar +type a : immutable_data = Foo of int | Bar +type b = a : immutable_data = Foo of int | Bar |}] type a : value mod portable = private Foo of int | Bar type b : value mod portable = a = private Foo of int | Bar [%%expect {| -type a = private Foo of int | Bar -type b = a = private Foo of int | Bar +type a : immutable_data = private Foo of int | Bar +type b = a : immutable_data = private Foo of int | Bar |}] type t : value mod uncontended = private Foo of int ref | Bar @@ -130,7 +130,7 @@ end = struct type t = { a : string } end [%%expect {| -module A : sig type t = { a : string; } end +module A : sig type t : immutable_data = { a : string; } end |}] (********************************************) @@ -140,7 +140,7 @@ type a : value mod portable uncontended = Foo of string type ('a : value mod portable uncontended) b type c = a b [%%expect {| -type a = Foo of string +type a : immutable_data = Foo of string type ('a : value mod uncontended portable) b type c = a b |}] @@ -158,7 +158,7 @@ type t : value mod portable uncontended = { a : string; b : int } let f : ('a : value mod portable uncontended). 'a -> 'a = fun x -> x let g (x : t) = f x [%%expect {| -type t = { a : string; b : int; } +type t : immutable_data = { a : string; b : int; } val f : ('a : value mod uncontended portable). 'a -> 'a = val g : t -> t = |}] @@ -166,7 +166,7 @@ val g : t -> t = type t : value mod portable uncontended = { a : int; b : int } let x : _ as (_ : value mod portable uncontended) = { a = 5; b = 5 } [%%expect {| -type t = { a : int; b : int; } +type t : immutable_data = { a : int; b : int; } val x : t = {a = 5; b = 5} |}] @@ -180,7 +180,7 @@ val x : (int, int) t = {a = 5; b = 5} type t : value mod portable uncontended = Foo of string | Bar of int let x : _ as (_ : value mod portable uncontended) = Foo "hello world" [%%expect {| -type t = Foo of string | Bar of int +type t : immutable_data = Foo of string | Bar of int val x : t = Foo "hello world" |}] @@ -200,7 +200,7 @@ type ('a : value mod portable) u = 'a type v = A.t u let x : _ as (_ : value mod portable) = ({ a = "hello" } : A.t) [%%expect {| -module A : sig type t = { a : string; } end +module A : sig type t : immutable_data = { a : string; } end type ('a : value mod portable) u = 'a type v = A.t u val x : A.t = {A.a = "hello"} @@ -210,7 +210,7 @@ type t : value mod portable = { a : string } let my_str : string @@ nonportable = "" let y = ({ a = my_str } : t @@ portable) [%%expect {| -type t = { a : string; } +type t : immutable_data = { a : string; } val my_str : string = "" val y : t = {a = ""} |}] @@ -230,7 +230,7 @@ let f () = let _ = ({ a = make_str () } : t @@ uncontended) in () [%%expect {| -type t = { a : string; } +type t : immutable_data = { a : string; } val make_str : unit -> string = val f : unit -> unit = |}] @@ -241,7 +241,7 @@ let f () = let _ : t @@ uncontended = { a = make_str () } in () [%%expect {| -type t = { a : string; } +type t : immutable_data = { a : string; } val make_str : unit -> string = val f : unit -> unit = |}] @@ -282,7 +282,7 @@ type t : value mod portable uncontended = Foo of string | Bar of int let g (x : t @@ nonportable contended) = f x; f (Foo ""); f (Bar 10) [%%expect {| val f : 'a @ portable -> unit = -type t = Foo of string | Bar of int +type t : immutable_data = Foo of string | Bar of int val g : t @ contended -> unit = |}] @@ -545,7 +545,7 @@ end = struct type v = t u end [%%expect {| -module A : sig type t = { a : string; } end +module A : sig type t : immutable_data = { a : string; } end |}, Principal{| Line 6, characters 11-12: 6 | type v = t u @@ -582,7 +582,7 @@ end = struct let x : _ as (_ : value mod portable) = { a = "hello" } end [%%expect {| -module A : sig type t = { a : string; } end +module A : sig type t : immutable_data = { a : string; } end |}, Principal{| Line 5, characters 42-57: 5 | let x : _ as (_ : value mod portable) = { a = "hello" } @@ -687,14 +687,14 @@ type a = { foo : string } type b : value mod portable = a = { foo : string } [%%expect {| type a = { foo : string; } -type b = a = { foo : string; } +type b = a : immutable_data = { foo : string; } |}] type a = private { foo : string } type b : value mod uncontended = a = private { foo : string } [%%expect {| type a = private { foo : string; } -type b = a = private { foo : string; } +type b = a : immutable_data = private { foo : string; } |}] type a = { foo : string -> string } @@ -727,14 +727,14 @@ type a = Foo of string | Bar type b : value mod uncontended = a = Foo of string | Bar [%%expect {| type a = Foo of string | Bar -type b = a = Foo of string | Bar +type b = a : immutable_data = Foo of string | Bar |}] type a = private Foo of string | Bar type b : value mod portable = a = private Foo of string | Bar [%%expect {| type a = private Foo of string | Bar -type b = a = private Foo of string | Bar +type b = a : immutable_data = private Foo of string | Bar |}] type a = Foo of { mutable x : int } | Bar diff --git a/testsuite/tests/typing-jkind-bounds/modalities.ml b/testsuite/tests/typing-jkind-bounds/modalities.ml index 74a5ed52049..776ac8d9764 100644 --- a/testsuite/tests/typing-jkind-bounds/modalities.ml +++ b/testsuite/tests/typing-jkind-bounds/modalities.ml @@ -96,12 +96,8 @@ 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 many uncontended portable external_ - non_null - with string @@ global - & value_or_null mod global unique many uncontended portable - external_ non_null - with string @@ global + immediate with string @@ global with string @@ global & immediate + with string @@ global with string @@ global 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 @@ -128,12 +124,9 @@ Line 1, characters 65-66: 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 many uncontended portable external_ - non_null - with string -> string @@ global - & value_or_null mod global unique many uncontended portable - external_ non_null - with string -> string @@ global + immediate with string -> string @@ global + with string -> string @@ global & immediate + with string -> string @@ global with string -> string @@ global 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 diff --git a/testsuite/tests/typing-layouts-or-null/reexport.ml b/testsuite/tests/typing-layouts-or-null/reexport.ml index f0559ea1a2c..f20a77151ee 100644 --- a/testsuite/tests/typing-layouts-or-null/reexport.ml +++ b/testsuite/tests/typing-layouts-or-null/reexport.ml @@ -21,8 +21,8 @@ Lines 2-4, characters 2-16: 4 | | This of 'a Error: The kind of type "'a or_null" is value_or_null because it is the primitive value_or_null type or_null. - But the kind of type "'a or_null" must be a subkind of - value mod many uncontended portable with 'a + But the kind of type "'a or_null" must be a subkind of immutable_data + with 'a because of the definition of t at lines 2-4, characters 2-16. |}] diff --git a/testsuite/tests/typing-layouts-products/basics_alpha.ml b/testsuite/tests/typing-layouts-products/basics_alpha.ml index e0e6a5b3332..b46f79b7f29 100644 --- a/testsuite/tests/typing-layouts-products/basics_alpha.ml +++ b/testsuite/tests/typing-layouts-products/basics_alpha.ml @@ -67,9 +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 mod global unique many uncontended portable external_ non_null + any_non_null mod global unique many uncontended portable external_ with t1 with t2 - & any mod global unique many uncontended portable external_ non_null + & any_non_null mod global unique many uncontended 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 @@ -86,9 +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 mod global unique many uncontended portable external_ non_null + any_non_null mod global unique many uncontended portable external_ with t1 with t2 - & any mod global unique many uncontended portable external_ non_null + & any_non_null mod global unique many uncontended portable external_ with t1 with t2 because it is an unboxed tuple. But the kind of type "#(t1 * t2)" must be a subkind of @@ -106,9 +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 mod global unique many uncontended portable external_ non_null + any_non_null mod global unique many uncontended portable external_ with t1 with t2 - & any mod global unique many uncontended portable external_ non_null + & any_non_null mod global unique many uncontended 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-unboxed-records/basics.ml b/testsuite/tests/typing-layouts-unboxed-records/basics.ml index 863768891c0..151f55b56b6 100644 --- a/testsuite/tests/typing-layouts-unboxed-records/basics.ml +++ b/testsuite/tests/typing-layouts-unboxed-records/basics.ml @@ -760,12 +760,8 @@ Line 1, characters 0-61: 1 | type q : any mod portable = #{ x : int -> int; y : int -> q } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The kind of type "q" is - value_or_null mod global unique many uncontended portable external_ - non_null - with int -> int with int -> q - & value_or_null mod global unique many uncontended portable - external_ non_null - with int -> int with int -> q + immediate with int -> int with int -> q & immediate with int -> int + with int -> q because it is an unboxed record. But the kind of type "q" must be a subkind of value_or_null mod portable & value_or_null mod portable diff --git a/typing/ctype.ml b/typing/ctype.ml index 4e0d598871e..dab8f45e0b2 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -2207,7 +2207,7 @@ let rec estimate_type_jkind ~expand_component env ty = (* Checking [has_baggage] here is needed for correctness, because intersection types sometimes do not unify with themselves. Removing this check causes typing-misc/pr7937.ml to fail. *) - if Jkind.has_baggage jkind + if Jkind.has_with_bounds jkind then let level = get_level ty in (* CR layouts v2.8: We could possibly skip this substitution if we're diff --git a/typing/jkind.ml b/typing/jkind.ml index cd7af237027..b80f885c201 100644 --- a/typing/jkind.ml +++ b/typing/jkind.ml @@ -368,7 +368,6 @@ module Error = struct from_attribute : Builtin_attributes.jkind_attribute Location.loc } | Unimplemented_syntax - | Modded_bound_with_baggage_constraints : 'a Axis.t -> t | With_on_right exception User_error of Location.t * t @@ -379,65 +378,42 @@ let raise ~loc err = raise (Error.User_error (loc, err)) (******************************) (*** Bounds, specialized to the real [type_expr] ***) -module Baggage = struct - include Jkind_types.Baggage +module With_bounds = struct + include Jkind_types.With_bounds type nonrec 'd t = (type_expr, 'd) t (* You might think that we can only do joins on the left. But that's not true! We can join constants. The important thing is that the allowances of both arguments are the same and that they match the result: this will mean that - if we have any baggage in either argument, the result is an l-Baggage, as + if we have any with_bounds in either argument, the result is an l-With_bounds, as required. This might change once we have arrow kinds, but we'll deal with that when we get there. *) let join (type l r) (bag1 : (l * r) t) (bag2 : (l * r) t) : (l * r) t = match bag1, bag2 with - | No_baggage, No_baggage -> No_baggage - | No_baggage, b -> b - | b, No_baggage -> b (* CR layouts v2.8: List concatentation is slow. *) - | Baggage (ty1, tys1), Baggage (ty2, tys2) -> - Baggage (ty1, tys1 @ (ty2 :: tys2)) + | No_with_bounds, No_with_bounds -> No_with_bounds + | No_with_bounds, b -> b + | b, No_with_bounds -> b (* CR layouts v2.8: List concatentation is slow. *) + | With_bounds (ty1, tys1), With_bounds (ty2, tys2) -> + With_bounds (ty1, tys1 @ (ty2 :: tys2)) let meet (type l1 l2) (bag1 : (l1 * allowed) t) (bag2 : (l2 * allowed) t) : (l1 * allowed) t = - match bag1, bag2 with No_baggage, No_baggage -> No_baggage + match bag1, bag2 with No_with_bounds, No_with_bounds -> No_with_bounds - let add_baggage (t : (allowed * 'r) t) baggage : (allowed * 'r) t = + let add ~deep_only ~modality ~type_expr (t : (allowed * 'r) t) : + (allowed * 'r) t = + let type_info = Type_info.create ~type_expr ~modality ~deep_only in match t with - | No_baggage -> Baggage (baggage, []) - | Baggage (ty, tys) -> Baggage (baggage, ty :: tys) -end - -module Bound = struct - include Jkind_types.Bound - - type nonrec ('d, 'a) t = (type_expr, 'd, 'a) t - - let simple modifier = { modifier; baggage = No_baggage } - - let join (type axis) ~(axis : axis Axis.t) { modifier = mod1; baggage = bag1 } - { modifier = mod2; baggage = bag2 } = - let (module Ops) = Axis.get axis in - { modifier = Ops.join mod1 mod2; baggage = Baggage.join bag1 bag2 } - - let meet (type axis) ~(axis : axis Axis.t) { modifier = mod1; baggage = bag1 } - { modifier = mod2; baggage = bag2 } = - let (module Ops) = Axis.get axis in - { modifier = Ops.meet mod1 mod2; baggage = Baggage.meet bag1 bag2 } - - let add_baggage (type axis) ({ modifier; baggage } as bound) - ~(axis : axis Axis.t) new_baggage = - (* No need to add baggage to top. While the subsumption check is still not - great, this is not just an optimization; see test - typing-layouts/illegal-across-modules/test.ml *) - (* CR layouts v2.8: Fix the comment above after we fix subsumption. *) - let (module Ops) = Axis.get axis in - if Ops.le Ops.max modifier - then bound - else { bound with baggage = Baggage.add_baggage baggage new_baggage } - - let reduce_baggage (type a) ~type_equal ~jkind_of_type ~(axis : a Axis.t) - modifier baggage = + | No_with_bounds -> With_bounds (type_info, []) + | With_bounds (ty, tys) -> With_bounds (type_info, ty :: tys) + + (* CR aspsmith: This should be refactored to operate holistically (eg on Bounds.t) + rather than per-axis. *) + (* Extend the given bound for an axis by (recursively) instantiating the given + with-bounds to determine their upper bounds *) + let extend_bound (type a l r) ~type_equal ~jkind_of_type ~(axis : a Axis.t) + ~bound (t : (l * r) t) = (* Sadly, it seems hard (impossible?) to be sure to expand all types here without using a fuel parameter to stop infinite regress. Here is a nasty case: @@ -467,7 +443,7 @@ module Bound = struct the path to a type constructor (like [t] or [loopy]) or a tuple. (We need to include tuples because of the possibility of recursive types and the fact that tuples track their element types in their - jkind's baggage.) + jkind's with_bounds.) The initial fuel per type head is 10, as it seems hard to imagine that we're going to make meaningful progress if we've seen the same type @@ -521,10 +497,10 @@ module Bound = struct | Tvar _ | Tarrow _ | Tunboxed_tuple _ | Tobject _ | Tfield _ | Tnil | Tvariant _ | Tunivar _ | Tpackage _ -> (* these cases either cannot be infinitely recursive or their jkinds - do not have baggage *) + do not have with_bounds *) Continue t | Tlink _ | Tsubst _ -> - Misc.fatal_error "Tlink or Tsubst in reduce_baggage" + Misc.fatal_error "Tlink or Tsubst in With_bounds.reduce" end in let (module A) = Axis.get axis in let rec loop ctl bound_so_far = function @@ -539,10 +515,12 @@ module Bound = struct match jkind_of_type b with | Some b_jkind -> let b_bound = Bounds.get ~axis b_jkind.jkind.upper_bounds in - let bound_so_far = A.join bound_so_far b_bound.modifier in + let types_on_axis = + With_bounds.types_on_axis ~axis b_jkind.jkind.with_bounds + in + let bound_so_far = A.join bound_so_far b_bound in let bound_so_far = - loop ctl_after_unpacking_b bound_so_far - (Baggage.as_list b_bound.baggage) + loop ctl_after_unpacking_b bound_so_far types_on_axis in (* Use *original* ctl here, so we don't fall over on a record with 20 lists with different payloads. *) @@ -554,47 +532,18 @@ module Bound = struct that we need to worry about principality here. *) A.max)) in - loop Loop_control.starting modifier baggage - - let reduce ~type_equal ~jkind_of_type ~axis bound = - reduce_baggage ~type_equal ~jkind_of_type ~axis bound.modifier - (Baggage.as_list bound.baggage) - - let less_or_equal : - type axis l r. - type_equal:_ -> - jkind_of_type:_ -> - axis:axis Axis.t -> - (allowed * r, axis) t -> - (l * allowed, axis) t -> - Misc.Le_result.t = - fun ~type_equal ~jkind_of_type ~axis { modifier = m1; baggage = b1 } - { modifier = m2; baggage = b2 } -> - let (module Axis_ops) = Axis.get axis in - match b1, b2 with - | No_baggage, No_baggage -> Axis_ops.less_or_equal m1 m2 - (* CR layouts v2.8: This should expand types on the left. *) - | Baggage (ty, tys), No_baggage -> - if Axis_ops.le Axis_ops.max m2 - then Less - else - let m1' = - reduce_baggage ~type_equal ~jkind_of_type ~axis m1 (ty :: tys) - in - Axis_ops.less_or_equal m1' m2 + loop Loop_control.starting bound (types_on_axis ~axis t) end module Bounds = struct include Jkind_types.Bounds - type nonrec 'd t = (type_expr, 'd) t - let min = Create.f { f = (fun (type axis) ~(axis : axis Axis.t) -> let (module Bound_ops) = Axis.get axis in - Bound.simple Bound_ops.min) + Bound_ops.min) } let max = @@ -602,48 +551,35 @@ module Bounds = struct { f = (fun (type axis) ~(axis : axis Axis.t) -> let (module Bound_ops) = Axis.get axis in - Bound.simple Bound_ops.max) + Bound_ops.max) } let simple ~locality ~linearity ~uniqueness ~portability ~contention ~externality ~nullability = - { locality = Bound.simple locality; - linearity = Bound.simple linearity; - uniqueness = Bound.simple uniqueness; - portability = Bound.simple portability; - contention = Bound.simple contention; - externality = Bound.simple externality; - nullability = Bound.simple nullability + { locality; + linearity; + uniqueness; + portability; + contention; + externality; + nullability } - let join bounds1 bounds2 = Map2.f { f = Bound.join } bounds1 bounds2 - - let meet bounds1 bounds2 = Map2.f { f = Bound.meet } bounds1 bounds2 - - let less_or_equal ~type_equal ~jkind_of_type bounds1 bounds2 = - Fold2.f + let join = + Map2.f { f = - (fun (type axis) ~(axis : axis Axis.t) bound1 bound2 -> - Bound.less_or_equal ~type_equal ~jkind_of_type ~axis bound1 bound2) + (fun (type axis) ~(axis : axis Axis.t) -> + let (module Bound_ops) = Axis.get axis in + Bound_ops.join) } - ~combine:Misc.Le_result.combine bounds1 bounds2 - let add_baggage ~modality ~deep_only ~baggage bounds = - (* Add the type as a baggage type along all deep axes *) - Map.f + let meet = + Map2.f { f = - (fun ~axis (bound : _ Bound.t) : _ Bound.t -> - if (not (Jkind_axis.Axis.modality_is_const_for_axis axis modality)) - && (Axis.is_deep axis || not deep_only) - then Bound.add_baggage bound ~axis baggage - else bound) + (fun (type axis) ~(axis : axis Axis.t) -> + let (module Bound_ops) = Axis.get axis in + Bound_ops.meet) } - bounds - - let has_baggage bounds = - Fold.f - { f = (fun ~axis:_ bound -> Baggage.has_baggage bound.baggage) } - ~combine:( || ) bounds end (***********************) @@ -680,9 +616,13 @@ module Const = struct include Layout_and_axes.Allow_disallow - let max = { layout = Layout.Const.max; upper_bounds = Bounds.max } + let max = + { layout = Layout.Const.max; + upper_bounds = Bounds.max; + with_bounds = No_with_bounds + } - let no_baggage_and_equal t1 t2 = + let no_with_bounds_and_equal t1 t2 = let open Misc.Stdlib.Monad.Option.Syntax in let t1_t2 = let* t1 = try_allow_l t1 in @@ -704,10 +644,10 @@ module Const = struct let mk_jkind ~mode_crossing ~nullability (layout : Layout.Const.t) = let upper_bounds = match mode_crossing with - | true -> { Bounds.min with nullability = Bound.simple nullability } - | false -> { Bounds.max with nullability = Bound.simple nullability } + | true -> { Bounds.min with nullability } + | false -> { Bounds.max with nullability } in - { layout; upper_bounds } + { layout; upper_bounds; with_bounds = No_with_bounds } let any = { jkind = mk_jkind Any ~mode_crossing:false ~nullability:Maybe_null; @@ -738,7 +678,8 @@ module Const = struct ~contention:Contention.Const.min ~portability:Portability.Const.min ~uniqueness:Uniqueness.Const.max ~locality:Locality.Const.max - ~externality:Externality.max ~nullability:Nullability.Non_null + ~externality:Externality.max ~nullability:Nullability.Non_null; + with_bounds = No_with_bounds }; name = "immutable_data" } @@ -751,7 +692,8 @@ module Const = struct ~contention:Contention.Const.max ~portability:Portability.Const.min ~uniqueness:Uniqueness.Const.max ~locality:Locality.Const.max - ~externality:Externality.max ~nullability:Nullability.Non_null + ~externality:Externality.max ~nullability:Nullability.Non_null; + with_bounds = No_with_bounds }; name = "mutable_data" } @@ -802,7 +744,7 @@ module Const = struct { immediate.jkind with upper_bounds = { immediate.jkind.upper_bounds with - externality = Bound.simple Externality.External64 + externality = Externality.External64 } }; name = "immediate64" @@ -881,89 +823,25 @@ module Const = struct type printable_jkind = { base : string; modal_bounds : string list; - with_tys : + printable_with_bounds : (Outcometree.out_type * Outcometree.out_modality_new list) list } - (* Note [Reconstructing modalities] - ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - Currently (though not forever!), we have two kinds of modalities: - - - Constant modalities - - Identity modalities - - For the purposes of [with]-kinds, identity modalities on an axis for a type serve - to "include" that type on the baggage for that axis, and constant modalities serve - to "exclude" that type from that axis. - - When printing jkinds, we scan the baggage on each axis, building up (morally) a map - from type, to axis, to a variant ([Modality_axis_map.modality]) indicating whether - to include a constant modality for that axis on that type in the [with] of the - jkind. We start out with a [Constant_modality] for the axes mentioned in the bounds - of the jkind, then when a type is mentioned on an axis, we switch it to - [Don't_include]. - *) - - module Modality_axis_map = struct - (* Tracks, for each axis, whether we should be including a constant modality "zeroing out" - that axis on a type. Used to reconstruct modalities when printing kinds. See Note - [Reconstructing modalities] for more. *) - - type modality = - | Constant_modality - | No_modality - (* Plausibly, once we have non-constant, non-identity modalities, this could be - extended to track those as well *) - - include Jkind_axis.Axis_collection (struct - type (+'type_expr, 'd, 'a) t = modality constraint 'd = 'l * 'r - end) - - let to_modality = - Fold.f - ~combine:(fun m1 m2 -> Mode.Modality.Value.Const.concat m1 ~then_:m2) - { f = - (fun (type axis) ~(axis : axis Jkind_axis.Axis.t) include_modality -> - match axis, include_modality with - | Modal axis, Constant_modality -> ( - let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in - match axis with - | Monadic ax -> - Mode.Modality.Value.Const.singleton - (Atom - ( Monadic ax, - Join_with (Mode.Value.Monadic.Const.max_axis ax) )) - | Comonadic ax -> - Mode.Modality.Value.Const.singleton - (Atom - ( Comonadic ax, - Meet_with (Mode.Value.Comonadic.Const.min_axis ax) )) - ) - | _ -> Mode.Modality.Value.Const.id) - } - end - - let get_modal_bound (type a) ~(axis : a Axis.t) ~(base : ('d1, a) Bound.t) - (actual : ('d2, a) Bound.t) = + let get_modal_bound (type a) ~(axis : a Axis.t) ~(base : a) (actual : a) = let (module A) = Axis.get axis in - let type_equal _ _ = false in - let jkind_of_type _ = None in (* CR layouts v2.8: Fix printing! *) let less_or_equal a b = - let open Misc.Stdlib.Monad.Option.Syntax in - let* a = Bound.try_allow_l a in - let* b = Bound.try_allow_r b in - Some (Bound.less_or_equal ~type_equal ~jkind_of_type ~axis a b) + let (module Axis_ops) = Axis.get axis in + Axis_ops.less_or_equal a b in match less_or_equal actual base with - | Some Less | Some Equal -> ( + | Less | Equal -> ( match less_or_equal base actual with - | Some Less | Some Equal -> `Valid None - | None | Some Not_le -> - `Valid (Some (Format.asprintf "%a" A.print actual.modifier))) - | None | Some Not_le -> `Invalid + | Less | Equal -> `Valid None + | Not_le -> `Valid (Some (Format.asprintf "%a" A.print actual))) + | Not_le -> `Invalid - let get_modal_bounds ~(base : _ Bounds.t) (actual : _ Bounds.t) = + let get_modal_bounds ~(base : Bounds.t) (actual : Bounds.t) = Axis.all |> List.map (fun (Axis.Pack axis) -> let base = Bounds.get ~axis base in @@ -978,55 +856,6 @@ module Const = struct | Some acc, `Valid (Some mode) -> Some (mode :: acc)) (Some []) - (* Reconstruct the [with]-types for the kind. - - See Note [Reconstructing modalities] *) - let get_with_tys ~base upper_bounds = - let default_include_modality = - Modality_axis_map.Create.f - { f = - (fun ~axis -> - let base = Bounds.get ~axis base in - let actual = Bounds.get ~axis upper_bounds in - (* Note we're only defaulting to [Constant_modality] for the bounds actually - mentioned in the kind, so we don't print eg `immutable_data with 'a` as - `immutable_data with 'a @@ global many *) - match get_modal_bound ~axis ~base actual with - | `Valid (Some _) -> Constant_modality - | `Valid None | `Invalid -> No_modality) - } - in - let types = Btype.TypeHash.create 8 in - Jkind_types.Bounds.Iter.f - { f = - (fun ~axis { modifier = _; baggage } -> - List.iter - (fun ty -> - let include_modality = - Btype.TypeHash.find_opt types ty - |> Option.value ~default:default_include_modality - in - let include_modality' = - (* If a type is mentioned on an axis, we don't want a modality on that - type! *) - Modality_axis_map.set ~axis include_modality No_modality - in - Btype.TypeHash.replace types ty include_modality') - (Jkind_types.Baggage.as_list baggage)) - } - upper_bounds; - Btype.TypeHash.to_seq types - |> Seq.map (fun (ty, mentioned) -> - let modality = Modality_axis_map.to_modality mentioned in - let ty = - !outcometree_of_type_scheme (Types.Transient_expr.type_expr ty) - in - let modalities = - !outcometree_of_modalities_new Types.Immutable [] modality - in - ty, modalities) - |> List.of_seq - (** Write [actual] in terms of [base] *) let convert_with_base ~(base : Builtin.t) actual = let matching_layouts = @@ -1035,12 +864,16 @@ module Const = struct let modal_bounds = get_modal_bounds ~base:base.jkind.upper_bounds actual.upper_bounds in - let with_tys = - get_with_tys ~base:base.jkind.upper_bounds actual.upper_bounds + let printable_with_bounds = + List.map + (fun With_bounds.Type_info.{ type_expr; modality; _ } -> + ( !outcometree_of_type_scheme type_expr, + !outcometree_of_modalities_new Types.Immutable [] modality )) + (With_bounds.as_list actual.with_bounds) in match matching_layouts, modal_bounds with | true, Some modal_bounds -> - Some { base = base.name; modal_bounds; with_tys } + Some { base = base.name; modal_bounds; printable_with_bounds } | false, _ | _, None -> None (** Select the out_jkind_const with the least number of modal bounds to print *) @@ -1059,14 +892,7 @@ module Const = struct let jkind = if Language_extension.(is_at_least Layouts Alpha) then jkind - else - { jkind with - upper_bounds = - Bounds.Map.f - { f = (fun ~axis:_ bound -> { bound with baggage = No_baggage }) - } - jkind.upper_bounds - } + else { jkind with with_bounds = No_with_bounds } in (* For each primitive jkind, we try to print the jkind in terms of it (this is possible if the primitive is a subjkind of it). We then choose the "simplest". The @@ -1091,9 +917,8 @@ module Const = struct { jkind = { layout = jkind.layout; upper_bounds = - { Bounds.max with - nullability = Bound.simple Nullability.Non_null - } + { Bounds.max with nullability = Nullability.Non_null }; + with_bounds = No_with_bounds }; name = Layout.Const.to_string jkind.layout } @@ -1106,7 +931,11 @@ module Const = struct let out_jkind_verbose = convert_with_base ~base: - { jkind = { layout = jkind.layout; upper_bounds = Bounds.max }; + { jkind = + { layout = jkind.layout; + upper_bounds = Bounds.max; + with_bounds = No_with_bounds + }; name = Layout.Const.to_string jkind.layout } jkind @@ -1117,12 +946,13 @@ module Const = struct in let base, with_tys = match printable_jkind with - | { base; modal_bounds = _ :: _ as modal_bounds; with_tys } -> + | { base; modal_bounds = _ :: _ as modal_bounds; printable_with_bounds } + -> ( Outcometree.Ojkind_const_mod (Ojkind_const_abbreviation base, modal_bounds), - with_tys ) - | { base; modal_bounds = []; with_tys } -> - Outcometree.Ojkind_const_abbreviation base, with_tys + printable_with_bounds ) + | { base; modal_bounds = []; printable_with_bounds } -> + Outcometree.Ojkind_const_abbreviation base, printable_with_bounds in (* Finally, add on the [with]-types and their modalities *) List.fold_left @@ -1138,16 +968,22 @@ module Const = struct (*******************************) (* converting user annotations *) - let jkind_of_product_annotations jkinds = - let folder (layouts_acc, upper_bounds_acc) { layout; upper_bounds } = - layout :: layouts_acc, Bounds.join upper_bounds upper_bounds_acc + let jkind_of_product_annotations (type l r) (jkinds : (l * r) t list) = + let folder (type l r) (layouts_acc, upper_bounds_acc, with_bounds_acc) + ({ layout; upper_bounds; with_bounds } : (l * r) t) = + ( layout :: layouts_acc, + Bounds.join upper_bounds upper_bounds_acc, + With_bounds.join with_bounds with_bounds_acc ) in - let layouts, upper_bounds = + let layouts, upper_bounds, with_bounds = List.fold_left folder - ([], Bounds.min |> Bounds.allow_left |> Bounds.allow_right) + ([], Bounds.min, Jkind_types.With_bounds.No_with_bounds) jkinds in - { layout = Layout.Const.Product (List.rev layouts); upper_bounds } + { layout = Layout.Const.Product (List.rev layouts); + upper_bounds; + with_bounds + } let rec of_user_written_annotation_unchecked_level : type l r. @@ -1181,7 +1017,7 @@ module Const = struct let upper_bounds = Bounds.Create.f { f = - (fun (type a) ~(axis : a Axis.t) : _ Bound.t -> + (fun (type a) ~(axis : a Axis.t) -> let (module A : Lattice with type t = a) = Axis.get axis in let parsed_modifier = Typemode.Transled_modifiers.get ~axis parsed_modifiers @@ -1189,17 +1025,11 @@ module Const = struct let base_bound = Bounds.get ~axis base.upper_bounds in match parsed_modifier, base_bound with | None, base_bound -> base_bound - | ( Some parsed_modifier, - { modifier = base_modifier; baggage = No_baggage } ) -> - { modifier = A.meet base_modifier parsed_modifier.txt; - baggage = No_baggage - } - | Some parsed_modifier, { modifier = _; baggage = Baggage _ } -> - raise ~loc:parsed_modifier.loc - (Modded_bound_with_baggage_constraints axis)) + | Some parsed_modifier, base_modifier -> + A.meet base_modifier parsed_modifier.txt) } in - { layout = base.layout; upper_bounds } + { layout = base.layout; upper_bounds; with_bounds = No_with_bounds } | Product ts -> let jkinds = List.map (of_user_written_annotation_unchecked_level context) ts @@ -1215,9 +1045,10 @@ module Const = struct Typemode.transl_modalities ~maturity:Stable Immutable [] modalities in { layout = base.layout; - upper_bounds = - Bounds.add_baggage ~modality ~deep_only:true ~baggage:type_ - base.upper_bounds + upper_bounds = base.upper_bounds; + with_bounds = + With_bounds.add ~modality ~deep_only:true ~type_expr:type_ + base.with_bounds }) | Default | Kind_of _ -> raise ~loc:jkind.pjkind_loc Unimplemented_syntax @@ -1230,7 +1061,7 @@ module Const = struct let get_required_layouts_level (_context : 'd Context_with_transl.t) (jkind : 'd t) = let rec scan_layout (l : Layout.Const.t) : Language_extension.maturity = - match l, jkind.upper_bounds.nullability.modifier with + match l, jkind.upper_bounds.nullability with | (Base (Float64 | Float32 | Word | Bits32 | Bits64 | Vec128) | Any), _ | Base Value, Non_null -> Stable @@ -1288,47 +1119,54 @@ module Jkind_desc = struct let add_nullability_crossing t = { t with - upper_bounds = - { t.upper_bounds with nullability = Bound.simple Nullability.min } + upper_bounds = { t.upper_bounds with nullability = Nullability.min } } - let add_portability_and_contention_crossing ~type_equal ~jkind_of_type ~from - to_ = - let add_crossing (type a) ~(axis : a Axis.t) to_ = + let add_portability_and_contention_crossing ~from to_ = + let add_crossing (type a) ~(axis : a Axis.t) ~constant_modality bounds + with_bounds = let (module A : Lattice with type t = a) = Axis.get axis in let from_bound = Bounds.get ~axis from.upper_bounds in - let to_bound = Bounds.get ~axis to_ in + let to_bound = Bounds.get ~axis bounds in let new_bound = (* Only do this when the new mode is less than the old one. We - don't want to discard baggage if the new one is greater than + don't want to discard with_bounds if the new one is greater than the old one. *) - if A.le from_bound.modifier to_bound.modifier - (* This discards any baggage, but that's what we want when doing illegal - crossing. *) - then Bound.simple from_bound.modifier - else to_bound + if A.le from_bound to_bound then from_bound else to_bound in let added_crossings = - not - (Misc.Le_result.is_le - (Bound.less_or_equal ~axis ~type_equal ~jkind_of_type to_bound - from_bound)) + match axis with + | Modal axis -> not (Mode.Alloc.Const.is_max axis from_bound) + | Nonmodal _ -> false + in + let with_bounds = + if added_crossings + then With_bounds.compose_modality with_bounds ~then_:constant_modality + else with_bounds in - Bounds.set ~axis to_ new_bound, added_crossings + Bounds.set ~axis bounds new_bound, with_bounds, added_crossings in - let upper_bounds = to_.upper_bounds in - let upper_bounds, added1 = - add_crossing ~axis:(Modal (Comonadic Portability)) upper_bounds + let { with_bounds; upper_bounds; _ } = to_ in + let upper_bounds, with_bounds, added1 = + add_crossing ~axis:(Modal (Comonadic Portability)) + ~constant_modality: + (Mode.Modality.Atom + (Comonadic Portability, Meet_with Mode.Portability.Const.Portable)) + upper_bounds with_bounds in - let upper_bounds, added2 = - add_crossing ~axis:(Modal (Monadic Contention)) upper_bounds + let upper_bounds, with_bounds, added2 = + add_crossing ~axis:(Modal (Monadic Contention)) + ~constant_modality: + (Mode.Modality.Atom + (Monadic Contention, Join_with Mode.Contention.Const.Contended)) + upper_bounds with_bounds in - { to_ with upper_bounds }, added1 || added2 + { to_ with upper_bounds; with_bounds }, added1 || added2 - let add_baggage ~deep_only ~baggage ~modality t = + let add_with_bounds ~deep_only ~type_expr ~modality t = { t with - upper_bounds = - Bounds.add_baggage ~deep_only ~baggage ~modality t.upper_bounds + with_bounds = + With_bounds.add ~deep_only ~type_expr ~modality t.with_bounds } let max = of_const Const.max @@ -1336,24 +1174,58 @@ module Jkind_desc = struct let equate_or_equal ~allow_mutation t1 t2 = Layout_and_axes.equal (Layout.equate_or_equal ~allow_mutation) t1 t2 - let sub ~type_equal ~jkind_of_type { layout = lay1; upper_bounds = bounds1 } - { layout = lay2; upper_bounds = bounds2 } = - Misc.Le_result.combine (Layout.sub lay1 lay2) - (Bounds.less_or_equal ~type_equal ~jkind_of_type bounds1 bounds2) + let sub (type l r) ~type_equal ~jkind_of_type + ({ layout = lay1; upper_bounds = bounds1; with_bounds = with_bounds1 } : + (allowed * r) t) + ({ layout = lay2; upper_bounds = bounds2; with_bounds = with_bounds2 } : + (l * allowed) t) = + let bounds = + (* CR aspsmith: iterating axis-first here (specifically for With_bounds.reduce) + rather than type-first is probably the wrong choice; this is an artifact of when + baggage was per-axis and should (eventually) be re-thought for the purposes of + finding better asymptotics. + *) + Axis.all + |> List.map (fun (Axis.Pack axis) : Misc.Le_result.t -> + let (module Axis_ops) = Axis.get axis in + let bound1 = Bounds.get ~axis bounds1 in + let bound2 = Bounds.get ~axis bounds2 in + match with_bounds1, with_bounds2 with + | No_with_bounds, No_with_bounds -> + Axis_ops.less_or_equal bound1 bound2 + (* CR layouts v2.8: This should expand types on the left. *) + | (With_bounds (_, _) as wbs), No_with_bounds -> + if Axis_ops.le Axis_ops.max bound2 + then Less + else + let bound1_extended = + With_bounds.extend_bound ~type_equal ~jkind_of_type ~axis + ~bound:bound1 wbs + in + Axis_ops.less_or_equal bound1_extended bound2) + |> Misc.Le_result.combine_list + in + Misc.Le_result.combine (Layout.sub lay1 lay2) bounds - let intersection { layout = lay1; upper_bounds = bounds1 } - { layout = lay2; upper_bounds = bounds2 } = + let intersection + { layout = lay1; upper_bounds = bounds1; with_bounds = with_bounds1 } + { layout = lay2; upper_bounds = bounds2; with_bounds = with_bounds2 } = match Layout.intersection lay1 lay2 with | None -> None - | Some layout -> Some { layout; upper_bounds = Bounds.meet bounds1 bounds2 } + | Some layout -> + Some + { layout; + upper_bounds = Bounds.meet bounds1 bounds2; + with_bounds = With_bounds.meet with_bounds1 with_bounds2 + } let map_type_expr f t = Layout_and_axes.map_type_expr f t let of_new_sort_var nullability_upper_bound = let layout, sort = Layout.of_new_sort_var () in ( { layout; - upper_bounds = - { Bounds.max with nullability = Bound.simple nullability_upper_bound } + upper_bounds = { Bounds.max with nullability = nullability_upper_bound }; + with_bounds = No_with_bounds }, sort ) @@ -1382,14 +1254,14 @@ module Jkind_desc = struct | [_] -> (jkind_of_first_type ()).jkind | _ -> let layout = Layout.product layouts in - let upper_bounds = + let upper_bounds = Bounds.min in + let with_bounds = List.fold_right - (fun (ty, modality) bounds -> - Bounds.add_baggage ~deep_only:false ~baggage:ty bounds ~modality) - tys_modalities - (Bounds.min |> Bounds.disallow_right) + (fun (type_expr, modality) bounds -> + With_bounds.add ~deep_only:false ~type_expr ~modality bounds) + tys_modalities Jkind_types.With_bounds.No_with_bounds in - { layout; upper_bounds } + { layout; upper_bounds; with_bounds } let get t = Layout_and_axes.map Layout.get t @@ -1474,7 +1346,7 @@ module Builtin = struct (List.init arity (fun _ -> fst (Layout.of_new_sort_var ()))) in let desc : _ Jkind_desc.t = - { layout; upper_bounds = Bounds.max |> Bounds.disallow_right } + { layout; upper_bounds = Bounds.max; with_bounds = No_with_bounds } in fresh_jkind_poly desc ~annotation:None ~why:(Product_creation why) end @@ -1482,20 +1354,24 @@ end let add_nullability_crossing t = { t with jkind = Jkind_desc.add_nullability_crossing t.jkind } -let add_baggage ~modality ~baggage t = +let add_with_bounds ~modality ~type_expr t = { t with - jkind = Jkind_desc.add_baggage ~deep_only:true ~baggage ~modality t.jkind + jkind = + Jkind_desc.add_with_bounds ~deep_only:true ~type_expr ~modality t.jkind } -let has_baggage t = Bounds.has_baggage t.jkind.upper_bounds +let has_with_bounds (type l r) (t : (l * r) t) = + match t.jkind.with_bounds with + | No_with_bounds -> false + | With_bounds _ -> true -let add_portability_and_contention_crossing ~type_equal ~jkind_of_type ~from t = +let add_portability_and_contention_crossing ~from t = match try_allow_r from with | None -> t, false | Some from -> let jkind, added_crossings = - Jkind_desc.add_portability_and_contention_crossing ~type_equal - ~jkind_of_type ~from:from.jkind t.jkind + Jkind_desc.add_portability_and_contention_crossing ~from:from.jkind + t.jkind in { t with jkind }, added_crossings @@ -1584,10 +1460,10 @@ let all_void_labels lbls = (fun (lbl : Types.label_declaration) -> Sort.Const.(equal void lbl.ld_sort)) lbls -let add_labels_as_baggage lbls jkind = +let add_labels_as_with_bounds lbls jkind = List.fold_right (fun (lbl : Types.label_declaration) -> - add_baggage ~baggage:lbl.ld_type ~modality:lbl.ld_modalities) + add_with_bounds ~type_expr:lbl.ld_type ~modality:lbl.ld_modalities) lbls jkind let for_boxed_record lbls = @@ -1599,7 +1475,7 @@ let for_boxed_record lbls = (if is_mutable then Builtin.mutable_data else Builtin.immutable_data) ~why:Boxed_record in - add_labels_as_baggage lbls base + add_labels_as_with_bounds lbls base let for_unboxed_record ~jkind_of_type lbls = let open Types in @@ -1648,8 +1524,8 @@ let for_boxed_variant cstrs = in if has_gadt_constructor (* CR layouts v2.8: This is sad, but I don't know how to account for - existentials in the baggage. See doc named "Existential - baggage". *) + existentials in the with_bounds. See doc named "Existential + with_bounds". *) then Builtin.value ~why:Boxed_variant else let base = @@ -1661,9 +1537,9 @@ let for_boxed_variant cstrs = | Cstr_tuple args -> List.fold_right (fun arg -> - add_baggage ~modality:arg.ca_modalities ~baggage:arg.ca_type) + add_with_bounds ~modality:arg.ca_modalities ~type_expr:arg.ca_type) args jkind - | Cstr_record lbls -> add_labels_as_baggage lbls jkind + | Cstr_record lbls -> add_labels_as_with_bounds lbls jkind in List.fold_right add_cstr_args cstrs base @@ -1674,7 +1550,8 @@ let for_arrow = Bounds.simple ~linearity:Linearity.Const.max ~locality:Locality.Const.max ~uniqueness:Uniqueness.Const.min ~portability:Portability.Const.max ~contention:Contention.Const.min - ~externality:Externality.max ~nullability:Nullability.Non_null + ~externality:Externality.max ~nullability:Nullability.Non_null; + with_bounds = No_with_bounds } ~annotation:None ~why:(Value_creation Arrow) @@ -1693,7 +1570,8 @@ let for_object = { layout = Sort (Base Value); upper_bounds = Bounds.simple ~linearity ~locality ~uniqueness ~portability ~contention - ~externality:Externality.max ~nullability:Non_null + ~externality:Externality.max ~nullability:Non_null; + with_bounds = No_with_bounds } ~annotation:None ~why:(Value_creation Object) @@ -1724,37 +1602,33 @@ let get_layout jk : Layout.Const.t option = Layout.get_const jk.jkind.layout let extract_layout jk = jk.jkind.layout +let upper_bound_for_axis (type a) ~type_equal ~jkind_of_type ~(axis : a Axis.t) + jk = + With_bounds.extend_bound ~axis ~type_equal ~jkind_of_type + ~bound:(Bounds.get jk.jkind.upper_bounds ~axis) + jk.jkind.with_bounds + 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 (Comonadic Areality)) ~type_equal ~jkind_of_type - bounds.locality; - linearity = - Bound.reduce ~axis:(Modal (Comonadic Linearity)) ~type_equal - ~jkind_of_type bounds.linearity; - uniqueness = - Bound.reduce ~axis:(Modal (Monadic Uniqueness)) ~type_equal ~jkind_of_type - bounds.uniqueness; - portability = - Bound.reduce ~axis:(Modal (Comonadic Portability)) ~type_equal - ~jkind_of_type bounds.portability; - contention = - Bound.reduce ~axis:(Modal (Monadic Contention)) ~type_equal ~jkind_of_type - bounds.contention + let upper_bound_for_axis (type a) (axis : a Axis.t) = + upper_bound_for_axis ~type_equal ~jkind_of_type ~axis jk + in + { areality = upper_bound_for_axis (Modal (Comonadic Areality)); + linearity = upper_bound_for_axis (Modal (Comonadic Linearity)); + uniqueness = upper_bound_for_axis (Modal (Monadic Uniqueness)); + portability = upper_bound_for_axis (Modal (Comonadic Portability)); + contention = upper_bound_for_axis (Modal (Monadic Contention)) } let get_externality_upper_bound ~type_equal ~jkind_of_type jk = - Bound.reduce ~axis:(Nonmodal Externality) ~type_equal ~jkind_of_type - jk.jkind.upper_bounds.externality + upper_bound_for_axis ~type_equal ~jkind_of_type ~axis:(Nonmodal Externality) + jk let set_externality_upper_bound jk externality_upper_bound = { jk with jkind = { jk.jkind with upper_bounds = - { jk.jkind.upper_bounds with - externality = Bound.simple externality_upper_bound - } + { jk.jkind.upper_bounds with externality = externality_upper_bound } } } @@ -2338,16 +2212,15 @@ let intersection_or_error ~type_equal ~jkind_of_type ~reason t1 t2 = has_warned = t1.has_warned || t2.has_warned } -let round_up ~type_equal ~jkind_of_type t = +let round_up (type l r) ~type_equal ~jkind_of_type (t : (allowed * r) t) : + (l * allowed) t = let upper_bounds = - Bounds.Map.f + Bounds.Create.f { f = - (fun ~axis bound -> - Bound.simple (Bound.reduce ~axis ~type_equal ~jkind_of_type bound)) + (fun ~axis -> upper_bound_for_axis ~type_equal ~jkind_of_type ~axis t) } - t.jkind.upper_bounds in - { t with jkind = { t.jkind with upper_bounds } } + { t with jkind = { t.jkind with upper_bounds; with_bounds = No_with_bounds } } let map_type_expr f t = { t with jkind = Jkind_desc.map_type_expr f t.jkind } @@ -2402,31 +2275,34 @@ let sub_jkind_l ~type_equal ~jkind_of_type sub super = Misc.Le_result.is_le (Layout.sub sub.jkind.layout super.jkind.layout) in let bounds = - Bounds.Fold2.f - { f = - (fun (type axis) ~(axis : axis Axis.t) (bound1 : _ Bound.t) - (bound2 : _ Bound.t) -> - (* Maybe an individual axis has the right shape on the right; - try this again before doing the stupid equality check. *) - match Bound.try_allow_r bound2 with - | Some bound2 -> - Misc.Le_result.is_le - (Bound.less_or_equal ~axis ~type_equal ~jkind_of_type bound1 - bound2) - | None -> - let (module Bound_ops) = Axis.get axis in - let baggage1 = Baggage.as_list bound1.baggage in - let baggage2 = Baggage.as_list bound2.baggage in - let modifiers = - Bound_ops.equal bound1.modifier bound2.modifier - in - let baggages = - List.compare_lengths baggage1 baggage2 = 0 - && List.for_all2 type_equal baggage1 baggage2 - in - modifiers && baggages) - } - ~combine:( && ) sub.jkind.upper_bounds super.jkind.upper_bounds + List.for_all + (fun (Axis.Pack axis) -> + let (module Axis_ops) = Axis.get axis in + let bound1 = Bounds.get ~axis sub.jkind.upper_bounds in + let bound2 = Bounds.get ~axis super.jkind.upper_bounds in + (* Maybe an individual axis has the right shape on the right; + try this again before doing the stupid equality check. *) + if Axis_ops.le Axis_ops.max bound2 + then true + else + match With_bounds.types_on_axis ~axis super.jkind.with_bounds with + | [] -> + let bound1' = + With_bounds.extend_bound ~type_equal ~jkind_of_type ~axis + ~bound:bound1 sub.jkind.with_bounds + in + Axis_ops.less_or_equal bound1' bound2 |> Misc.Le_result.is_le + | with_bounds2 -> + let with_bounds1 = + With_bounds.types_on_axis ~axis sub.jkind.with_bounds + in + let modifiers = Axis_ops.equal bound1 bound2 in + let with_bounds = + List.compare_lengths with_bounds1 with_bounds2 = 0 + && List.for_all2 type_equal with_bounds1 with_bounds2 + in + modifiers && with_bounds) + Axis.all in if layouts && bounds then success else failure @@ -2460,13 +2336,11 @@ let is_value_for_printing { jkind; _ } = else { value with upper_bounds = - { value.upper_bounds with - nullability = Bound.simple Nullability.Maybe_null - } + { value.upper_bounds with nullability = Nullability.Maybe_null } } :: values in - List.exists (fun v -> Const.no_baggage_and_equal const v) values + List.exists (fun v -> Const.no_with_bounds_and_equal const v) values (*********************************) (* debugging *) @@ -2652,11 +2526,13 @@ module Debug_printers = struct a (history ~print_type_expr) h module Const = struct - let t ~print_type_expr ppf (jkind : _ Const.t) = - fprintf ppf "@[{ layout = %a@,; modes_upper_bounds = %a@,}@]" - Layout.Const.Debug_printers.t jkind.layout - (Bounds.debug_print ~print_type_expr) - jkind.upper_bounds + let t ~print_type_expr ppf + ({ layout; upper_bounds; with_bounds } : _ Const.t) = + fprintf ppf + "@[{ layout = %a@,; upper_bounds = %a@,; with_bounds = %a@, }@]" + Layout.Const.Debug_printers.t layout Bounds.debug_print upper_bounds + (With_bounds.debug_print ~print_type_expr) + with_bounds end end @@ -2696,11 +2572,6 @@ let report_error ~loc : Error.t -> _ = function Pprintast.jkind_annotation jkind hint) | Unimplemented_syntax -> Location.errorf ~loc "@[Unimplemented kind syntax@]" - | Modded_bound_with_baggage_constraints axis -> - Location.errorf ~loc - "Attempted to 'mod' a kind along the %s axis, which has already been \ - constrained with a 'with' constraint." - (Axis.name axis) | With_on_right -> Location.errorf ~loc "'with' syntax is not allowed on a right mode." diff --git a/typing/jkind.mli b/typing/jkind.mli index 6ad46e3b82d..0424350dbea 100644 --- a/typing/jkind.mli +++ b/typing/jkind.mli @@ -207,12 +207,12 @@ module Const : sig val to_out_jkind_const : 'd t -> Outcometree.out_jkind_const - (** This returns [true] iff both types have no baggage and they are equal. + (** This returns [true] iff both types have no with-bounds and they are equal. Normally, we want an equality check to happen only on values that are - allowed on both the left and the right. But a type with no baggage is + allowed on both the left and the right. But a type with no with-bounds is allowed on the left and the right, so we test for that condition first before doing the proper equality check. *) - val no_baggage_and_equal : 'd1 t -> 'd2 t -> bool + val no_with_bounds_and_equal : 'd1 t -> 'd2 t -> bool (* CR layouts: Remove this once we have a better story for printing with jkind abbreviations. *) @@ -328,25 +328,21 @@ end (** Take an existing [t] and add an ability to cross across the nullability axis. *) val add_nullability_crossing : 'd t -> 'd t -(** Take an existing [jkind_l] and add some baggage. *) -val add_baggage : +(** Take an existing [jkind_l] and add some with-bounds. *) +val add_with_bounds : modality:Mode.Modality.Value.Const.t -> - baggage:Types.type_expr -> + type_expr:Types.type_expr -> jkind_l -> jkind_l -(** Does this jkind have baggage? *) -val has_baggage : jkind_l -> bool +(** Does this jkind have with-bounds? *) +val has_with_bounds : jkind_l -> bool (** Take an existing [t] and add an ability to mode-cross along the portability and contention axes, if [from] crosses the respective axes. Return the new jkind, along with a boolean of whether illegal crossing was added *) val add_portability_and_contention_crossing : - type_equal:(Types.type_expr -> Types.type_expr -> bool) -> - jkind_of_type:(Types.type_expr -> jkind_l option) -> - from:'d t -> - (allowed * 'r) t -> - (allowed * 'r) t * bool + from:'d t -> (allowed * 'r) t -> (allowed * 'r) t * bool (******************************) (* construction *) diff --git a/typing/jkind_axis.ml b/typing/jkind_axis.ml index 243e5196a72..f46a15b4577 100644 --- a/typing/jkind_axis.ml +++ b/typing/jkind_axis.ml @@ -167,209 +167,269 @@ module Axis = struct end module type Axed = sig - type (+'type_expr, 'd, 'axis) t constraint 'd = 'l * 'r + type 'axis t end -(* Sadly this needs to be functorized since we don't have higher-kinded types *) -module Axis_collection (T : Axed) = struct - type (+'type_expr, 'd) t = - { locality : ('type_expr, 'd, Mode.Locality.Const.t) T.t; - linearity : ('type_expr, 'd, Mode.Linearity.Const.t) T.t; - uniqueness : ('type_expr, 'd, Mode.Uniqueness.Const.t) T.t; - portability : ('type_expr, 'd, Mode.Portability.Const.t) T.t; - contention : ('type_expr, 'd, Mode.Contention.Const.t) T.t; - externality : ('type_expr, 'd, Externality.t) T.t; - nullability : ('type_expr, 'd, Nullability.t) T.t +module Axis_collection = struct + type 'a t = + { locality : 'a; + linearity : 'a; + uniqueness : 'a; + portability : 'a; + contention : 'a; + externality : 'a; + nullability : 'a + } + + let create ~(f : axis:Axis.packed -> _) = + { locality = f ~axis:(Pack (Modal (Comonadic Areality))); + linearity = f ~axis:(Pack (Modal (Comonadic Linearity))); + uniqueness = f ~axis:(Pack (Modal (Monadic Uniqueness))); + portability = f ~axis:(Pack (Modal (Comonadic Portability))); + contention = f ~axis:(Pack (Modal (Monadic Contention))); + externality = f ~axis:(Pack (Nonmodal Externality)); + nullability = f ~axis:(Pack (Nonmodal Nullability)) } - let get (type a) ~(axis : a Axis.t) values : (_, _, a) T.t = + let get (type a) ~(axis : a Axis.t) t = match axis with - | 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 - | Nonmodal Externality -> values.externality - | Nonmodal Nullability -> values.nullability - - let set (type a) ~(axis : a Axis.t) values (value : (_, _, a) T.t) = + | Modal (Comonadic Areality) -> t.locality + | Modal (Comonadic Linearity) -> t.linearity + | Modal (Monadic Uniqueness) -> t.uniqueness + | Modal (Comonadic Portability) -> t.portability + | Modal (Monadic Contention) -> t.contention + | Nonmodal Externality -> t.externality + | Nonmodal Nullability -> t.nullability + + let set (type a) ~(axis : a Axis.t) t value = match axis with - | 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 } - | Nonmodal Externality -> { values with externality = value } - | Nonmodal Nullability -> { values with nullability = value } - - (* Since we don't have polymorphic parameters, use a record to pass the - polymorphic function *) - module Create = struct - module Monadic (M : Misc.Stdlib.Monad.S) = struct - type ('type_expr, 'd) f = - { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t M.t } - [@@unboxed] + | Modal (Comonadic Areality) -> { t with locality = value } + | Modal (Comonadic Linearity) -> { t with linearity = value } + | Modal (Monadic Uniqueness) -> { t with uniqueness = value } + | Modal (Comonadic Portability) -> { t with portability = value } + | Modal (Monadic Contention) -> { t with contention = value } + | Nonmodal Externality -> { t with externality = value } + | Nonmodal Nullability -> { t with nullability = value } + + let map ~(f : axis:Axis.packed -> _ -> _) + { locality; + linearity; + uniqueness; + portability; + contention; + externality; + nullability + } = + { locality = f ~axis:(Pack (Modal (Comonadic Areality))) locality; + linearity = f ~axis:(Pack (Modal (Comonadic Linearity))) linearity; + uniqueness = f ~axis:(Pack (Modal (Monadic Uniqueness))) uniqueness; + portability = f ~axis:(Pack (Modal (Comonadic Portability))) portability; + contention = f ~axis:(Pack (Modal (Monadic Contention))) contention; + externality = f ~axis:(Pack (Nonmodal Externality)) externality; + nullability = f ~axis:(Pack (Nonmodal Nullability)) nullability + } - let[@inline] f { f } = - let open M.Syntax 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* externality = f ~axis:Axis.(Nonmodal Externality) in - let* nullability = f ~axis:Axis.(Nonmodal Nullability) in - M.return - { locality; - uniqueness; - linearity; - contention; - portability; - externality; - nullability - } + let map' ~f = map ~f:(fun ~axis:_ x -> f x) + + let fold ~(f : axis:Axis.packed -> _ -> _) ~combine + { locality; + linearity; + uniqueness; + portability; + contention; + externality; + nullability + } = + combine (f ~axis:(Pack (Modal (Comonadic Areality))) locality) + @@ combine (f ~axis:(Pack (Modal (Comonadic Linearity))) uniqueness) + @@ combine (f ~axis:(Pack (Modal (Monadic Uniqueness))) linearity) + @@ combine (f ~axis:(Pack (Modal (Comonadic Portability))) contention) + @@ combine (f ~axis:(Pack (Modal (Monadic Contention))) portability) + @@ combine (f ~axis:(Pack (Nonmodal Externality)) externality) + @@ f ~axis:(Pack (Nonmodal Nullability)) nullability + + (* Sadly this needs to be functorized since we don't have higher-kinded types *) + module Indexed (T : Axed) = struct + type t = + { locality : Mode.Locality.Const.t T.t; + linearity : Mode.Linearity.Const.t T.t; + uniqueness : Mode.Uniqueness.Const.t T.t; + portability : Mode.Portability.Const.t T.t; + contention : Mode.Contention.Const.t T.t; + externality : Externality.t T.t; + nullability : Nullability.t T.t + } + + let get (type a) ~(axis : a Axis.t) values : a T.t = + match axis with + | 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 + | 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 (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 } + | Nonmodal Externality -> { values with externality = value } + | Nonmodal Nullability -> { values with nullability = value } + + (* Since we don't have polymorphic parameters, use a record to pass the + polymorphic function *) + module Create = struct + module Monadic (M : Misc.Stdlib.Monad.S) = struct + type f = { f : 'axis. axis:'axis Axis.t -> 'axis T.t M.t } [@@unboxed] + + let[@inline] f { f } = + let open M.Syntax 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* externality = f ~axis:Axis.(Nonmodal Externality) in + let* nullability = f ~axis:Axis.(Nonmodal Nullability) in + M.return + { locality; + uniqueness; + linearity; + contention; + portability; + externality; + nullability + } + end + [@@inline] + + module Monadic_identity = Monadic (Misc.Stdlib.Monad.Identity) + + type f = Monadic_identity.f + + let[@inline] f f = Monadic_identity.f f end - [@@inline] - module Monadic_identity = Monadic (Misc.Stdlib.Monad.Identity) + module Map = struct + module Monadic (M : Misc.Stdlib.Monad.S) = struct + type f = { f : 'axis. axis:'axis Axis.t -> 'axis T.t -> 'axis T.t M.t } + [@@unboxed] - type ('type_expr, 'd) f = ('type_expr, 'd) Monadic_identity.f + module Create = Create.Monadic (M) - let[@inline] f f = Monadic_identity.f f - end + let[@inline] f { f } bounds = + Create.f { f = (fun ~axis -> f ~axis (get ~axis bounds)) } + end + [@@inline] - module Map = struct - module Monadic (M : Misc.Stdlib.Monad.S) = struct - type ('type_expr, 'd1, 'd2) f = - { f : - 'axis. - axis:'axis Axis.t -> - ('type_expr, 'd1, 'axis) T.t -> - ('type_expr, 'd2, 'axis) T.t M.t - } - [@@unboxed] + module Monadic_identity = Monadic (Misc.Stdlib.Monad.Identity) - module Create = Create.Monadic (M) + type f = Monadic_identity.f - let[@inline] f { f } bounds = - Create.f { f = (fun ~axis -> f ~axis (get ~axis bounds)) } + let[@inline] f f bounds = Monadic_identity.f f bounds end - [@@inline] - module Monadic_identity = Monadic (Misc.Stdlib.Monad.Identity) + module Iter = struct + type f = { f : 'axis. axis:'axis Axis.t -> 'axis T.t -> unit } + + let[@inline] f { f } + { locality; + linearity; + uniqueness; + portability; + contention; + externality; + nullability + } = + f ~axis:Axis.(Modal (Comonadic Areality)) locality; + f ~axis:Axis.(Modal (Monadic Uniqueness)) uniqueness; + f ~axis:Axis.(Modal (Comonadic Linearity)) linearity; + f ~axis:Axis.(Modal (Monadic Contention)) contention; + f ~axis:Axis.(Modal (Comonadic Portability)) portability; + f ~axis:Axis.(Nonmodal Externality) externality; + f ~axis:Axis.(Nonmodal Nullability) nullability + end - type ('type_expr, 'd1, 'd2) f = ('type_expr, 'd1, 'd2) Monadic_identity.f + module Map2 = struct + module Monadic (M : Misc.Stdlib.Monad.S) = struct + type f = + { f : + 'axis. + axis:'axis Axis.t -> 'axis T.t -> 'axis T.t -> 'axis T.t M.t + } + [@@unboxed] - let[@inline] f f bounds = Monadic_identity.f f bounds - end + module Create = Create.Monadic (M) - module Iter = struct - type ('type_expr, 'd) f = - { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t -> unit } - - let[@inline] f { f } - { locality; - linearity; - uniqueness; - portability; - contention; - externality; - nullability - } = - f ~axis:Axis.(Modal (Comonadic Areality)) locality; - f ~axis:Axis.(Modal (Monadic Uniqueness)) uniqueness; - f ~axis:Axis.(Modal (Comonadic Linearity)) linearity; - f ~axis:Axis.(Modal (Monadic Contention)) contention; - f ~axis:Axis.(Modal (Comonadic Portability)) portability; - f ~axis:Axis.(Nonmodal Externality) externality; - f ~axis:Axis.(Nonmodal Nullability) nullability - end + let[@inline] f { f } bounds1 bounds2 = + Create.f + { f = (fun ~axis -> f ~axis (get ~axis bounds1) (get ~axis bounds2)) + } + end + [@@inline] - module Map2 = struct - module Monadic (M : Misc.Stdlib.Monad.S) = struct - type ('type_expr, 'd1, 'd2, 'd3) f = - { f : - 'axis. - axis:'axis Axis.t -> - ('type_expr, 'd1, 'axis) T.t -> - ('type_expr, 'd2, 'axis) T.t -> - ('type_expr, 'd3, 'axis) T.t M.t - } - [@@unboxed] + module Monadic_identity = Monadic (Misc.Stdlib.Monad.Identity) - module Create = Create.Monadic (M) + type f = Monadic_identity.f - let[@inline] f { f } bounds1 bounds2 = - Create.f - { f = (fun ~axis -> f ~axis (get ~axis bounds1) (get ~axis bounds2)) } + let[@inline] f f bounds1 bounds2 = Monadic_identity.f f bounds1 bounds2 end - [@@inline] - - module Monadic_identity = Monadic (Misc.Stdlib.Monad.Identity) - type ('type_expr, 'd1, 'd2, 'd3) f = - ('type_expr, 'd1, 'd2, 'd3) Monadic_identity.f + module Fold = struct + type 'r f = { f : 'axis. axis:'axis Axis.t -> 'axis T.t -> 'r } + [@@unboxed] - let[@inline] f f bounds1 bounds2 = Monadic_identity.f f bounds1 bounds2 - end + let[@inline] f { f } + { locality; + linearity; + uniqueness; + portability; + contention; + externality; + nullability + } ~combine = + 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.(Nonmodal Externality) externality) + @@ f ~axis:Axis.(Nonmodal Nullability) nullability + end - module Fold = struct - type ('type_expr, 'd, 'r) f = - { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t -> 'r } - [@@unboxed] - - let[@inline] f { f } - { locality; - linearity; - uniqueness; - portability; - contention; - externality; - nullability - } ~combine = - 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.(Nonmodal Externality) externality) - @@ f ~axis:Axis.(Nonmodal Nullability) nullability - end + module Fold2 = struct + type 'r f = + { f : 'axis. axis:'axis Axis.t -> 'axis T.t -> 'axis T.t -> 'r } + [@@unboxed] - module Fold2 = struct - type ('type_expr, 'd1, 'd2, 'r) f = - { f : - 'axis. - axis:'axis Axis.t -> - ('type_expr, 'd1, 'axis) T.t -> - ('type_expr, 'd2, 'axis) T.t -> - 'r - } - [@@unboxed] - - let[@inline] f { f } - { locality = loc1; - linearity = lin1; - uniqueness = uni1; - portability = por1; - contention = con1; - externality = ext1; - nullability = nul1 - } - { locality = loc2; - linearity = lin2; - uniqueness = uni2; - portability = por2; - contention = con2; - externality = ext2; - nullability = nul2 - } ~combine = - 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.(Nonmodal Externality) ext1 ext2) - @@ f ~axis:Axis.(Nonmodal Nullability) nul1 nul2 + let[@inline] f { f } + { locality = loc1; + linearity = lin1; + uniqueness = uni1; + portability = por1; + contention = con1; + externality = ext1; + nullability = nul1 + } + { locality = loc2; + linearity = lin2; + uniqueness = uni2; + portability = por2; + contention = con2; + externality = ext2; + nullability = nul2 + } ~combine = + 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.(Nonmodal Externality) ext1 ext2) + @@ f ~axis:Axis.(Nonmodal Nullability) nul1 nul2 + end end end diff --git a/typing/jkind_axis.mli b/typing/jkind_axis.mli index 06be5fdbc82..3253e0d9bd6 100644 --- a/typing/jkind_axis.mli +++ b/typing/jkind_axis.mli @@ -66,145 +66,120 @@ end (** [Axed] describes a type that is parameterized by axis. *) module type Axed = sig - type (+'type_expr, 'd, 'axis) t constraint 'd = 'l * 'r + type 'axis t end -(** A collection with one item for each jkind axis. - [T] parametrizes what element is being held for each axis. *) -module Axis_collection (T : Axed) : sig - (** [t] is parameterized over 'type_expr to enable usages in - [jkind_types.mli]. It is tempting to make those usages instead push the - [`type_expr] into the functor arg [T], but this leads to issues at - usages of [Jkind.t] in [types.mli] due to recursive definitions. *) - type (+'type_expr, 'd) t = - { locality : ('type_expr, 'd, Mode.Locality.Const.t) T.t; - linearity : ('type_expr, 'd, Mode.Linearity.Const.t) T.t; - uniqueness : ('type_expr, 'd, Mode.Uniqueness.Const.t) T.t; - portability : ('type_expr, 'd, Mode.Portability.Const.t) T.t; - contention : ('type_expr, 'd, Mode.Contention.Const.t) T.t; - externality : ('type_expr, 'd, Externality.t) T.t; - nullability : ('type_expr, 'd, Nullability.t) T.t +(** A collection with one item for each jkind axis *) +module Axis_collection : sig + type 'a t = + { locality : 'a; + linearity : 'a; + uniqueness : 'a; + portability : 'a; + contention : 'a; + externality : 'a; + nullability : 'a } - val get : axis:'a Axis.t -> ('type_expr, 'd) t -> ('type_expr, 'd, 'a) T.t + val create : f:(axis:Axis.packed -> 'a) -> 'a t - val set : - axis:'a Axis.t -> - ('type_expr, 'd) t -> - ('type_expr, 'd, 'a) T.t -> - ('type_expr, 'd) t + val get : axis:'ax Axis.t -> 'a t -> 'a - (** Create an axis collection by applying the function on each axis *) - module Create : sig - module Monadic (M : Misc.Stdlib.Monad.S) : sig - type ('type_expr, 'd) f = - { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t M.t } - [@@unboxed] + val set : axis:'ax Axis.t -> 'a t -> 'a -> 'a t + + val map : f:(axis:Axis.packed -> 'a -> 'a) -> 'a t -> 'a t + + val map' : f:('a -> 'a) -> 'a t -> 'a t + + val fold : + f:(axis:Axis.packed -> 'a -> 'r) -> combine:('r -> 'r -> 'r) -> 'a t -> 'r + + (** A collection with one item for each jkind axis, where the value type is indexed by the + particular axis. *) + module Indexed (T : Axed) : sig + type t = + { locality : Mode.Locality.Const.t T.t; + linearity : Mode.Linearity.Const.t T.t; + uniqueness : Mode.Uniqueness.Const.t T.t; + portability : Mode.Portability.Const.t T.t; + contention : Mode.Contention.Const.t T.t; + externality : Externality.t T.t; + nullability : Nullability.t T.t + } - val f : ('type_expr, 'd) f -> ('type_expr, 'd) t M.t + val get : axis:'a Axis.t -> t -> 'a T.t + + val set : axis:'a Axis.t -> t -> 'a T.t -> t + + (** Create an axis collection by applying the function on each axis *) + module Create : sig + module Monadic (M : Misc.Stdlib.Monad.S) : sig + type f = { f : 'axis. axis:'axis Axis.t -> 'axis T.t M.t } [@@unboxed] + + val f : f -> t M.t + end + + (** This record type is used to pass a polymorphic function to [create] *) + type f = Monadic(Misc.Stdlib.Monad.Identity).f + + val f : f -> t end - (** This record type is used to pass a polymorphic function to [create] *) - type ('type_expr, 'd) f = - ('type_expr, 'd) Monadic(Misc.Stdlib.Monad.Identity).f + (** Map an operation over all the bounds *) + module Map : sig + module Monadic (M : Misc.Stdlib.Monad.S) : sig + type f = { f : 'axis. axis:'axis Axis.t -> 'axis T.t -> 'axis T.t M.t } + [@@unboxed] - val f : ('type_expr, 'd) f -> ('type_expr, 'd) t - end + val f : f -> t -> t M.t + end - (** Map an operation over all the bounds *) - module Map : sig - module Monadic (M : Misc.Stdlib.Monad.S) : sig - type ('type_expr, 'd1, 'd2) f = - { f : - 'axis. - axis:'axis Axis.t -> - ('type_expr, 'd1, 'axis) T.t -> - ('type_expr, 'd2, 'axis) T.t M.t - } - [@@unboxed] + type f = Monadic(Misc.Stdlib.Monad.Identity).f - val f : - ('type_expr, 'd1, 'd2) f -> - ('type_expr, 'd1) t -> - ('type_expr, 'd2) t M.t + val f : f -> t -> t end - type ('type_expr, 'd1, 'd2) f = - ('type_expr, 'd1, 'd2) Monadic(Misc.Stdlib.Monad.Identity).f + module Iter : sig + type f = { f : 'axis. axis:'axis Axis.t -> 'axis T.t -> unit } - val f : - ('type_expr, 'd1, 'd2) f -> ('type_expr, 'd1) t -> ('type_expr, 'd2) t - end + val f : f -> t -> unit + end - module Iter : sig - type ('type_expr, 'd) f = - { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t -> unit } + (** Map an operation over two sets of bounds *) + module Map2 : sig + module Monadic (M : Misc.Stdlib.Monad.S) : sig + type f = + { f : + 'axis. + axis:'axis Axis.t -> 'axis T.t -> 'axis T.t -> 'axis T.t M.t + } + [@@unboxed] - val f : ('type_expr, 'd) f -> ('type_expr, 'd) t -> unit - end + val f : f -> t -> t -> t M.t + end - (** Map an operation over two sets of bounds *) - module Map2 : sig - module Monadic (M : Misc.Stdlib.Monad.S) : sig - type ('type_expr, 'd1, 'd2, 'd3) f = - { f : - 'axis. - axis:'axis Axis.t -> - ('type_expr, 'd1, 'axis) T.t -> - ('type_expr, 'd2, 'axis) T.t -> - ('type_expr, 'd3, 'axis) T.t M.t - } - [@@unboxed] + type f = Monadic(Misc.Stdlib.Monad.Identity).f - val f : - ('type_expr, 'd1, 'd2, 'd3) f -> - ('type_expr, 'd1) t -> - ('type_expr, 'd2) t -> - ('type_expr, 'd3) t M.t + val f : f -> t -> t -> t end - type ('type_expr, 'd1, 'd2, 'd3) f = - ('type_expr, 'd1, 'd2, 'd3) Monadic(Misc.Stdlib.Monad.Identity).f + (** Fold an operation over the bounds to a summary value *) + module Fold : sig + type 'r f = { f : 'axis. axis:'axis Axis.t -> 'axis T.t -> 'r } + [@@unboxed] - val f : - ('type_expr, 'd1, 'd2, 'd3) f -> - ('type_expr, 'd1) t -> - ('type_expr, 'd2) t -> - ('type_expr, 'd3) t - end + (** [combine] should be associative. *) + val f : 'r f -> t -> combine:('r -> 'r -> 'r) -> 'r + end - (** Fold an operation over the bounds to a summary value *) - module Fold : sig - type ('type_expr, 'd, 'r) f = - { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t -> 'r } - [@@unboxed] - - (** [combine] should be associative. *) - val f : - ('type_expr, 'd, 'r) f -> - ('type_expr, 'd) t -> - combine:('r -> 'r -> 'r) -> - 'r - end + (** Fold an operation over two sets of bounds to a summary value *) + module Fold2 : sig + type 'r f = + { f : 'axis. axis:'axis Axis.t -> 'axis T.t -> 'axis T.t -> 'r } + [@@unboxed] - (** Fold an operation over two sets of bounds to a summary value *) - module Fold2 : sig - type ('type_expr, 'd1, 'd2, 'r) f = - { f : - 'axis. - axis:'axis Axis.t -> - ('type_expr, 'd1, 'axis) T.t -> - ('type_expr, 'd2, 'axis) T.t -> - 'r - } - [@@unboxed] - - (** [combine] should be associative. *) - val f : - ('type_expr, 'd1, 'd2, 'r) f -> - ('type_expr, 'd1) t -> - ('type_expr, 'd2) t -> - combine:('r -> 'r -> 'r) -> - 'r + (** [combine] should be associative. *) + val f : 'r f -> t -> t -> combine:('r -> 'r -> 'r) -> 'r + end end end diff --git a/typing/jkind_types.ml b/typing/jkind_types.ml index 7dc25a57ffd..1a1f530371d 100644 --- a/typing/jkind_types.ml +++ b/typing/jkind_types.ml @@ -522,20 +522,58 @@ module Layout = struct end end -module Baggage = struct +module With_bounds = struct + module Type_info = struct + type +'type_expr t = + { type_expr : 'type_expr; + modality : Mode.Modality.Value.Const.t; + nullability : bool + } + + let print ~print_type_expr ppf { type_expr; modality } = + let open Format in + if Mode.Modality.Value.Const.is_id modality + then print_type_expr ppf type_expr + else + fprintf ppf "(@[%a@ @@@@ %a])" print_type_expr type_expr + Mode.Modality.Value.Const.print modality + + let map_type_expr f ({ type_expr; _ } as t) = + { t with type_expr = f type_expr } + + let is_on_axis (type a) ~(axis : a Jkind_axis.Axis.t) t = + match axis with + | Nonmodal Externality -> true (* All fields matter for externality *) + | Nonmodal Nullability -> t.nullability + | Modal axis -> + let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in + not + (Mode.Modality.Value.Const.proj axis t.modality + |> Mode.Modality.is_constant) + + let compose_modality t ~then_ = + let modality = Mode.Modality.Value.Const.compose t.modality ~then_ in + assert (not (Mode.Modality.Value.Const.is_id modality)); + { t with modality } + + let create ~type_expr ~modality ~deep_only = + { type_expr; modality; nullability = not deep_only } + end + type (+'type_expr, 'd) t = - | No_baggage : ('type_expr, 'l * 'r) t - | Baggage : - 'type_expr * 'type_expr list + | No_with_bounds : ('type_expr, 'l * 'r) t + (* There must always be at least one type. *) + | With_bounds : + 'type_expr Type_info.t * 'type_expr Type_info.t list -> ('type_expr, 'l * Allowance.disallowed) t let as_list : type l r. (_, l * r) t -> _ = function - | No_baggage -> [] - | Baggage (ty, tys) -> ty :: tys + | No_with_bounds -> [] + | With_bounds (ty, tys) -> ty :: tys - let has_baggage : type l r. (_, l * r) t -> _ = function - | No_baggage -> false - | Baggage _ -> true + let has_with_bounds : type l r. (_, l * r) t -> _ = function + | No_with_bounds -> false + | With_bounds _ -> true open Allowance @@ -545,134 +583,91 @@ module Baggage = struct let disallow_left : type l r. ('type_expr, l * r) t -> ('type_expr, disallowed * r) t = function - | No_baggage -> No_baggage - | Baggage _ as b -> b + | No_with_bounds -> No_with_bounds + | With_bounds _ as b -> b let disallow_right : type l r. ('type_expr, l * r) t -> ('type_expr, l * disallowed) t = function - | No_baggage -> No_baggage - | Baggage _ as b -> b + | No_with_bounds -> No_with_bounds + | With_bounds _ as b -> b let allow_left : type l r. ('type_expr, allowed * r) t -> ('type_expr, l * r) t = function - | No_baggage -> No_baggage - | Baggage _ as b -> b + | No_with_bounds -> No_with_bounds + | With_bounds _ as b -> b let allow_right : type l r. ('type_expr, l * allowed) t -> ('type_expr, l * r) t = function - | No_baggage -> No_baggage + | No_with_bounds -> No_with_bounds end) let try_allow_l : type l r. ('type_expr, l * r) t -> ('type_expr, allowed * r) t option = function - | No_baggage -> Some No_baggage - | Baggage _ as b -> Some b + | No_with_bounds -> Some No_with_bounds + | With_bounds _ as b -> Some b let try_allow_r : type l r. ('type_expr, l * r) t -> ('type_expr, l * allowed) t option = function - | No_baggage -> Some No_baggage - | Baggage _ -> None + | No_with_bounds -> Some No_with_bounds + | With_bounds _ -> None let map_type_expr (type l r) f : ('type_expr, l * r) t -> ('type_expr, l * r) t = function - | No_baggage -> No_baggage - | Baggage (ty, tys) -> Baggage (f ty, List.map f tys) + | No_with_bounds -> No_with_bounds + | With_bounds (ty, tys) -> + let f' = Type_info.map_type_expr f in + With_bounds (f' ty, List.map f' tys) + + let types_on_axis (type l r a) ~(axis : a Jkind_axis.Axis.t) : + (_, l * r) t -> _ = function + | No_with_bounds -> [] + | With_bounds (ti, tis) -> + List.filter_map + (fun (type_info : _ Type_info.t) -> + if Type_info.is_on_axis ~axis type_info + then Some type_info.type_expr + else None) + (ti :: tis) + + let compose_modality (type l r) ~then_ : (_, l * r) t -> (_, l * r) t = + function + | No_with_bounds -> No_with_bounds + | With_bounds (t, ts) -> + With_bounds + ( Type_info.compose_modality ~then_ t, + List.map (Type_info.compose_modality ~then_) ts ) let debug_print (type l r) ~print_type_expr ppf : (_, l * r) t -> _ = let open Format in function - | No_baggage -> fprintf ppf "No_baggage" - | Baggage (ty, tys) -> - fprintf ppf "Baggage @[[%a]@]" + | No_with_bounds -> fprintf ppf "No_with_bounds" + | With_bounds (ty, tys) -> + fprintf ppf "With_bounds @[[%a]@]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";@ ") - print_type_expr) + (Type_info.print ~print_type_expr)) (ty :: tys) end -module Bound = struct - open Allowance - - type (+'type_expr, 'd, 'a) t = - { modifier : 'a; - baggage : ('type_expr, 'd) Baggage.t - } - constraint 'd = 'l * 'r - - include Magic_allow_disallow (struct - type ('type_expr, 'a, 'd) sided = ('type_expr, 'd, 'a) t - - let disallow_left t = { t with baggage = Baggage.disallow_left t.baggage } - - let disallow_right t = { t with baggage = Baggage.disallow_right t.baggage } - - let allow_left t = { t with baggage = Baggage.allow_left t.baggage } - - let allow_right t = { t with baggage = Baggage.allow_right t.baggage } - end) - - let try_allow_l { modifier; baggage } = - match Baggage.try_allow_l baggage with - | Some baggage -> Some { modifier; baggage } - | None -> None - - let try_allow_r { modifier; baggage } = - match Baggage.try_allow_r baggage with - | Some baggage -> Some { modifier; baggage } - | None -> None - - let map_type_expr f t = { t with baggage = Baggage.map_type_expr f t.baggage } - - let equal : - _ -> (_, allowed * allowed, _) t -> (_, allowed * allowed, _) t -> bool = - fun eq_axis { modifier = m1; baggage = b1 } { modifier = m2; baggage = b2 } -> - match b1, b2 with No_baggage, No_baggage -> eq_axis m1 m2 - - let debug_print ~print_type_expr print_modifier ppf { modifier; baggage } = - Format.fprintf ppf "@[{ modifier = %a;@ baggage = %a }@]" print_modifier - modifier - (Baggage.debug_print ~print_type_expr) - baggage -end - module Bounds = struct open Jkind_axis - include Axis_collection (Bound) - - include Allowance.Magic_allow_disallow (struct - type ('type_expr, _, 'd) sided = ('type_expr, 'd) t - - let disallow_left bounds = - Map.f { f = (fun ~axis:_ bound -> Bound.disallow_left bound) } bounds - - let disallow_right bounds = - Map.f { f = (fun ~axis:_ bound -> Bound.disallow_right bound) } bounds - - let allow_left bounds = - Map.f { f = (fun ~axis:_ bound -> Bound.allow_left bound) } bounds - - let allow_right bounds = - Map.f { f = (fun ~axis:_ bound -> Bound.allow_right bound) } bounds - end) - - let map_type_expr f t = - Map.f { f = (fun ~axis:_ bound -> Bound.map_type_expr f bound) } t + include Axis_collection.Indexed (Misc.Stdlib.Monad.Identity) let equal bounds1 bounds2 = Fold2.f { f = (fun (type axis) ~(axis : axis Axis.t) bound1 bound2 -> let (module Bound_ops) = Axis.get axis in - Bound.equal Bound_ops.equal bound1 bound2) + Bound_ops.equal bound1 bound2) } ~combine:( && ) bounds1 bounds2 - let debug_print ~print_type_expr ppf + let debug_print ppf { locality; linearity; uniqueness; @@ -681,30 +676,20 @@ module Bounds = struct externality; nullability } = - let print_bound print_mod = Bound.debug_print ~print_type_expr print_mod in Format.fprintf ppf "@[{ locality = %a;@ linearity = %a;@ uniqueness = %a;@ portability = \ %a;@ contention = %a;@ externality = %a;@ nullability = %a }@]" - (print_bound Mode.Locality.Const.print) - locality - (print_bound Mode.Linearity.Const.print) - linearity - (print_bound Mode.Uniqueness.Const.print) - uniqueness - (print_bound Mode.Portability.Const.print) - portability - (print_bound Mode.Contention.Const.print) - contention - (print_bound Externality.print) - externality - (print_bound Nullability.print) - nullability + Mode.Locality.Const.print locality Mode.Linearity.Const.print linearity + Mode.Uniqueness.Const.print uniqueness Mode.Portability.Const.print + portability Mode.Contention.Const.print contention Externality.print + externality Nullability.print nullability end module Layout_and_axes = struct type ('type_expr, 'layout, 'd) t = { layout : 'layout; - upper_bounds : ('type_expr, 'd) Bounds.t + upper_bounds : Bounds.t; + with_bounds : ('type_expr, 'd) With_bounds.t } constraint 'd = 'l * 'r @@ -712,16 +697,16 @@ module Layout_and_axes = struct type ('type_expr, 'layout, 'd) sided = ('type_expr, 'layout, 'd) t let disallow_left t = - { t with upper_bounds = Bounds.disallow_left t.upper_bounds } + { t with with_bounds = With_bounds.disallow_left t.with_bounds } let disallow_right t = - { t with upper_bounds = Bounds.disallow_right t.upper_bounds } + { t with with_bounds = With_bounds.disallow_right t.with_bounds } let allow_left t = - { t with upper_bounds = Bounds.allow_left t.upper_bounds } + { t with with_bounds = With_bounds.allow_left t.with_bounds } let allow_right t = - { t with upper_bounds = Bounds.allow_right t.upper_bounds } + { t with with_bounds = With_bounds.allow_right t.with_bounds } end) include Allow_disallow @@ -732,37 +717,34 @@ module Layout_and_axes = struct match f t.layout with None -> None | Some layout -> Some { t with layout } let map_type_expr f t = - { t with upper_bounds = Bounds.map_type_expr f t.upper_bounds } + { t with with_bounds = With_bounds.map_type_expr f t.with_bounds } let equal eq_layout { layout = lay1; upper_bounds = bounds1 } { layout = lay2; upper_bounds = bounds2 } = eq_layout lay1 lay2 && Bounds.equal bounds1 bounds2 - let try_allow_l { layout; upper_bounds } = - let module Bounds_map_option = Bounds.Map.Monadic (Misc.Stdlib.Monad.Option) in - match - Bounds_map_option.f - { f = (fun ~axis:_ bound -> Bound.try_allow_l bound) } - upper_bounds - with - | Some upper_bounds -> Some { layout; upper_bounds } + let try_allow_l : + type l r. + ('type_expr, 'layout, l * r) t -> + ('type_expr, 'layout, Allowance.allowed * r) t option = + fun { layout; upper_bounds; with_bounds } -> + match With_bounds.try_allow_l with_bounds with | None -> None + | Some with_bounds -> + Some { layout; upper_bounds = Obj.magic upper_bounds; with_bounds } - let try_allow_r { layout; upper_bounds } = - let module Bounds_map_option = Bounds.Map.Monadic (Misc.Stdlib.Monad.Option) in - match - Bounds_map_option.f - { f = (fun ~axis:_ bound -> Bound.try_allow_r bound) } - upper_bounds - with - | Some upper_bounds -> Some { layout; upper_bounds } + let try_allow_r { layout; upper_bounds; with_bounds } = + match With_bounds.try_allow_r with_bounds with + | Some with_bounds -> + Some { layout; upper_bounds = Obj.magic upper_bounds; with_bounds } | None -> None - let debug_print ~print_type_expr format_layout ppf { layout; upper_bounds } = - Format.fprintf ppf "{ layout = %a;@ upper_bounds = %a }" format_layout - layout - (Bounds.debug_print ~print_type_expr) - upper_bounds + let debug_print ~print_type_expr format_layout ppf + { layout; upper_bounds; with_bounds } = + Format.fprintf ppf "{ layout = %a;@ upper_bounds = %a;@ with_bounds = %a }" + format_layout layout Bounds.debug_print upper_bounds + (With_bounds.debug_print ~print_type_expr) + with_bounds end module Jkind_desc = struct diff --git a/typing/jkind_types.mli b/typing/jkind_types.mli index 00346163e65..2a07b42bdc2 100644 --- a/typing/jkind_types.mli +++ b/typing/jkind_types.mli @@ -106,53 +106,61 @@ module Layout : sig end end -module Baggage : sig +module With_bounds : sig + module Type_info : sig + type +'type_expr t = + { type_expr : 'type_expr; + modality : Mode.Modality.Value.Const.t; + nullability : bool + } + + val create : + type_expr:'type_expr -> + modality:Mode.Modality.Value.Const.t -> + deep_only:bool -> + 'type_expr t + end + type (+'type_expr, 'd) t = - | No_baggage : ('type_expr, 'l * 'r) t + | No_with_bounds : ('type_expr, 'l * 'r) t (* There must always be at least one type. *) - | Baggage : - 'type_expr * 'type_expr list + | With_bounds : + 'type_expr Type_info.t * 'type_expr Type_info.t list -> ('type_expr, 'l * Allowance.disallowed) t - val as_list : ('type_expr, 'l * 'r) t -> 'type_expr list - - val has_baggage : ('type_expr, 'l * 'r) t -> bool -end - -module Bound : sig - open Allowance - - type (+'type_expr, 'd, 'a) t = - { modifier : 'a; - baggage : ('type_expr, 'd) Baggage.t - } - constraint 'd = 'l * 'r + include Allowance.Allow_disallow with type ('a, _, 'd) sided = ('a, 'd) t - val try_allow_l : - ('type_expr, 'l * 'r, 'a) t -> ('type_expr, allowed * 'r, 'a) t option + val as_list : ('type_expr, 'l * 'r) t -> 'type_expr Type_info.t list - val try_allow_r : - ('type_expr, 'l * 'r, 'a) t -> ('type_expr, 'l * allowed, 'a) t option -end + val has_with_bounds : ('type_expr, 'l * 'r) t -> bool -module Bounds : sig - include module type of Jkind_axis.Axis_collection (Bound) + val types_on_axis : + axis:'a Jkind_axis.Axis.t -> ('type_expr, 'l * 'r) t -> 'type_expr list - include Allowance.Allow_disallow with type ('a, _, 'd) sided = ('a, 'd) t + val compose_modality : + then_:Mode.Modality.t -> ('type_expr, 'l * 'r) t -> ('type_expr, 'l * 'r) t val debug_print : print_type_expr:(Format.formatter -> 'type_expr -> unit) -> Format.formatter -> - ('type_expr, 'd) t -> + ('type_expr, 'l * 'r) t -> unit end +module Bounds : sig + include module type of + Jkind_axis.Axis_collection.Indexed (Misc.Stdlib.Monad.Identity) + + val debug_print : Format.formatter -> t -> unit +end + module Layout_and_axes : sig open Allowance type (+'type_expr, 'layout, 'd) t = { layout : 'layout; - upper_bounds : ('type_expr, 'd) Bounds.t + upper_bounds : Bounds.t; + with_bounds : ('type_expr, 'd) With_bounds.t } constraint 'd = 'l * 'r diff --git a/typing/mode.ml b/typing/mode.ml index 6f0658e5466..2c434b8d2e9 100644 --- a/typing/mode.ml +++ b/typing/mode.ml @@ -1755,6 +1755,13 @@ module Value_with (Areality : Areality) = struct | Comonadic ax -> Comonadic.Const.lattice_of_axis ax | Monadic ax -> Monadic.Const.lattice_of_axis ax + let all_axes = + [ P (Comonadic Areality); + P (Monadic Uniqueness); + P (Comonadic Linearity); + P (Monadic Contention); + P (Comonadic Portability) ] + 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 @@ -2634,6 +2641,10 @@ module Modality = struct match ax with | Monadic ax -> Monadic.proj ax monadic | Comonadic ax -> Comonadic.proj ax comonadic + + let print ppf { monadic; comonadic } = + Format.fprintf ppf "%a;%a" Monadic.print monadic Comonadic.print + comonadic end type t = (Monadic.t, Comonadic.t) monadic_comonadic diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli index 2bcb96a5909..8f4ddb03ae4 100644 --- a/typing/mode_intf.mli +++ b/typing/mode_intf.mli @@ -343,6 +343,8 @@ module type S = sig val lattice_of_axis : ('m, 'a, 'd) axis -> (module Lattice with type t = 'a) + val all_axes : ('l * 'r) axis_packed list + type ('a, 'b, 'c, 'd, 'e) modes = { areality : 'a; linearity : 'b; @@ -380,6 +382,10 @@ module type S = sig val print : Format.formatter -> t -> unit end + val is_max : ('m, 'a, 'd) axis -> 'a -> bool + + val is_min : ('m, 'a, 'd) axis -> 'a -> bool + val split : t -> (Monadic.Const.t, Comonadic.Const.t) monadic_comonadic val merge : (Monadic.Const.t, Comonadic.Const.t) monadic_comonadic -> t @@ -549,6 +555,9 @@ module type S = sig (** [equate t0 t1] checks that [t0 = t1]. Definition: [t0 = t1] iff [t0 <= t1] and [t1 <= t0]. *) val equate : t -> t -> (unit, equate_error) Result.t + + (** Printing for debugging. *) + val print : Format.formatter -> t -> unit end (** A modality that acts on [Value] modes. Conceptually it is a sequnce of diff --git a/typing/predef.ml b/typing/predef.ml index f0097139471..a3c76d78a31 100644 --- a/typing/predef.ml +++ b/typing/predef.ml @@ -220,12 +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 + Jkind.add_with_bounds ~modality:Mode.Modality.Value.Const.id - ~baggage:param - (Jkind.add_baggage + ~type_expr:param + (Jkind.add_with_bounds ~modality:Mode.Modality.Value.Const.id - ~baggage:(type_list param) + ~type_expr:(type_list param) (Jkind.Builtin.immutable_data ~why:Boxed_variant)) let list_sort = Jkind.Sort.Const.value @@ -366,9 +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 + Jkind.add_with_bounds ~modality:Mode.Modality.Value.Const.id - ~baggage:param + ~type_expr:param (Jkind.Builtin.mutable_data ~why:(Primitive ident_array))) |> add_type1 ident_iarray ~variance:Variance.covariant @@ -376,9 +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 + Jkind.add_with_bounds ~modality:Mode.Modality.Value.Const.id - ~baggage:param + ~type_expr:param (Jkind.Builtin.immutable_data ~why:(Primitive ident_iarray))) |> add_type ident_bool ~kind:(variant [ cstr ident_false []; cstr ident_true []]) @@ -413,9 +413,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 + Jkind.add_with_bounds ~modality:Mode.Modality.Value.Const.id - ~baggage:param + ~type_expr:param (Jkind.Builtin.immutable_data ~why:Boxed_variant)) |> add_type_with_jkind ident_lexing_position ~kind:( @@ -448,10 +448,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 ~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_with_bounds ~modality:Mode.Modality.Value.Const.id ~type_expr:type_int |> + add_with_bounds ~modality:Mode.Modality.Value.Const.id ~type_expr:type_int |> + add_with_bounds ~modality:Mode.Modality.Value.Const.id ~type_expr:type_int |> + add_with_bounds ~modality:Mode.Modality.Value.Const.id ~type_expr: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/subst.ml b/typing/subst.ml index 9b779222398..5c848a8f97b 100644 --- a/typing/subst.ml +++ b/typing/subst.ml @@ -111,7 +111,7 @@ let with_additional_action = | Some const -> let builtin = List.find_opt (fun (builtin, _) -> - Jkind.Const.no_baggage_and_equal const builtin) + Jkind.Const.no_with_bounds_and_equal const builtin) builtins in begin match builtin with diff --git a/typing/typedecl.ml b/typing/typedecl.ml index fb8198c97d1..6c6bf5a707d 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -1829,13 +1829,11 @@ let update_decl_jkind env dpath decl = assert false in - let type_equal = Ctype.type_equal env in let jkind_of_type ty = Some (Ctype.type_jkind_purely env ty) in let add_crossings jkind = match !Clflags.allow_illegal_crossing with - | true -> Jkind.add_portability_and_contention_crossing - ~type_equal ~jkind_of_type ~from:decl.type_jkind jkind + | true -> Jkind.add_portability_and_contention_crossing ~from:decl.type_jkind jkind | false -> jkind, false in diff --git a/typing/typemode.ml b/typing/typemode.ml index fed816b76fc..a41817bd2ce 100644 --- a/typing/typemode.ml +++ b/typing/typemode.ml @@ -81,12 +81,13 @@ let transl_annot (type m) ~(annot_type : m annot_type) ~required_mode_maturity let unpack_mode_annot { txt = Parsetree.Mode s; loc } = { txt = s; loc } module Transled_modifier = struct - type (_, 'd, 'a) t = 'a Location.loc option constraint 'd = 'l * 'r + type 'a t = 'a Location.loc option let drop_loc modifier = Option.map Location.get_txt modifier end -module Transled_modifiers = Jkind_axis.Axis_collection (Transled_modifier) +module Transled_modifiers = + Jkind_axis.Axis_collection.Indexed (Transled_modifier) let transl_modifier_annots annots = let step modifiers_so_far annot = diff --git a/typing/typemode.mli b/typing/typemode.mli index 1d74dfbf496..eb8b3cc8cac 100644 --- a/typing/typemode.mli +++ b/typing/typemode.mli @@ -31,12 +31,12 @@ val untransl_modalities : Parsetree.modalities module Transled_modifier : sig - type (_, 'd, 'a) t = 'a Location.loc option constraint 'd = 'l * 'r + type 'a t = 'a Location.loc option end module Transled_modifiers : - module type of Jkind_axis.Axis_collection (Transled_modifier) + module type of Jkind_axis.Axis_collection.Indexed (Transled_modifier) (** Interpret a list of modifiers. A "modifier" is any keyword coming after a `mod` in a jkind *) -val transl_modifier_annots : Parsetree.modes -> _ Transled_modifiers.t +val transl_modifier_annots : Parsetree.modes -> Transled_modifiers.t