diff git a/src/attic/resizableArray.ml b/src/attic/resizableArray.ml
deleted file mode 100644
index d79d7649deb1f68c71534a6d160369f10dcb743e..0000000000000000000000000000000000000000
 a/src/attic/resizableArray.ml
+++ /dev/null
@@ 1,51 +0,0 @@
(* This module implements resizable arrays, that is, arrays that can
 grow upon explicit request. *)

type 'a t = {
 (* The default element is used to fill empty slots. *)
 default: 'a;
 (* The logical size of this array. *)
 mutable size: int;
 (* The physical array, whose length is at least [size]. *)
 mutable table: 'a array
 }

let make capacity default =
 (* [capacity] must be nonzero, so that doubling it actually
 enlarges the array. *)
 assert (capacity >= 0);
 let capacity = if capacity = 0 then 1 else capacity in
 let table = Array.make capacity default in
 { default; size = 0; table }

let length a =
 a.size

let get a i =
 assert (0 <= i && i < a.size);
 Array.unsafe_get a.table (i)

let set a i x =
 assert (0 <= i && i < a.size);
 Array.unsafe_set a.table (i) x

let resize a s =
 assert (s >= 0);
 if s < a.size then begin
 (* The logical size of the array decreases. *)
 Array.fill a.table s (a.size  s) a.default;
 a.size < s
 end
 else if s > a.size then begin
 (* The logical size of the array increases. *)
 let n = Array.length a.table in
 if s > n then begin
 (* The physical size of the array must increase. The new size is at
 least double of the previous size, and larger if requested. *)
 let table = Array.make (max (2 * n) s) a.default in
 Array.blit a.table 0 table 0 n;
 a.table < table
 end;
 a.size < s
 end;
 assert (a.size <= Array.length a.table)
diff git a/src/attic/resizableArray.mli b/src/attic/resizableArray.mli
deleted file mode 100644
index 96ca6ef2a91e635471298c187919ee0dc1d5d46c..0000000000000000000000000000000000000000
 a/src/attic/resizableArray.mli
+++ /dev/null
@@ 1,36 +0,0 @@
(* This module implements resizable arrays, that is, arrays that can
 grow upon explicit request. *)

type 'a t

(* [make capacity x] creates a resizable array of logical length 0, whose
 physical length is initially [capacity], and whose default element is [x].
 The default element is used to fill empty slots in the physical array. *)

val make: int > 'a > 'a t

(* [length a] returns the current logical length of the array [a]. *)

val length: 'a t > int

(* [resize a n] changes the logical length of the array [a] to [n]. If the
 length decreases, any excess elements are lost. The capacity of the
 underlying physical array remains the same. If the length increases, the
 new positions are filled with the array's default element, as initially
 supplied to [make]. The capacity of the underlying physical array grows
 by at least a factor of two. *)

val resize: 'a t > int > unit

(* [get a i] returns the element contained at offset [i] in the array [a].
 Slots are numbered 0 and up. [i] must be strictly less than the array's
 current logical length. *)

val get: 'a t > int > 'a

