From d08d5fe9c423115d4e265267874e5c2ff5ae7211 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 20 Jul 2021 10:07:29 -0400
Subject: [PATCH] feat(util): add VecI32 based on bigarray

---
 src/util/Sidekick_util.ml |  2 +-
 src/util/VecI32.ml        | 86 +++++++++++++++++++++++++++++++++++++++
 src/util/VecI32.mli       | 39 ++++++++++++++++++
 src/util/dune             |  2 +-
 4 files changed, 127 insertions(+), 2 deletions(-)
 create mode 100644 src/util/VecI32.ml
 create mode 100644 src/util/VecI32.mli

diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml
index e1de8bfd..31bce34f 100644
--- a/src/util/Sidekick_util.ml
+++ b/src/util/Sidekick_util.ml
@@ -1,9 +1,9 @@
 (* re-exports *)
 module Fmt = CCFormat
 
-
 module Util = Util
 module Vec = Vec
+module VecI32 = VecI32
 module Bitvec = Bitvec
 module Log = Log
 module Backtrack_stack = Backtrack_stack
diff --git a/src/util/VecI32.ml b/src/util/VecI32.ml
new file mode 100644
index 00000000..d5fa32a6
--- /dev/null
+++ b/src/util/VecI32.ml
@@ -0,0 +1,86 @@
+
+module A = Bigarray.Array1
+
+type int32arr = (int32, Bigarray.int32_elt, Bigarray.c_layout) A.t
+
+type t = {
+  mutable data: int32arr;
+  mutable sz: int;
+}
+
+let mk_arr_ sz : int32arr = A.create Bigarray.int32 Bigarray.c_layout sz
+
+let create () : t =
+  { sz=0; data=mk_arr_ 16 }
+
+let[@inline] clear self = self.sz <- 0
+let[@inline] shrink self n = if n < self.sz then self.sz <- n
+let[@inline] size self = self.sz
+let[@inline] is_empty self = self.sz = 0
+
+(* ensure capacity is [new_cap] *)
+let resize_cap_ self new_cap =
+  assert (A.dim self.data < new_cap);
+  let new_data = mk_arr_ new_cap in
+  A.blit self.data (A.sub new_data 0 (A.dim self.data));
+  self.data <- new_data
+
+let ensure_size self (n:int) =
+  if n > A.dim self.data then (
+    let new_cap = max n (A.dim self.data * 2 + 10) in
+    resize_cap_ self new_cap;
+  );
+  if n > self.sz then (
+    self.sz <- n
+  )
+
+let[@inline] push (self:t) i : unit =
+  ensure_size self (self.sz+1);
+  self.data.{self.sz} <- Int32.of_int i;
+  self.sz <- 1 + self.sz
+
+let[@inline] push_i32 self i =
+  ensure_size self (self.sz+1);
+  self.data.{self.sz} <- i;
+  self.sz <- 1 + self.sz
+
+let[@inline] pop self =
+  if self.sz > 0 then (
+    let x = Int32.to_int self.data.{self.sz-1} in
+    self.sz <- self.sz - 1;
+    x
+  ) else failwith "vecI32.pop: empty"
+
+let[@inline] get self i : int =
+  assert (i >= 0 && i < self.sz);
+  Int32.to_int (A.unsafe_get self.data i)
+
+let[@inline] get_i32 self i : int32 =
+  assert (i >= 0 && i < self.sz);
+  A.unsafe_get self.data i
+
+let[@inline] set self i x : unit =
+  assert (i >= 0 && i < self.sz);
+  A.unsafe_set self.data i (Int32.of_int x)
+
+let[@inline] set_i32 self i x : unit =
+  assert (i >= 0 && i < self.sz);
+  A.unsafe_set self.data i x
+
+let[@inline] iter ~f self =
+  for i=0 to self.sz - 1 do
+    f (Int32.to_int self.data.{i})
+  done
+
+let[@inline] iteri ~f self =
+  for i=0 to self.sz - 1 do
+    f i (Int32.to_int self.data.{i})
+  done
+
+let[@inline] to_iter self k = iter ~f:k self
+
+let pp out self =
+  Format.fprintf out "[@[";
+  iteri self ~f:(fun i x -> if i>0 then Format.fprintf out ",@ "; Format.pp_print_int out x);
+  Format.fprintf out "@]]"
+
diff --git a/src/util/VecI32.mli b/src/util/VecI32.mli
new file mode 100644
index 00000000..4fada4dc
--- /dev/null
+++ b/src/util/VecI32.mli
@@ -0,0 +1,39 @@
+
+(** Vectors of int32 integers
+
+    These vectors are more optimized than {!Vec}. *)
+
+type t
+
+val create : unit -> t
+
+val ensure_size : t -> int -> unit
+
+val size : t -> int
+
+val clear : t -> unit
+
+val is_empty : t -> bool
+
+val push : t -> int -> unit
+
+val pop : t -> int
+
+val push_i32 : t -> int32 -> unit
+
+val get : t -> int -> int
+
+val get_i32 : t -> int -> int32
+
+val set : t -> int -> int -> unit
+
+val set_i32 : t -> int -> int32 -> unit
+
+val shrink : t -> int -> unit
+
+val iter : f:(int -> unit) -> t -> unit
+val iteri : f:(int -> int -> unit) -> t -> unit
+
+val to_iter : t -> int Iter.t
+
+val pp : t CCFormat.printer
diff --git a/src/util/dune b/src/util/dune
index 800a53c7..5ed24b17 100644
--- a/src/util/dune
+++ b/src/util/dune
@@ -2,4 +2,4 @@
   (name sidekick_util)
   (public_name sidekick.util)
   (flags :standard -warn-error -a+8)
-  (libraries containers iter sidekick.sigs))
+  (libraries containers iter sidekick.sigs bigarray))