Merge PR #12955: Reroot primitive arrays on access

Reviewed-by: maximedenes

12 files changed, 47 insertions, 86 deletions

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 314cb54d1d..5cd91b4e74 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -58,7 +58,6 @@ type t =
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength
 
 let parse = function
@@ -110,7 +109,6 @@ let parse = function
   | "array_set" -> Arrayset
   | "array_length" -> Arraylength
   | "array_copy" -> Arraycopy
-  | "array_reroot" -> Arrayreroot
   | _ -> raise Not_found
 
 let equal (p1 : t) (p2 : t) =
@@ -164,8 +162,7 @@ let hash = function
   | Arraydefault -> 45
   | Arrayset -> 46
   | Arraycopy -> 47
-  | Arrayreroot -> 48
-  | Arraylength -> 49
+  | Arraylength -> 48
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -216,7 +213,6 @@ let to_string = function
   | Arraydefault -> "arraydefault"
   | Arrayset -> "arrayset"
   | Arraycopy -> "arraycopy"
-  | Arrayreroot -> "arrayreroot"
   | Arraylength -> "arraylength"
 
 type const =
@@ -302,7 +298,6 @@ let types =
   | Arraydefault -> [array_ty; PITT_param 1]
   | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty]
   | Arraycopy -> [array_ty; array_ty]
-  | Arrayreroot -> [array_ty; array_ty]
   | Arraylength -> [array_ty; int_ty]
 
 let one_param =
@@ -360,7 +355,6 @@ let params = function
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength -> one_param
 
 let nparams x = List.length (params x)