(* [set a i x] sets the element contained at offset [i] in the array [a]
 to [x]. Slots are numbered 0 and up. [i] must be strictly less than
 the array's current logical length. *)

val set: 'a t > int > 'a > unit

diff git a/src/resizableArray.ml b/src/resizableArray.ml
new file mode 100644
index 0000000000000000000000000000000000000000..cd0235e219fa77529ff5226d44784bafbeb0193a
 /dev/null
+++ b/src/resizableArray.ml
@@ 0,0 +1,100 @@
+(* This module implements resizable arrays, that is, arrays that can
+ grow upon explicit request. *)
+
+type 'a t = {
+ (* The default element is used to fill empty slots when growing or shrinking
+ the physical array. *)
+ default: 'a;
+ (* The init function is used to initialize newly allocated slots when
+ growing the logical array. *)
+ init: int > 'a;
+ (* The logical size of this array. *)
+ mutable size: int;
+ (* The physical array, whose length is at least [size]. *)
+ mutable table: 'a array
+ }
+
+let make capacity default init =
+ (* [capacity] must be nonzero, so that doubling it actually
+ enlarges the array. *)
+ assert (capacity >= 0);
+ let capacity = if capacity = 0 then 1 else capacity in
+ let table = Array.make capacity default in
+ { default; init; size = 0; table }
+
+let make_ capacity default =
+ make capacity default (fun _ > default)
+
+let length a =
+ a.size
+
+let get a i =
+ assert (0 <= i && i < a.size);
+ Array.unsafe_get a.table (i)
+
+let set a i x =
+ assert (0 <= i && i < a.size);
+ Array.unsafe_set a.table (i) x
+
+let shrink a s =
+ (* This is [resize a s], assuming [0 <= s < a.size]. *)
+ Array.fill a.table s (a.size  s) a.default;
+ a.size < s
+
+let grow a s =
+ (* This is [resize a s], assuming [0 <= s && a.size < s]. *)
+ let n = Array.length a.table in
+ if s > n then begin
+ (* The physical size of the array must increase. The new size is at
+ least double of the previous size, and larger if requested. *)
+ let table = Array.make (max (2 * n) s) a.default in
+ Array.blit a.table 0 table 0 n;
+ a.table < table
+ end;
+ (* From [a.size] to [s], we have new logical slots. Initialize them. *)
+ let init = a.init
+ and table = a.table in
+ for i = a.size to s  1 do
+ Array.unsafe_set table i (init i)
+ done;
+ (* Update the array's logical size. *)
+ a.size < s
+
+let resize a s =
+ assert (0 <= s);
+ if s < a.size then
+ shrink a s
+ else if s > a.size then
+ grow a s
+
+let push a x =
+ let s = a.size in (* equivalent to: [length a] *)
+ begin (* equivalent to: [resize a (s + 1)] *)
+ let s = s + 1 in
+ let n = Array.length a.table in
+ if s > n then begin
+ (* assert (s = n + 1); *)
+ (* assert (max (2 * n) s = 2 * n); *)
+ let table = Array.make (2 * n) a.default in
+ Array.blit a.table 0 table 0 n;
+ a.table < table
+ end;
+ (* No need to call [init], since there is just one new logical slot
+ and we are about to write it anyway. *)
+ a.size < s
+ end;
+ Array.unsafe_set a.table (s) x (* equivalent to: [set a s x] *)
+
+let pop a =
+ let s = a.size in (* equivalent to: [length a] *)
+ assert (s > 0);
+ let s = s  1 in
+ a.size < s;
+ let table = a.table in
+ let x = Array.unsafe_get table (s) in (* equivalent to: [get a s] *)
+ Array.unsafe_set table (s) a.default; (* equivalent to: [resize a s] *)
+ x
+
+let default a =
+ a.default
+
diff git a/src/resizableArray.mli b/src/resizableArray.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bd57f08efe45aeacdbda39e942e3101a7af631dc
 /dev/null
+++ b/src/resizableArray.mli
@@ 0,0 +1,60 @@
+(* This module implements resizable arrays, that is, arrays that can
+ grow upon explicit request. *)
+
+type 'a t
+
+(* [make capacity default init] creates a resizable array of logical length 0,
+ whose physical length is initially [capacity], and whose default element is
+ [default]. The default element is used to fill empty slots in the physical
+ array; it is otherwise irrelevant. The [init] function is used to
+ initialize new logical slots when the logical size of the array grows, so,
+ unlike [default], it is semantically meaningful. *)
+
+val make: int > 'a > (int > 'a) > 'a t
+
+(* [make_] is a simplified variant of [make] where the [init] function always
+ returns [default], i.e., where new logical slots are initialized with
+ [default] when the array is grown. *)
+
+val make_: int > 'a > 'a t
+
+(* [length a] returns the current logical length of the array [a]. *)
+
+val length: 'a t > int
+
+(* [resize a n] changes the logical length of the array [a] to [n]. If the
+ length decreases, any excess elements are lost. The capacity of the
+ underlying physical array remains the same. If the length increases, the
+ new positions are filled with the array's default element, as initially
+ supplied to [make]. The capacity of the underlying physical array grows
+ by at least a factor of two. *)
+
+val resize: 'a t > int > unit
+
+(* [get a i] returns the element contained at offset [i] in the array [a].
+ Slots are numbered 0 and up. [i] must be strictly less than the array's
+ current logical length. *)
+
+val get: 'a t > int > 'a
+
+(* [set a i x] sets the element contained at offset [i] in the array [a]
+ to [x]. Slots are numbered 0 and up. [i] must be strictly less than
+ the array's current logical length. *)
+
+val set: 'a t > int > 'a > unit
+
+(* [push a x] appends the element [x] at the end of the array [a], whose
+ length increases by one. *)
+
+val push: 'a t > 'a > unit
+
+(* [pop a] removes the element [x] found at the end of the array [a], whose
+ length decreases by one. The array must have nonzero length. *)
+
+val pop: 'a t > 'a
+
+(* [default a] returns the default value that was used when the array [a]
+ was created. This should be seldom useful, but can be convenient. *)
+
+val default: 'a t > 'a
+