From 858616606b46419d808fbc42961292faa738230b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 19 Nov 2019 14:46:33 -0600 Subject: [PATCH] add `CCVector.shrink_to_fit` to limit memory usage --- src/core/CCVector.ml | 15 +++++++++++++++ src/core/CCVector.mli | 5 ++++- 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/src/core/CCVector.ml b/src/core/CCVector.ml index 454bc104..4bff2543 100644 --- a/src/core/CCVector.ml +++ b/src/core/CCVector.ml @@ -453,6 +453,21 @@ let shrink v n = ) *) +let shrink_to_fit v : unit = + if v.size = 0 then ( + v.vec <- [| |] + ) else if v.size < Array.length v.vec then ( + v.vec <- Array.sub v.vec 0 v.size + ) + +(*$QR + (gen Q.small_int) (fun v -> + let v' = copy v in + shrink_to_fit v; + to_list v = to_list v' + ) +*) + let sort' cmp v = (* possibly copy array (to avoid junk at its end), then sort the array *) let a = diff --git a/src/core/CCVector.mli b/src/core/CCVector.mli index c2da68e9..7271e2f9 100644 --- a/src/core/CCVector.mli +++ b/src/core/CCVector.mli @@ -1,4 +1,3 @@ - (* This file is free software, part of containers. See file "license" for more details. *) (** {1 Growable, mutable vector} *) @@ -124,6 +123,10 @@ val shrink : ('a, rw) t -> int -> unit (** Shrink to the given size (remove elements above this size). Does nothing if the parameter is bigger than the current size. *) +val shrink_to_fit : ('a, _) t -> unit +(** Shrink internal array to fit the size of the vector + @since NEXT_RELEASE *) + val member : eq:('a -> 'a -> bool) -> 'a -> ('a, _) t -> bool (** Is the element a member of the vector? *)