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 *)