@@ -414,7 +408,6 @@ let univs = function
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength -> one_univ
 
 type arg_kind =
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 41b3bff465..0db643faf4 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -56,7 +56,6 @@ type t =
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength
 
 (** Can raise [Not_found].
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 9e17f97a56..05c98e4b87 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -739,15 +739,6 @@ let arraycopy accu vA t =
     no_check_arraycopy t
   else accu vA t
 
-let no_check_arrayreroot t =
-  of_parray (Parray.reroot (to_parray t))
-[@@ocaml.inline always]
-
-let arrayreroot accu vA t =
-  if is_parray t then
-    no_check_arrayreroot t
-  else accu vA t
-
 let no_check_arraylength t =
   mk_uint (Parray.length (to_parray t))
 [@@ocaml.inline always]
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 08c5bd7126..b9b75a9d7c 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -344,7 +344,6 @@ val arrayget : t -> t -> t -> t -> t (* accu A t n *)
 val arraydefault : t -> t -> t (* accu A t *)
 val arrayset : t -> t -> t -> t -> t -> t (* accu A t n v *)
 val arraycopy : t -> t -> t -> t (* accu A t *)
-val arrayreroot : t -> t -> t -> t (* accu A t *)
 val arraylength : t -> t -> t -> t (* accu A t *)
 val arrayinit : t -> t -> t -> t (* accu A n f def *)
 val arraymap : t -> t -> t (* accu A B f t *)
@@ -364,8 +363,5 @@ val no_check_arrayset : t -> t -> t -> t
 val no_check_arraycopy : t -> t
 [@@ocaml.inline always]
 
-val no_check_arrayreroot : t -> t
-[@@ocaml.inline always]
-
 val no_check_arraylength : t -> t
 [@@ocaml.inline always]
diff --git a/kernel/parray.ml b/kernel/parray.ml
index ea314c1883..0953f4b33f 100644
--- a/kernel/parray.ml
+++ b/kernel/parray.ml
@@ -27,45 +27,52 @@ and 'a kind =
 let unsafe_of_array t def = ref (Array (t,def))
 let of_array t def = unsafe_of_array (Array.copy t) def
 
-let rec length_int p =
-  match !p with
-  | Array (t,_) -> Array.length t
-  | Updated (_, _, p) -> length_int p
+let rec rerootk t k =
+  match !t with
+  | Array (a, _) -> k a
+  | Updated (i, v, p) ->
+      let k' a =
+        let v' = Array.unsafe_get a i in
+        Array.unsafe_set a i v;
+        t := !p; (* i.e., Array (a, def) *)
+        p := Updated (i, v', t);
+        k a in
+      rerootk p k'
+
+let reroot t = rerootk t (fun a -> a)
+
+let length_int p =
+  Array.length (reroot p)
 
 let length p = Uint63.of_int @@ length_int p
 
-let rec get p n =
-  match !p with
-  | Array (t,def) ->
-      let l = Array.length t in
-      if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then
-        Array.unsafe_get t (length_to_int n)
-      else def
-  | Updated (k,e,p) ->
-     if Uint63.equal n (Uint63.of_int k) then e
-     else get p n
+let get p n =
+  let t = reroot p in
+  let l = Array.length t in
+  if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then
+    Array.unsafe_get t (length_to_int n)
+  else
+    match !p with
+    | Array (_, def) -> def
+    | Updated _ -> assert false
 
 let set p n e =
-  let kind = !p in
-  match kind with
-  | Array (t,_) ->
-      let l = Uint63.of_int @@ Array.length t in
-      if Uint63.le Uint63.zero n && Uint63.lt n l then
-        let res = ref kind in
-        let n = length_to_int n in
-        p := Updated (n, Array.unsafe_get t n, res);
-        Array.unsafe_set t n e;
-        res
-      else p
-  | Updated _ ->
-      if Uint63.le Uint63.zero n && Uint63.lt n (length p) then
-        ref (Updated((length_to_int n), e, p))
-      else p
-
-let rec default p =
+  let a = reroot p in
+  let l = Uint63.of_int (Array.length a) in
+  if Uint63.le Uint63.zero n && Uint63.lt n l then
+    let i = length_to_int n in
+    let v' = Array.unsafe_get a i in
+    Array.unsafe_set a i e;
+    let t = ref !p in (* i.e., Array (a, def) *)
+    p := Updated (i, v', t);
+    t
+  else p
+
+let default p =
+  let _ = reroot p in
   match !p with
   | Array (_,def) -> def
-  | Updated (_,_,p) -> default p
+  | Updated _ -> assert false
 
 let make n def =
   ref (Array (Array.make (trunc_size n) def, def))
@@ -75,33 +82,19 @@ let init n f def =
   let t = Array.init n f in
   ref (Array (t, def))
 
-let rec to_array p =
+let to_array p =
+  let _ = reroot p in
   match !p with
   | Array (t,def) -> Array.copy t, def
-  | Updated (n,e,p) ->
-      let (t,_) as r = to_array p in
-      Array.unsafe_set t n e; r
+  | Updated _ -> assert false
 
 let copy p =
   let (t,def) = to_array p in
   ref (Array (t,def))
 
-let rec rerootk t k =
-  match !t with
-  | Array _ -> k ()
-  | Updated (i, v, t') ->
-      let k' () =
-        begin match !t' with
-        | Array (a,_def) as n ->
-            let v' = a.(i) in
-            Array.unsafe_set a i v;
-            t := n;
-            t' := Updated (i, v', t)
-        | Updated _ -> assert false
-        end; k() in
-      rerootk t' k'
-
-let reroot t = rerootk t (fun () -> t)
+let reroot t =
+  let _ = reroot t in
+  t
 
 let map f p =
   let p = reroot p in
diff --git a/kernel/parray.mli b/kernel/parray.mli
index 0276278bd0..8b6565c159 100644
--- a/kernel/parray.mli
+++ b/kernel/parray.mli
@@ -19,7 +19,6 @@ val default : 'a t -> 'a
 val make    : Uint63.t -> 'a -> 'a t
 val init    : Uint63.t -> (int -> 'a) -> 'a -> 'a t
 val copy    : 'a t -> 'a t
-val reroot  : 'a t -> 'a t
 
 val map : ('a -> 'b) -> 'a t -> 'b t
 
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 90eeeb9be7..f158cfacea 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -365,11 +365,6 @@ struct
       let t = get_parray evd args 1 in
       let t' = Parray.copy t in
       E.mkArray env u t' ty
-    | Arrayreroot ->
-      let ar = E.get args 1 in
-      let t = E.get_parray evd ar in
-      let _ = Parray.reroot t in
-      ar
     | Arraylength ->
       let t = get_parray evd args 1 in
       E.mkInt env (Parray.length t)
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 375b1aface..16a0f42664 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -508,7 +508,6 @@ let is_caml_prim = let open CPrimitives in function
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength -> true
   | _ -> false
 
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index f913cb906c..ec8601edc9 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -262,7 +262,7 @@ let check_prim_op = function
   | Arraymake -> opISINT_CAML_CALL2
   | Arrayget -> opISARRAY_INT_CAML_CALL2
   | Arrayset -> opISARRAY_INT_CAML_CALL3
-  | Arraydefault | Arraycopy | Arrayreroot | Arraylength ->
+  | Arraydefault | Arraycopy | Arraylength ->
       opISARRAY_CAML_CALL1
 
 let emit_instr env = function
diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
index 4ad830a298..9d80dc578b 100644
--- a/kernel/vmsymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -69,7 +69,6 @@ let parray_get = set_global Vmvalues.parray_get
 let parray_get_default = set_global Vmvalues.parray_get_default
 let parray_set = set_global Vmvalues.parray_set
 let parray_copy = set_global Vmvalues.parray_copy
-let parray_reroot = set_global Vmvalues.parray_reroot
 let parray_length = set_global Vmvalues.parray_length
 
 (* table pour les structured_constant et les annotations des switchs *)
@@ -135,7 +134,6 @@ let slot_for_caml_prim =
   | Arraydefault -> parray_get_default
   | Arrayset -> parray_set
   | Arraycopy -> parray_copy
-  | Arrayreroot -> parray_reroot
   | Arraylength -> parray_length
   | _ -> assert false
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 0678f37a0b..2068133b10 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -700,5 +700,4 @@ let parray_get = Obj.magic Parray.get
 let parray_get_default = Obj.magic Parray.default
 let parray_set = Obj.magic Parray.set
 let parray_copy = Obj.magic Parray.copy
-let parray_reroot = Obj.magic Parray.reroot
 let parray_length = Obj.magic Parray.length
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 6632dc46b2..d15595766a 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -204,5 +204,4 @@ val parray_get : values
 val parray_get_default : values
 val parray_set : values
 val parray_copy : values
-val parray_reroot : values
 val parray_length : values