1 (* This module implements resizable arrays, also known as vectors,
  2    for short. *)
  3 
  4 mutable data vector a =
  5   Vector {
  6     (* A default function, used to initialize new locations when the
  7        vector is enlarged. *)
  8     default: int -> a;
  9     (* The array's logical size. It is always less than or equal
 10        to the length of the array [table]. *)
 11     size: int;
 12     (* The underlying array. The length of this array is arbitrary,
 13        but is of course at least [size]. *)
 14     (* For the moment, I am using an array of options, with the
 15        invariant property that every slot below [size] is [Some].
 16        If we had permissions for array segments, then we would be
 17        able to encode this invariant and get rid of the option,
 18        I suppose. TEMPORARY that would be nice! *)
 19     table: array (option a)
 20   }
 21 
 22 val minimum_length =
 23   16 (* must be non-zero *)
 24 
 25 val new_length (length: int, size: int) : int =
 26   (* By default, we double the vector's length until it reaches the
 27      requested size or exceeds [array::max_length]. *)
 28   let length =
 29     max (
 30       minimum_length,
 31       (array::above (length, size))
 32     )
 33   in
 34   if size <= length then
 35     length
 36   else if size <= array::max_length then
 37     size
 38   else
 39     (* The requested size is too large. *)
 40     fail
 41 
 42 val init [a] (size: int, default: int -> a, f: int -> a) : vector a =
 43   let length = new_length (0, size) in
 44   Vector {
 45     default = default;
 46     size = size;
 47     table = array::init (Up, length, fun (i: int) : option a =
 48       if i < size then some (f i) else None
 49     )
 50   }
 51 
 52 val grab [a] (consumes r: array a, default: int -> a) : vector a =
 53   (* We take the ownership of [r]. We replace every element [x]
 54      with [some x], so as to make it an array of type [option a]. *)
 55   array::transform (Up, r, fun (_: int, consumes x: a) : option a = some x);
 56   Vector {
 57     default = default;
 58     size = array::length r;
 59     table = r
 60   }
 61 
 62 val list2vector [a] (consumes xs: list::list a, default: int -> a) : vector a =
 63   grab (list::list2array xs, default)
 64 
 65 val create [a] (default: int -> a) : vector a =
 66   init (0, default, fun (i : int) : a = fail)
 67 
 68 val size [a] (v: vector a) : int =
 69   v.size
 70 
 71 val resize [a] (v: vector a, new_size: int) : () =
 72   if new_size < 0 then
 73     fail;
 74   let old_size = v.size in
 75   if new_size <> old_size then begin
 76     (* Update the logical size of the vector. *)
 77     v.size <- new_size;
 78     let table = v.table in
 79     if new_size < old_size then
 80       (* The logical size of the vector decreases. *)
 81       (* Avoid a memory leak. *)
 82       (* TEMPORARY we would like to use:
 83          array::fill_segment (table, new_size, n, None);
 84          but this is not currently possible, see comment in [array.mz];
 85          so, instead, we must use an explicit loop: *)
 86       array::iter_segment (Up, new_size, old_size, fun (k: int | table @ array (option a)) : () =
 87           array::set (table, k, None)
 88       )
 89     else begin
 90       (* The logical size of the vector increases. *)
 91       v.size <- new_size;
 92       let old_length = array::length table in
 93       if new_size > old_length then begin
 94         let new_length = new_length (old_length, new_size) in
 95         (* The physical size of the array must increase. *)
 96         (* The array [table'] is initialized with [None], a duplicable value,
 97            so [array::create] can be used. Thus, [table'] has type [array None].
 98            Because [array] is covariant, [table'] also has type [array (option a)],
 99            and is a suitable argument for [array::steal]. *)
100         let table' = array::create [None] (new_length, None) in
101         array::steal [option a] (table, table', 0);
102         v.table <- table'
103       end;
104       (* Initialize the new elements. *)
105       array::iter_segment (Up, old_size, new_size, fun (k: int | v @ vector a) : () =
106         array::set (v.table, k, some (v.default k))
107       )
108     end
109   end
110 
111 val shrink [a] (v: vector a, delta: int) : () =
112   if delta < 0 then
113     fail;
114   resize (v, size v - delta)
115 
116 val pop [a] (v: vector a) : () =
117   resize (v, size v - 1)
118 
119 val get [a] duplicable a => (v: vector a, i: int) : a =
120   if i >= 0 && i < v.size then
121     option::force (array::get (v.table, i))
122   else
123     fail
124 
125 val set [a] (v: vector a, i: int, consumes x: a) : () =
126   if i >= 0 && i < v.size then
127     array::set (v.table, i, some x)
128   else
129     fail
130 
131 val push [a] (v: vector a, consumes x: a) : () =
132   let i = size v in
133   resize (v, i + 1);
134   array::set (v.table, i, some x)
135 
136 val last [a] duplicable a => (v: vector a) : a =
137   get (v, size v - 1)
138 
139 val sort [a, p : perm] duplicable a => (v: vector a, cmp: (a, a | p) -> int | p) : () =
140   (* We must define a comparison function over options. *)
141   let cmp (x: option a, y: option a | p) : int =
142     cmp (option::force x, option::force y)
143   in
144   (* The cool thing is, we do not need to copy the array in order to
145      sort an initial segment of it. *)
146   array::sort_initial_segment (cmp, v.table, v.size)
147 
148 (* TEMPORARY ideally, we should provide more operations over vectors,
149    taking inspiration from the array library. Can we avoid duplication?
150    One option would be for the vector to expose the underlying array;
151    this would be somewhat inelegant, but less dangerous than in a normal
152    programming language, because the type-checker would check that the
153    ownership of the array is returned before the vector can be used again.
154    Another option would be to to define a library of operations that work
155    uniformly on arrays, vectors, and other random access containers. *)
156 
157 (* API differences with Cubicle's common/vec.ml:
158 
159    Vec.get raises Not_found if the element is equal to the default element
160    (this seems strange, and I don't think this feature is exploited).
161 
162    Vec.set automatically increases the array's logical size if required but
163    does not increase its physical length (this seems strange). Our function
164    vector::set does not do this; vector::resize must be called first.
165 
166    Vec.grow_to_by_double is a bit strange, because it increases the vector's
167    physical length, but does not change its logical size. I guess this is
168    consistent with the fact that Vec.set automatically increases the vector's
169    logical size. Vec.grow_to_by_double is replaced by vector::resize here. *)
170 
171 (*
172   Local Variables:
173   compile-command: "../mezzo vector.mz"
174   End:
175 *)