non_float arrays are addrarrays

parsing/language_extension.ml

@@ -73,6 +73,7 @@ let get_level_ops : type a. a t -> (module Extension_level with type t = a) =
   | Labeled_tuples -> (module Unit)
   | Small_numbers -> (module Maturity)
   | Instances -> (module Unit)
+  | Separability -> (module Unit)
 
 (* We'll do this in a more principled way later. *)
 (* CR layouts: Note that layouts is only "mostly" erasable, because of annoying
@@ -85,7 +86,8 @@ let get_level_ops : type a. a t -> (module Extension_level with type t = a) =
 let is_erasable : type a. a t -> bool = function
   | Mode | Unique | Overwriting | Layouts -> true
   | Comprehensions | Include_functor | Polymorphic_parameters | Immutable_arrays
-  | Module_strengthening | SIMD | Labeled_tuples | Small_numbers | Instances ->
+  | Module_strengthening | SIMD | Labeled_tuples | Small_numbers | Instances
+  | Separability ->
     false
 
 let maturity_of_unique_for_drf = Stable
@@ -109,6 +111,7 @@ module Exist_pair = struct
     | Pair (Labeled_tuples, ()) -> Stable
     | Pair (Small_numbers, m) -> m
     | Pair (Instances, ()) -> Stable
+    | Pair (Separability, ()) -> Stable
 
   let is_erasable : t -> bool = function Pair (ext, _) -> is_erasable ext
 
@@ -122,7 +125,7 @@ module Exist_pair = struct
     | Pair
         ( (( Comprehensions | Include_functor | Polymorphic_parameters
            | Immutable_arrays | Module_strengthening | Labeled_tuples
-           | Instances | Overwriting ) as ext),
+           | Instances | Overwriting | Separability ) as ext),
           _ ) ->
       to_string ext
 
@@ -153,6 +156,7 @@ module Exist_pair = struct
     | "small_numbers" -> Some (Pair (Small_numbers, Stable))
     | "small_numbers_beta" -> Some (Pair (Small_numbers, Beta))
     | "instances" -> Some (Pair (Instances, ()))
+    | "separability" -> Some (Pair (Separability, ()))
     | _ -> None
 end
 
@@ -173,7 +177,8 @@ let all_extensions =
     Pack SIMD;
     Pack Labeled_tuples;
     Pack Small_numbers;
-    Pack Instances ]
+    Pack Instances;
+    Pack Separability ]
 
 (**********************************)
 (* string conversions *)
@@ -212,9 +217,11 @@ let equal_t (type a b) (a : a t) (b : b t) : (a, b) Misc.eq option =
   | Labeled_tuples, Labeled_tuples -> Some Refl
   | Small_numbers, Small_numbers -> Some Refl
   | Instances, Instances -> Some Refl
+  | Separability, Separability -> Some Refl
   | ( ( Comprehensions | Mode | Unique | Overwriting | Include_functor
       | Polymorphic_parameters | Immutable_arrays | Module_strengthening
-      | Layouts | SIMD | Labeled_tuples | Small_numbers | Instances ),
+      | Layouts | SIMD | Labeled_tuples | Small_numbers | Instances
+      | Separability ),
       _ ) ->
     None
 

parsing/language_extension.mli

@@ -31,6 +31,7 @@ type 'a t = 'a Language_extension_kernel.t =
   | Labeled_tuples : unit t
   | Small_numbers : maturity t
   | Instances : unit t
+  | Separability : unit t
 
 (** Require that an extension is enabled for at least the provided level, or
     else throw an exception at the provided location saying otherwise. *)

testsuite/tests/typing-layouts-or-null/non_float_array.ml

