diff --git a/src/util/Vec.ml b/src/util/Vec.ml index 277ec362..28036828 100644 --- a/src/util/Vec.ml +++ b/src/util/Vec.ml @@ -96,6 +96,16 @@ let[@inline] fast_remove t i = Array.unsafe_set t.data i @@ Array.unsafe_get t.data (t.sz - 1); t.sz <- t.sz - 1 +let append ~into v : unit = + if v.sz = 0 then () + else ( + if v.sz + into.sz > Array.length into.data then ( + resize_ into v.data.(0) (v.sz + into.sz); + ); + Array.blit v.data 0 into.data into.sz v.sz; + into.sz <- into.sz + v.sz; + ) + let prepend v ~into : unit = if v.sz = 0 then () else ( @@ -104,6 +114,7 @@ let prepend v ~into : unit = ); Array.blit into.data 0 into.data v.sz into.sz; (* shift elements *) Array.blit v.data 0 into.data 0 v.sz; + into.sz <- into.sz + v.sz; ) let filter_in_place f vec = diff --git a/src/util/Vec.mli b/src/util/Vec.mli index feae52b7..b9a1733e 100644 --- a/src/util/Vec.mli +++ b/src/util/Vec.mli @@ -70,6 +70,9 @@ val fast_remove : 'a t -> int -> unit (** Remove element at index [i] without preserving order (swap with last element) *) +val append : into:'a t -> 'a t -> unit +(** [append ~into v] pushes elements of [v] in the vector [into] *) + val prepend : 'a t -> into:'a t -> unit (** [prepend v ~into] pushes all elements of [v] into [into], at the beginning. consumes [v]. *)