mirror of
https://github.com/c-cube/linol.git
synced 2026-01-22 09:26:40 -05:00
102 lines
48 KiB
HTML
102 lines
48 KiB
HTML
<!DOCTYPE html>
|
||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Dynarray (ocaml.Stdlib.Dynarray)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../_odoc-theme/odoc.css"/><meta name="generator" content="odoc 2.4.4"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">ocaml</a> » <a href="../index.html">Stdlib</a> » Dynarray</nav><header class="odoc-preamble"><h1>Module <code><span>Stdlib.Dynarray</span></code></h1><p>Dynamic arrays.</p><p>The <a href="../Array/index.html"><code>Array</code></a> module provide arrays of fixed length. <a href="#"><code>Dynarray</code></a> provides arrays whose length can change over time, by adding or removing elements at the end of the array.</p><p>This is typically used to accumulate elements whose number is not known in advance or changes during computation, while also providing fast access to elements at arbitrary positions.</p><pre class="language-ocaml"><code>let dynarray_of_list li =
|
||
let arr = Dynarray.create () in
|
||
List.iter (fun v -> Dynarray.add_last arr v) li;
|
||
arr</code></pre><p>The <a href="../Buffer/index.html"><code>Buffer</code></a> module provides similar features, but it is specialized for accumulating characters into a dynamically-resized string.</p><p>The <a href="../Stack/index.html"><code>Stack</code></a> module provides a last-in first-out data structure that can be easily implemented on top of dynamic arrays.</p><p><b>Warning.</b> In their current implementation, the memory layout of dynamic arrays differs from the one of <a href="../Array/index.html"><code>Array</code></a>s. See the <a href="#memory_layout" title="memory_layout">Memory Layout</a> section for more information.</p><ul class="at-tags"><li class="since"><span class="at-tag">since</span> 5.2</li></ul></header><nav class="odoc-toc"><ul><li><a href="#dynarrays">Dynamic arrays</a></li><li><a href="#adding">Adding elements</a></li><li><a href="#removing">Removing elements</a></li><li><a href="#iteration">Iteration</a></li><li><a href="#conversions">Conversions to other data structures</a></li><li><a href="#advanced">Advanced topics for performance</a><ul><li><a href="#capacity">Backing array, capacity</a></li><li><a href="#noleaks">No leaks: preservation of memory liveness</a></li><li><a href="#memory_layout">Memory layout of dynarrays</a></li></ul></li><li><a href="#examples">Code examples</a><ul><li><a href="#example_min_heap">Min-heaps for mutable priority queues</a></li></ul></li></ul></nav><div class="odoc-content"><p><b>Unsynchronized accesses</b></p><p>Concurrent accesses to dynamic arrays must be synchronized (for instance with a <a href="../Mutex/index.html#type-t"><code>Mutex.t</code></a>). Unsynchronized accesses to a dynamic array are a programming error that may lead to an invalid dynamic array state, on which some operations would fail with an <code>Invalid_argument</code> exception.</p><h2 id="dynarrays"><a href="#dynarrays" class="anchor"></a>Dynamic arrays</h2><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> <span>!'a t</span></span></code></div><div class="spec-doc"><p>A dynamic array containing values of type <code>'a</code>.</p><p>A dynamic array <code>a</code> provides constant-time <code>get</code> and <code>set</code> operations on indices between <code>0</code> and <code>Dynarray.length a - 1</code> included. Its <a href="#val-length"><code>length</code></a> may change over time by adding or removing elements to the end of the array.</p><p>We say that an index into a dynarray <code>a</code> is valid if it is in <code>0 .. length a - 1</code> and invalid otherwise.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span>unit <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>create ()</code> is a new, empty array.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-make"><a href="#val-make" class="anchor"></a><code><span><span class="keyword">val</span> make : <span>int <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>make n x</code> is a new array of length <code>n</code>, filled with <code>x</code>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Invalid_argument"><code>Invalid_argument</code></a> <p>if <code>n < 0</code> or <code>n > Sys.max_array_length</code>.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-init"><a href="#val-init" class="anchor"></a><code><span><span class="keyword">val</span> init : <span>int <span class="arrow">-></span></span> <span><span>(<span>int <span class="arrow">-></span></span> <span class="type-var">'a</span>)</span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>init n f</code> is a new array <code>a</code> of length <code>n</code>, such that <code>get a i</code> is <code>f i</code>. In other words, the elements of <code>a</code> are <code>f 0</code>, then <code>f 1</code>, then <code>f 2</code>... and <code>f (n - 1)</code> last, evaluated in that order.</p><p>This is similar to <a href="../Array/index.html#val-init"><code>Array.init</code></a>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Invalid_argument"><code>Invalid_argument</code></a> <p>if <code>n < 0</code> or <code>n > Sys.max_array_length</code>.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get"><a href="#val-get" class="anchor"></a><code><span><span class="keyword">val</span> get : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p><code>get a i</code> is the <code>i</code>-th element of <code>a</code>, starting with index <code>0</code>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Invalid_argument"><code>Invalid_argument</code></a> <p>if the index is invalid</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-set"><a href="#val-set" class="anchor"></a><code><span><span class="keyword">val</span> set : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>set a i x</code> sets the <code>i</code>-th element of <code>a</code> to be <code>x</code>.</p><p><code>i</code> must be a valid index. <code>set</code> does not add new elements to the array -- see <a href="#val-add_last"><code>add_last</code></a> to add an element.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Invalid_argument"><code>Invalid_argument</code></a> <p>if the index is invalid.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-length"><a href="#val-length" class="anchor"></a><code><span><span class="keyword">val</span> length : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p><code>length a</code> is the number of elements in the array.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_empty"><a href="#val-is_empty" class="anchor"></a><code><span><span class="keyword">val</span> is_empty : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p><code>is_empty a</code> is <code>true</code> if <code>a</code> is empty, that is, if <code>length a = 0</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get_last"><a href="#val-get_last" class="anchor"></a><code><span><span class="keyword">val</span> get_last : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p><code>get_last a</code> is the element of <code>a</code> at index <code>length a - 1</code>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Invalid_argument"><code>Invalid_argument</code></a> <p>if <code>a</code> is empty.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-find_last"><a href="#val-find_last" class="anchor"></a><code><span><span class="keyword">val</span> find_last : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> option</span></span></code></div><div class="spec-doc"><p><code>find_last a</code> is <code>None</code> if <code>a</code> is empty and <code>Some (get_last a)</code> otherwise.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-copy"><a href="#val-copy" class="anchor"></a><code><span><span class="keyword">val</span> copy : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>copy a</code> is a shallow copy of <code>a</code>, a new array containing the same elements as <code>a</code>.</p></div></div><h2 id="adding"><a href="#adding" class="anchor"></a>Adding elements</h2><p>Note: all operations adding elements raise <code>Invalid_argument</code> if the length needs to grow beyond <a href="../Sys/index.html#val-max_array_length"><code>Sys.max_array_length</code></a>.</p><div class="odoc-spec"><div class="spec value anchored" id="val-add_last"><a href="#val-add_last" class="anchor"></a><code><span><span class="keyword">val</span> add_last : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>add_last a x</code> adds the element <code>x</code> at the end of the array <code>a</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-append_array"><a href="#val-append_array" class="anchor"></a><code><span><span class="keyword">val</span> append_array : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> array</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>append_array a b</code> adds all elements of <code>b</code> at the end of <code>a</code>, in the order they appear in <code>b</code>.</p><p>For example:</p><pre class="language-ocaml"><code>let a = Dynarray.of_list [1;2] in
|
||
Dynarray.append_array a [|3; 4|];
|
||
assert (Dynarray.to_list a = [1; 2; 3; 4])</code></pre></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-append_list"><a href="#val-append_list" class="anchor"></a><code><span><span class="keyword">val</span> append_list : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> list</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Like <a href="#val-append_array"><code>append_array</code></a> but with a list.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-append"><a href="#val-append" class="anchor"></a><code><span><span class="keyword">val</span> append : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>append a b</code> is like <code>append_array a b</code>, but <code>b</code> is itself a dynamic array instead of a fixed-size array.</p><p>Warning: <code>append a a</code> is a programming error because it iterates on <code>a</code> and adds elements to it at the same time -- see the <a href="#iteration" title="iteration">Iteration</a> section below. It fails with <code>Invalid_argument</code>. If you really want to append a copy of <code>a</code> to itself, you can use <code>Dynarray.append_array a (Dynarray.to_array a)</code> which copies <code>a</code> into a temporary array.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-append_seq"><a href="#val-append_seq" class="anchor"></a><code><span><span class="keyword">val</span> append_seq : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="../Seq/index.html#type-t">Seq.t</a></span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Like <a href="#val-append_array"><code>append_array</code></a> but with a sequence.</p><p>Warning: <code>append_seq a (to_seq_reentrant a)</code> simultaneously traverses <code>a</code> and adds element to it; the ordering of those operations is unspecified, and may result in an infinite loop -- the new elements may in turn be produced by <code>to_seq_reentrant a</code> and get added again and again.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-append_iter"><a href="#val-append_iter" class="anchor"></a><code><span><span class="keyword">val</span> append_iter : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span>(<span><span>(<span><span class="type-var">'a</span> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> <span><span class="type-var">'x</span> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> <span><span class="type-var">'x</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>append_iter a iter x</code> adds each element of <code>x</code> to the end of <code>a</code>. This is <code>iter (add_last a) x</code>.</p><p>For example, <code>append_iter a List.iter [1;2;3]</code> would add elements <code>1</code>, <code>2</code>, and then <code>3</code> at the end of <code>a</code>. <code>append_iter a Queue.iter q</code> adds elements from the queue <code>q</code>.</p></div></div><h2 id="removing"><a href="#removing" class="anchor"></a>Removing elements</h2><div class="odoc-spec"><div class="spec value anchored" id="val-pop_last_opt"><a href="#val-pop_last_opt" class="anchor"></a><code><span><span class="keyword">val</span> pop_last_opt : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> option</span></span></code></div><div class="spec-doc"><p><code>pop_last_opt a</code> removes and returns the last element of <code>a</code>, or <code>None</code> if the array is empty.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop_last"><a href="#val-pop_last" class="anchor"></a><code><span><span class="keyword">val</span> pop_last : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p><code>pop_last a</code> removes and returns the last element of <code>a</code>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Not_found"><code>Not_found</code></a> <p>on an empty array.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-remove_last"><a href="#val-remove_last" class="anchor"></a><code><span><span class="keyword">val</span> remove_last : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>remove_last a</code> removes the last element of <code>a</code>, if any. It does nothing if <code>a</code> is empty.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-truncate"><a href="#val-truncate" class="anchor"></a><code><span><span class="keyword">val</span> truncate : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>truncate a n</code> truncates <code>a</code> to have at most <code>n</code> elements.</p><p>It removes elements whose index is greater or equal to <code>n</code>. It does nothing if <code>n >= length a</code>.</p><p><code>truncate a n</code> is equivalent to:</p><pre class="language-ocaml"><code>if n < 0 then invalid_argument "...";
|
||
while length a > n do
|
||
remove_last a
|
||
done</code></pre><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Invalid_argument"><code>Invalid_argument</code></a> <p>if <code>n < 0</code>.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-clear"><a href="#val-clear" class="anchor"></a><code><span><span class="keyword">val</span> clear : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>clear a</code> is <code>truncate a 0</code>, it removes all the elements of <code>a</code>.</p></div></div><h2 id="iteration"><a href="#iteration" class="anchor"></a>Iteration</h2><p>The iteration functions traverse the elements of a dynamic array. Traversals of <code>a</code> are computed in increasing index order: from the element of index <code>0</code> to the element of index <code>length a - 1</code>.</p><p>It is a programming error to change the length of an array (by adding or removing elements) during an iteration on the array. Any iteration function will fail with <code>Invalid_argument</code> if it detects such a length change.</p><div class="odoc-spec"><div class="spec value anchored" id="val-iter"><a href="#val-iter" class="anchor"></a><code><span><span class="keyword">val</span> iter : <span><span>(<span><span class="type-var">'a</span> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>iter f a</code> calls <code>f</code> on each element of <code>a</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iteri"><a href="#val-iteri" class="anchor"></a><code><span><span class="keyword">val</span> iteri : <span><span>(<span>int <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>iteri f a</code> calls <code>f i x</code> for each <code>x</code> at index <code>i</code> in <code>a</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-map"><a href="#val-map" class="anchor"></a><code><span><span class="keyword">val</span> map : <span><span>(<span><span class="type-var">'a</span> <span class="arrow">-></span></span> <span class="type-var">'b</span>)</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'b</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>map f a</code> is a new array of elements of the form <code>f x</code> for each element <code>x</code> of <code>a</code>.</p><p>For example, if the elements of <code>a</code> are <code>x0</code>, <code>x1</code>, <code>x2</code>, then the elements of <code>b</code> are <code>f x0</code>, <code>f x1</code>, <code>f x2</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mapi"><a href="#val-mapi" class="anchor"></a><code><span><span class="keyword">val</span> mapi : <span><span>(<span>int <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <span class="arrow">-></span></span> <span class="type-var">'b</span>)</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'b</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>mapi f a</code> is a new array of elements of the form <code>f i x</code> for each element <code>x</code> of <code>a</code> at index <code>i</code>.</p><p>For example, if the elements of <code>a</code> are <code>x0</code>, <code>x1</code>, <code>x2</code>, then the elements of <code>b</code> are <code>f 0 x0</code>, <code>f 1 x1</code>, <code>f 2 x2</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-fold_left"><a href="#val-fold_left" class="anchor"></a><code><span><span class="keyword">val</span> fold_left : <span><span>(<span><span class="type-var">'acc</span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <span class="arrow">-></span></span> <span class="type-var">'acc</span>)</span> <span class="arrow">-></span></span> <span><span class="type-var">'acc</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span class="type-var">'acc</span></span></code></div><div class="spec-doc"><p><code>fold_left f acc a</code> folds <code>f</code> over <code>a</code> in order, starting with accumulator <code>acc</code>.</p><p>For example, if the elements of <code>a</code> are <code>x0</code>, <code>x1</code>, then <code>fold f acc a</code> is</p><pre class="language-ocaml"><code>let acc = f acc x0 in
|
||
let acc = f acc x1 in
|
||
acc</code></pre></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-fold_right"><a href="#val-fold_right" class="anchor"></a><code><span><span class="keyword">val</span> fold_right : <span><span>(<span><span class="type-var">'a</span> <span class="arrow">-></span></span> <span><span class="type-var">'acc</span> <span class="arrow">-></span></span> <span class="type-var">'acc</span>)</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'acc</span> <span class="arrow">-></span></span> <span class="type-var">'acc</span></span></code></div><div class="spec-doc"><p><code>fold_right f a acc</code> computes <code>f x0 (f x1 (... (f xn acc) ...))</code> where <code>x0</code>, <code>x1</code>, ..., <code>xn</code> are the elements of <code>a</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-exists"><a href="#val-exists" class="anchor"></a><code><span><span class="keyword">val</span> exists : <span><span>(<span><span class="type-var">'a</span> <span class="arrow">-></span></span> bool)</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p><code>exists f a</code> is <code>true</code> if some element of <code>a</code> satisfies <code>f</code>.</p><p>For example, if the elements of <code>a</code> are <code>x0</code>, <code>x1</code>, <code>x2</code>, then <code>exists f a</code> is <code>f x0 || f x1 || f x2</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-for_all"><a href="#val-for_all" class="anchor"></a><code><span><span class="keyword">val</span> for_all : <span><span>(<span><span class="type-var">'a</span> <span class="arrow">-></span></span> bool)</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p><code>for_all f a</code> is <code>true</code> if all elements of <code>a</code> satisfy <code>f</code>. This includes the case where <code>a</code> is empty.</p><p>For example, if the elements of <code>a</code> are <code>x0</code>, <code>x1</code>, then <code>exists f a</code> is <code>f x0 && f x1 && f x2</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-filter"><a href="#val-filter" class="anchor"></a><code><span><span class="keyword">val</span> filter : <span><span>(<span><span class="type-var">'a</span> <span class="arrow">-></span></span> bool)</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>filter f a</code> is a new array of all the elements of <code>a</code> that satisfy <code>f</code>. In other words, it is an array <code>b</code> such that, for each element <code>x</code> in <code>a</code> in order, <code>x</code> is added to <code>b</code> if <code>f x</code> is <code>true</code>.</p><p>For example, <code>filter (fun x -> x >= 0) a</code> is a new array of all non-negative elements of <code>a</code>, in order.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-filter_map"><a href="#val-filter_map" class="anchor"></a><code><span><span class="keyword">val</span> filter_map : <span><span>(<span><span class="type-var">'a</span> <span class="arrow">-></span></span> <span><span class="type-var">'b</span> option</span>)</span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'b</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>filter_map f a</code> is a new array of elements <code>y</code> such that <code>f x</code> is <code>Some y</code> for an element <code>x</code> of <code>a</code>. In others words, it is an array <code>b</code> such that, for each element <code>x</code> of <code>a</code> in order:</p><ul><li>if <code>f x = Some y</code>, then <code>y</code> is added to <code>b</code>,</li><li>if <code>f x = None</code>, then no element is added to <code>b</code>.</li></ul><p>For example, <code>filter_map int_of_string_opt inputs</code> returns a new array of integers read from the strings in <code>inputs</code>, ignoring strings that cannot be converted to integers.</p></div></div><h2 id="conversions"><a href="#conversions" class="anchor"></a>Conversions to other data structures</h2><p>Note: the <code>of_*</code> functions raise <code>Invalid_argument</code> if the length needs to grow beyond <a href="../Sys/index.html#val-max_array_length"><code>Sys.max_array_length</code></a>.</p><p>The <code>to_*</code> functions, except those specifically marked "reentrant", iterate on their dynarray argument. In particular it is a programming error if the length of the dynarray changes during their execution, and the conversion functions raise <code>Invalid_argument</code> if they observe such a change.</p><div class="odoc-spec"><div class="spec value anchored" id="val-of_array"><a href="#val-of_array" class="anchor"></a><code><span><span class="keyword">val</span> of_array : <span><span><span class="type-var">'a</span> array</span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>of_array arr</code> returns a dynamic array corresponding to the fixed-sized array <code>a</code>. Operates in <code>O(n)</code> time by making a copy.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_array"><a href="#val-to_array" class="anchor"></a><code><span><span class="keyword">val</span> to_array : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> array</span></span></code></div><div class="spec-doc"><p><code>to_array a</code> returns a fixed-sized array corresponding to the dynamic array <code>a</code>. This always allocate a new array and copies elements into it.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_list"><a href="#val-of_list" class="anchor"></a><code><span><span class="keyword">val</span> of_list : <span><span><span class="type-var">'a</span> list</span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>of_list l</code> is the array containing the elements of <code>l</code> in the same order.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_list"><a href="#val-to_list" class="anchor"></a><code><span><span class="keyword">val</span> to_list : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> list</span></span></code></div><div class="spec-doc"><p><code>to_list a</code> is a list with the elements contained in the array <code>a</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_seq"><a href="#val-of_seq" class="anchor"></a><code><span><span class="keyword">val</span> of_seq : <span><span><span class="type-var">'a</span> <a href="../Seq/index.html#type-t">Seq.t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div><div class="spec-doc"><p><code>of_seq seq</code> is an array containing the same elements as <code>seq</code>.</p><p>It traverses <code>seq</code> once and will terminate only if <code>seq</code> is finite.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_seq"><a href="#val-to_seq" class="anchor"></a><code><span><span class="keyword">val</span> to_seq : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="../Seq/index.html#type-t">Seq.t</a></span></span></code></div><div class="spec-doc"><p><code>to_seq a</code> is the sequence of elements <code>get a 0</code>, <code>get a 1</code>... <code>get a (length a - 1)</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_seq_reentrant"><a href="#val-to_seq_reentrant" class="anchor"></a><code><span><span class="keyword">val</span> to_seq_reentrant : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="../Seq/index.html#type-t">Seq.t</a></span></span></code></div><div class="spec-doc"><p><code>to_seq_reentrant a</code> is a reentrant variant of <a href="#val-to_seq"><code>to_seq</code></a>, in the sense that one may still access its elements after the length of <code>a</code> has changed.</p><p>Demanding the <code>i</code>-th element of the resulting sequence (which can happen zero, one or several times) will access the <code>i</code>-th element of <code>a</code> at the time of the demand. The sequence stops if <code>a</code> has less than <code>i</code> elements at this point.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_seq_rev"><a href="#val-to_seq_rev" class="anchor"></a><code><span><span class="keyword">val</span> to_seq_rev : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="../Seq/index.html#type-t">Seq.t</a></span></span></code></div><div class="spec-doc"><p><code>to_seq_rev a</code> is the sequence of elements <code>get a (l - 1)</code>, <code>get a (l - 2)</code>... <code>get a 0</code>, where <code>l</code> is <code>length a</code> at the time <code>to_seq_rev</code> is invoked.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_seq_rev_reentrant"><a href="#val-to_seq_rev_reentrant" class="anchor"></a><code><span><span class="keyword">val</span> to_seq_rev_reentrant : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="../Seq/index.html#type-t">Seq.t</a></span></span></code></div><div class="spec-doc"><p><code>to_seq_rev_reentrant a</code> is a reentrant variant of <a href="#val-to_seq_rev"><code>to_seq_rev</code></a>, in the sense that one may still access its elements after the length of <code>a</code> has changed.</p><p>Elements that have been removed from the array by the time they are demanded in the sequence are skipped.</p></div></div><h2 id="advanced"><a href="#advanced" class="anchor"></a>Advanced topics for performance</h2><h3 id="capacity"><a href="#capacity" class="anchor"></a>Backing array, capacity</h3><p>Internally, a dynamic array uses a <b>backing array</b> (a fixed-size array as provided by the <a href="../Array/index.html"><code>Array</code></a> module) whose length is greater or equal to the length of the dynamic array. We define the <b>capacity</b> of a dynamic array as the length of its backing array.</p><p>The capacity of a dynamic array is relevant in advanced scenarios, when reasoning about the performance of dynamic array programs:</p><ul><li>The memory usage of a dynamic array is proportional to its capacity, rather than its length.</li><li>When there is no empty space left at the end of the backing array, adding elements requires allocating a new, larger backing array.</li></ul><p>The implementation uses a standard exponential reallocation strategy which guarantees amortized constant-time operation; in particular, the total capacity of all backing arrays allocated over the lifetime of a dynamic array is at worst proportional to the total number of elements added.</p><p>In other words, users need not care about capacity and reallocations, and they will get reasonable behavior by default. However, in some performance-sensitive scenarios the functions below can help control memory usage or guarantee an optimal number of reallocations.</p><div class="odoc-spec"><div class="spec value anchored" id="val-capacity"><a href="#val-capacity" class="anchor"></a><code><span><span class="keyword">val</span> capacity : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p><code>capacity a</code> is the length of <code>a</code>'s backing array.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-ensure_capacity"><a href="#val-ensure_capacity" class="anchor"></a><code><span><span class="keyword">val</span> ensure_capacity : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>ensure_capacity a n</code> makes sure that the capacity of <code>a</code> is at least <code>n</code>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Invalid_argument"><code>Invalid_argument</code></a> <p>if the requested capacity is outside the range <code>0 .. Sys.max_array_length</code>.</p><p>An example would be to reimplement <a href="#val-of_array"><code>of_array</code></a> without using <a href="#val-init"><code>init</code></a>:</p><pre class="language-ocaml"><code>let of_array arr =
|
||
let a = Dynarray.create () in
|
||
Dynarray.ensure_capacity a (Array.length arr);
|
||
Array.iter (fun v -> add_last a v) arr</code></pre><p>Using <code>ensure_capacity</code> guarantees that at most one reallocation will take place, instead of possibly several.</p><p>Without this <code>ensure_capacity</code> hint, the number of resizes would be logarithmic in the length of <code>arr</code>, creating a constant-factor slowdown noticeable when <code>arr</code> is large.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-ensure_extra_capacity"><a href="#val-ensure_extra_capacity" class="anchor"></a><code><span><span class="keyword">val</span> ensure_extra_capacity : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>ensure_extra_capacity a n</code> is <code>ensure_capacity a (length a + n)</code>, it makes sure that <code>a</code> has room for <code>n</code> extra items.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Invalid_argument"><code>Invalid_argument</code></a> <p>if the total requested capacity is outside the range <code>0 .. Sys.max_array_length</code>.</p><p>A use case would be to implement <a href="#val-append_array"><code>append_array</code></a>:</p><pre class="language-ocaml"><code>let append_array a arr =
|
||
ensure_extra_capacity a (Array.length arr);
|
||
Array.iter (fun v -> add_last a v) arr</code></pre></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-fit_capacity"><a href="#val-fit_capacity" class="anchor"></a><code><span><span class="keyword">val</span> fit_capacity : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>fit_capacity a</code> reallocates a backing array if necessary, so that the resulting capacity is exactly <code>length a</code>, with no additional empty space at the end. This can be useful to make sure there is no memory wasted on a long-lived array.</p><p>Note that calling <code>fit_capacity</code> breaks the amortized complexity guarantees provided by the default reallocation strategy. Calling it repeatedly on an array may have quadratic complexity, both in time and in total number of words allocated.</p><p>If you know that a dynamic array has reached its final length, which will remain fixed in the future, it is sufficient to call <code>to_array</code> and only keep the resulting fixed-size array. <code>fit_capacity</code> is useful when you need to keep a dynamic array for eventual future resizes.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-set_capacity"><a href="#val-set_capacity" class="anchor"></a><code><span><span class="keyword">val</span> set_capacity : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>set_capacity a n</code> reallocates a backing array if necessary, so that the resulting capacity is exactly <code>n</code>. In particular, all elements of index <code>n</code> or greater are removed.</p><p>Like <a href="#val-fit_capacity"><code>fit_capacity</code></a>, this function breaks the amortized complexity guarantees provided by the reallocation strategy. Calling it repeatedly on an array may have quadratic complexity, both in time and in total number of words allocated.</p><p>This is an advanced function; in particular, <a href="#val-ensure_capacity"><code>ensure_capacity</code></a> should be preferred to increase the capacity, as it preserves those amortized guarantees.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <a href="../index.html#exception-Invalid_argument"><code>Invalid_argument</code></a> <p>if <code>n < 0</code>.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-reset"><a href="#val-reset" class="anchor"></a><code><span><span class="keyword">val</span> reset : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>reset a</code> clears <code>a</code> and replaces its backing array by an empty array.</p><p>It is equivalent to <code>set_capacity a 0</code> or <code>clear a; fit_capacity a</code>.</p></div></div><h3 id="noleaks"><a href="#noleaks" class="anchor"></a>No leaks: preservation of memory liveness</h3><p>The user-provided values reachable from a dynamic array <code>a</code> are exactly the elements in the positions <code>0</code> to <code>length a - 1</code>. In particular, no user-provided values are "leaked" by being present in the backing array in position <code>length a</code> or later.</p><h3 id="memory_layout"><a href="#memory_layout" class="anchor"></a>Memory layout of dynarrays</h3><p>In the current implementation, the backing array of an <code>'a Dynarray.t</code> is not an <code>'a array</code>, but something with the same representation as an <code>'a option array</code> or <code>'a ref array</code>. Each element is in a "box", allocated when the element is first added to the array -- see the implementation for more details.</p><p>Using an <code>'a array</code> would be delicate, as there is no obvious type-correct way to represent the empty space at the end of the backing array -- using user-provided values would either complicate the API or violate the <a href="#noleaks" title="noleaks">no leaks</a> guarantee. The constraint of remaining memory-safe under unsynchronized concurrent usage makes it even more difficult. Various unsafe ways to do this have been discussed, with no consensus on a standard implementation so far.</p><p>On a realistic automated-theorem-proving program that relies heavily on dynamic arrays, we measured the overhead of this extra "boxing" as at most 25%. We believe that the overhead for most uses of dynarray is much smaller, negligible in many cases, but you may still prefer to use your own specialized implementation for performance. (If you know that you do not need the <a href="noleaks">no leaks</a> guarantee, you can also speed up deleting elements.)</p><h2 id="examples"><a href="#examples" class="anchor"></a>Code examples</h2><h3 id="example_min_heap"><a href="#example_min_heap" class="anchor"></a>Min-heaps for mutable priority queues</h3><p>We can use dynamic arrays to implement a mutable priority queue. A priority queue provides a function to add elements, and a function to extract the minimum element -- according to some comparison function.</p><pre class="language-ocaml"><code>(* We present our priority queues as a functor
|
||
parametrized on the comparison function. *)
|
||
module Heap (Elem : Map.OrderedType) : sig
|
||
type t
|
||
val create : unit -> t
|
||
val add : t -> Elem.t -> unit
|
||
val pop_min : t -> Elem.t option
|
||
end = struct
|
||
|
||
(* Our priority queues are implemented using the standard "min heap"
|
||
data structure, a dynamic array representing a binary tree. *)
|
||
type t = Elem.t Dynarray.t
|
||
let create = Dynarray.create
|
||
|
||
(* The node of index [i] has as children the nodes of index [2 * i + 1]
|
||
and [2 * i + 2] -- if they are valid indices in the dynarray. *)
|
||
let left_child i = 2 * i + 1
|
||
let right_child i = 2 * i + 2
|
||
let parent_node i = (i - 1) / 2
|
||
|
||
(* We use indexing operators for convenient notations. *)
|
||
let ( .!() ) = Dynarray.get
|
||
let ( .!()<- ) = Dynarray.set
|
||
|
||
(* Auxiliary functions to compare and swap two elements
|
||
in the dynamic array. *)
|
||
let order h i j =
|
||
Elem.compare h.!(i) h.!(j)
|
||
|
||
let swap h i j =
|
||
let v = h.!(i) in
|
||
h.!(i) <- h.!(j);
|
||
h.!(j) <- v
|
||
|
||
(* We say that a heap respects the "heap ordering" if the value of
|
||
each node is smaller than the value of its children. The
|
||
algorithm manipulates arrays that respect the heap algorithm,
|
||
except for one node whose value may be too small or too large.
|
||
|
||
The auxiliary functions [heap_up] and [heap_down] take
|
||
such a misplaced value, and move it "up" (respectively: "down")
|
||
the tree by permuting it with its parent value (respectively:
|
||
a child value) until the heap ordering is restored. *)
|
||
|
||
let rec heap_up h i =
|
||
if i = 0 then () else
|
||
let parent = parent_node i in
|
||
if order h i parent < 0 then
|
||
(swap h i parent; heap_up h parent)
|
||
|
||
and heap_down h ~len i =
|
||
let left, right = left_child i, right_child i in
|
||
if left >= len then () (* no child, stop *) else
|
||
let smallest =
|
||
if right >= len then left (* no right child *) else
|
||
if order h left right < 0 then left else right
|
||
in
|
||
if order h i smallest > 0 then
|
||
(swap h i smallest; heap_down h ~len smallest)
|
||
|
||
let add h s =
|
||
let i = Dynarray.length h in
|
||
Dynarray.add_last h s;
|
||
heap_up h i
|
||
|
||
let pop_min h =
|
||
if Dynarray.is_empty h then None
|
||
else begin
|
||
(* Standard trick: swap the 'best' value at index 0
|
||
with the last value of the array. *)
|
||
let last = Dynarray.length h - 1 in
|
||
swap h 0 last;
|
||
(* At this point [pop_last] returns the 'best' value,
|
||
and leaves a heap with one misplaced element at position 0. *)
|
||
let best = Dynarray.pop_last h in
|
||
(* Restore the heap ordering -- does nothing if the heap is empty. *)
|
||
heap_down h ~len:last 0;
|
||
Some best
|
||
end
|
||
end</code></pre><p>The production code from which this example was inspired includes logic to free the backing array when the heap becomes empty, only in the case where the capacity is above a certain threshold. This can be done by calling the following function from <code>pop</code>:</p><pre class="language-ocaml"><code>let shrink h =
|
||
if Dynarray.length h = 0 && Dynarray.capacity h > 1 lsl 18 then
|
||
Dynarray.reset h</code></pre><p>The <code>Heap</code> functor can be used to implement a sorting function, by adding all elements into a priority queue and then extracting them in order.</p><pre class="language-ocaml"><code>let heap_sort (type a) cmp li =
|
||
let module Heap = Heap(struct type t = a let compare = cmp end) in
|
||
let heap = Heap.create () in
|
||
List.iter (Heap.add heap) li;
|
||
List.map (fun _ -> Heap.pop_min heap |> Option.get) li</code></pre></div></body></html>
|