@@ -0,0 +1,127 @@
+(* TEST
+ flags = "-dlambda -dno-unique-ids";
+ expect;
+*)
+
+(* Normal arrays are [genarray]s. Due to the float array optimization,
+   they must check whether their elements are float or non-float on
+   creation, [get] and [set].
+
+   We can see what kind of array we are getting by looking at Lambda. *)
+
+let mk_gen (x : 'a) = [| x |]
+[%%expect{|
+(let (mk_gen = (function {nlocal = 0} x : genarray (makearray[gen] x)))
+  (apply (field_imm 1 (global Toploop!)) "mk_gen" mk_gen))
+val mk_gen : 'a -> 'a array = <fun>
+|}]
+
+let get_gen (xs : 'a array) i = xs.(i)
+[%%expect{|
+(let
+  (get_gen =
+     (function {nlocal = 0} xs[genarray] i[int]
+       (array.get[gen indexed by int] xs i)))
+  (apply (field_imm 1 (global Toploop!)) "get_gen" get_gen))
+val get_gen : 'a array -> int -> 'a = <fun>
+|}]
+
+let set_gen (xs : 'a array) x i = xs.(i) <- x
+[%%expect{|
+(let
+  (set_gen =
+     (function {nlocal = 0} xs[genarray] x i[int] : int
+       (array.set[gen indexed by int] xs i x)))
+  (apply (field_imm 1 (global Toploop!)) "set_gen" set_gen))
+val set_gen : 'a array -> 'a -> int -> unit = <fun>
+|}]
+
+(* [non_float] arrays are [addrarray]s. Operations on [addrarray]s
+   skip checks related to floats.
+
+   Here we can see that our operations are postfixed with [addr]. *)
+
+let mk (type t : value mod non_float) (x : t) = [| x |]
+[%%expect{|
+(let (mk = (function {nlocal = 0} x : addrarray (makearray[addr] x)))
+  (apply (field_imm 1 (global Toploop!)) "mk" mk))
+val mk : ('t : value mod non_float). 't -> 't array = <fun>
+|}]
+
+let get (type t : value mod non_float) (xs : t array) i = xs.(i)
+[%%expect{|
+(let
+  (get =
+     (function {nlocal = 0} xs[addrarray] i[int]
+       (array.get[addr indexed by int] xs i)))
+  (apply (field_imm 1 (global Toploop!)) "get" get))
+val get : ('t : value mod non_float). 't array -> int -> 't = <fun>
+|}]
+
+let set (type t : value mod non_float) (xs : t array) x i = xs.(i) <- x
+
+[%%expect{|
+(let
+  (set =
+     (function {nlocal = 0} xs[addrarray] x i[int] : int
+       (array.set[addr indexed by int] xs i x)))
+  (apply (field_imm 1 (global Toploop!)) "set" set))
+val set : ('t : value mod non_float). 't array -> 't -> int -> unit = <fun>
+|}]
+
+(* A concrete example. *)
+
+module X : sig
+  type t : immutable_data
+
+  val x1 : t
+  val x2 : t
+end = struct
+  type t = { a: string; b: int }
+
+  let x1 = { a = "first"; b = 1 }
+  let x2 = { a = "second"; b = 2 }
+end
+
+[%%expect{|
+(apply (field_imm 1 (global Toploop!)) "X/370"
+  (let
+    (x1 =[(consts ()) (non_consts ([0: *, [int]]))] [0: "first" 1]
+     x2 =[(consts ()) (non_consts ([0: *, [int]]))] [0: "second" 2])
+    (makeblock 0 x1 x2)))
+module X : sig type t : immutable_data val x1 : t val x2 : t end
+|}]
+
+(* Create an [addrarray] and perform [addr] operations on it. *)
+
+let () =
+  let xs = Array.make 4 X.x1 in
+  xs.(1) <- X.x2;
+  xs.(2) <- X.x2;
+  assert (xs.(0) = xs.(3));
+  assert (xs.(1) = xs.(2));
+  assert (not (xs.(0) = xs.(1)))
+;;
+
+[%%expect{|
+(let
+  (X = (apply (field_imm 0 (global Toploop!)) "X/370")
+   *match* =[int]
+     (let (xs =[addrarray] (caml_make_vect 4 (field_imm 0 X)))
+       (seq (array.set[addr indexed by int] xs 1 (field_imm 1 X))
+         (array.set[addr indexed by int] xs 2 (field_imm 1 X))
+         (if
+           (caml_equal (array.get[addr indexed by int] xs 0)
+             (array.get[addr indexed by int] xs 3))
+           0 (raise (makeblock 0 (getpredef Assert_failure!!) [0: "" 5 2])))
+         (if
+           (caml_equal (array.get[addr indexed by int] xs 1)
+             (array.get[addr indexed by int] xs 2))
+           0 (raise (makeblock 0 (getpredef Assert_failure!!) [0: "" 6 2])))
+         (if
+           (not
+             (caml_equal (array.get[addr indexed by int] xs 0)
+               (array.get[addr indexed by int] xs 1)))
+           0 (raise (makeblock 0 (getpredef Assert_failure!!) [0: "" 7 2]))))))
+  0)
+|}]

testsuite/tests/typing-layouts-or-null/non_float_array_no_separability.ml

@@ -0,0 +1,123 @@
+(* TEST
+ flags = "-dlambda -dno-unique-ids -no-extension separability";
+ expect;
+*)
+
+(* Copy of [non_float_array.ml] with [-no-extension separability] for comparison. *)
+
+let mk_gen (x : 'a) = [| x |]
+[%%expect{|
+(let (mk_gen = (function {nlocal = 0} x : genarray (makearray[gen] x)))
+  (apply (field_imm 1 (global Toploop!)) "mk_gen" mk_gen))
+val mk_gen : 'a -> 'a array = <fun>
+|}]
+
+let get_gen (xs : 'a array) i = xs.(i)
+[%%expect{|
+(let
+  (get_gen =
+     (function {nlocal = 0} xs[genarray] i[int]
+       (array.get[gen indexed by int] xs i)))
+  (apply (field_imm 1 (global Toploop!)) "get_gen" get_gen))
+val get_gen : 'a array -> int -> 'a = <fun>
+|}]
+
+let set_gen (xs : 'a array) x i = xs.(i) <- x
+[%%expect{|
+(let
+  (set_gen =
+     (function {nlocal = 0} xs[genarray] x i[int] : int
+       (array.set[gen indexed by int] xs i x)))
+  (apply (field_imm 1 (global Toploop!)) "set_gen" set_gen))
+val set_gen : 'a array -> 'a -> int -> unit = <fun>
+|}]
+
+(* [non_float] arrays are [addrarray]s. Operations on [addrarray]s
+   skip checks related to floats.
+
+   Here we can see that our operations are postfixed with [addr]. *)
+
+let mk (type t : value mod non_float) (x : t) = [| x |]
+[%%expect{|
+(let (mk = (function {nlocal = 0} x : genarray (makearray[gen] x)))
+  (apply (field_imm 1 (global Toploop!)) "mk" mk))
+val mk : ('t : value mod non_float). 't -> 't array = <fun>
+|}]
+
+let get (type t : value mod non_float) (xs : t array) i = xs.(i)
+[%%expect{|
+(let
+  (get =
+     (function {nlocal = 0} xs[genarray] i[int]
+       (array.get[gen indexed by int] xs i)))
+  (apply (field_imm 1 (global Toploop!)) "get" get))
+val get : ('t : value mod non_float). 't array -> int -> 't = <fun>
+|}]
+
+let set (type t : value mod non_float) (xs : t array) x i = xs.(i) <- x
+
+[%%expect{|
+(let
+  (set =
+     (function {nlocal = 0} xs[genarray] x i[int] : int
+       (array.set[gen indexed by int] xs i x)))
+  (apply (field_imm 1 (global Toploop!)) "set" set))
+val set : ('t : value mod non_float). 't array -> 't -> int -> unit = <fun>
+|}]
+
+(* A concrete example. *)
+
+module X : sig
+  type t : immutable_data
+
+  val x1 : t
+  val x2 : t
+end = struct
+  type t = { a: string; b: int }
+
+  let x1 = { a = "first"; b = 1 }
+  let x2 = { a = "second"; b = 2 }
+end
+
+[%%expect{|
+(apply (field_imm 1 (global Toploop!)) "X/370"
+  (let
+    (x1 =[(consts ()) (non_consts ([0: *, [int]]))] [0: "first" 1]
+     x2 =[(consts ()) (non_consts ([0: *, [int]]))] [0: "second" 2])
+    (makeblock 0 x1 x2)))
+module X : sig type t : immutable_data val x1 : t val x2 : t end
+|}]
+
+(* Create an [addrarray] and perform [addr] operations on it. *)
+
+let () =
+  let xs = Array.make 4 X.x1 in
+  xs.(1) <- X.x2;
+  xs.(2) <- X.x2;
+  assert (xs.(0) = xs.(3));
+  assert (xs.(1) = xs.(2));
+  assert (not (xs.(0) = xs.(1)))
+;;
+
+[%%expect{|
+(let
+  (X = (apply (field_imm 0 (global Toploop!)) "X/370")
+   *match* =[int]
+     (let (xs =[genarray] (caml_make_vect 4 (field_imm 0 X)))
+       (seq (array.set[gen indexed by int] xs 1 (field_imm 1 X))
+         (array.set[gen indexed by int] xs 2 (field_imm 1 X))
+         (if
+           (caml_equal (array.get[gen indexed by int] xs 0)
+             (array.get[gen indexed by int] xs 3))
+           0 (raise (makeblock 0 (getpredef Assert_failure!!) [0: "" 5 2])))
+         (if
+           (caml_equal (array.get[gen indexed by int] xs 1)
+             (array.get[gen indexed by int] xs 2))
+           0 (raise (makeblock 0 (getpredef Assert_failure!!) [0: "" 6 2])))
+         (if
+           (not
+             (caml_equal (array.get[gen indexed by int] xs 0)
+               (array.get[gen indexed by int] xs 1)))
+           0 (raise (makeblock 0 (getpredef Assert_failure!!) [0: "" 7 2]))))))
+  0)
+|}]

typing/ctype.ml

@@ -2589,6 +2589,14 @@ let check_type_nullability env ty null =
   | Ok () -> true
   | Error _ -> false
 
+let check_type_separability env ty sep =
+  let upper_bound =
+    Jkind.set_separability_upper_bound (Jkind.Builtin.any ~why:Dummy_jkind) sep
+  in
+  match check_type_jkind env ty upper_bound with
+  | Ok () -> true
+  | Error _ -> false
+
 let check_type_jkind_exn env texn ty jkind =
   match check_type_jkind env ty jkind with
   | Ok _ -> ()

typing/ctype.mli

@@ -667,6 +667,12 @@ val check_type_externality :
 val check_type_nullability :
   Env.t -> type_expr -> Jkind_axis.Nullability.t -> bool
 
+(* Check whether a type's separability is less than some target.
+   Potentially cheaper than just calling [type_jkind], because this can stop
+   expansion once it succeeds. *)
+val check_type_separability :
+  Env.t -> type_expr -> Jkind_axis.Separability.t -> bool
+
 (* This function should get called after a type is generalized.
 
    It does two things:

typing/jkind.ml

@@ -2581,6 +2581,16 @@ let set_nullability_upper_bound jk nullability_upper_bound =
   in
   { jk with jkind = { jk.jkind with mod_bounds = new_bounds } }
 
+let set_separability_upper_bound jk separability_upper_bound =
+  { jk with
+    jkind =
+      { jk.jkind with
+        mod_bounds =
+          Mod_bounds.set_separability separability_upper_bound
+            jk.jkind.mod_bounds
+      }
+  }
+
 let set_layout jk layout = { jk with jkind = { jk.jkind with layout } }
 
 let apply_modality_l modality jk =

typing/jkind.mli

@@ -588,10 +588,15 @@ val get_nullability :
   Jkind_axis.Nullability.t
 
 (** Computes a jkind that is the same as the input but with an updated maximum
-    mode for the externality axis *)
+    mode for the nullability axis *)
 val set_nullability_upper_bound :
   Types.jkind_r -> Jkind_axis.Nullability.t -> Types.jkind_r
 
+(** Computes a jkind that is the same as the input but with an updated maximum
+    mode for the separability axis *)
+val set_separability_upper_bound :
+  Types.jkind_r -> Jkind_axis.Separability.t -> Types.jkind_r
+
 (** Sets the layout in a jkind. *)
 val set_layout : 'd Types.jkind -> Sort.t Layout.t -> 'd Types.jkind