1 (* This module implements resizable arrays, also known as vectors, 2 for short. *) 3 4 abstract vector +a 5 fact exclusive (vector a) 6 7 (* An array has a logical size -- the number of its elements -- and a 8 physical length -- the length of the underlying array. The length 9 is always greater than or equal to the size. The vector's size can 10 be increased or decreased by the user. The vector's length is under 11 the control of the implementation. *) 12 13 (* [create default] creates a new vector of size zero. The function [default] 14 is stored, and will be later invoked by [resize] when the vector is 15 enlarged in order to initialize the newly created slots. *) 16 17 val create: [a] (default: int -> a) -> vector a 18 19 (* [init (size, default, f)] creates a new vector of size [size]. The function 20 [default] serves the same purpose as in [create] above. The function [f] is 21 invoked immediately in order to initialize the [size] initial elements. *) 22 23 val init: [a] (size: int, default: int -> a, f: int -> a) -> vector a 24 25 (* [grab (r, default)] turns the array [r] into a vector of the same size. 26 [default] serves the same purpose as in [create] above. *) 27 28 val grab: [a] (consumes r: array a, default: int -> a) -> vector a 29 30 (* [list2vector (xs, default)] turns the list [xs] into a vector of the 31 same size. [default] serves the same purpose as in [create] above. *) 32 33 val list2vector: [a] (consumes xs: list::list a, default: int -> a) -> vector a 34 35 (* [size v] returns the current size of the vector [v]. *) 36 37 val size: [a] vector a -> int 38 39 (* [resize (v, new_size)] increases or decreases the size of the vector [v] 40 to [new_size]. If [new_size] is greater than the vector's current size, 41 the function [f] that was supplied at vector creation time is invoked to 42 initialize the new slots. *) 43 44 val resize: [a] (vector a, new_size: int) -> () 45 46 (* [shrink (v, delta)] is a short-hand for [resize (v, size v - delta)]. 47 [delta] must be comprised between 0 and [size v], inclusive. *) 48 49 val shrink: [a] (vector a, int) -> () 50 51 (* [pop v] is a short-hand for [shrink (v, 1)]. *) 52 53 val pop: [a] vector a -> () 54 55 (* [get (v, i)] reads the element at index [i] in the vector [v]. Because the 56 value is copied, the type [a] must be duplicable. The index [i] must be 57 comprised between 0, inclusive, and [size v], exclusive. *) 58 59 val get: [a] duplicable a => (vector a, int) -> a 60 61 (* [set (r, i, x)] sets the element at index [i] in the vector [v] to the 62 value [x]. The index [i] must be comprised between 0, inclusive, and [size 63 v], exclusive. *) 64 65 val set: [a] (vector a, int, consumes a) -> () 66 67 (* [push (v, x)] appends the element [x] at the end of the vector [v]. *) 68 69 val push: [a] (vector a, consumes a) -> () 70 71 (* [last v] returns the last element in the vector [v], that is, the element 72 at index [size v - 1]. *) 73 74 val last: [a] duplicable a => vector a -> a 75 76 (* [sort (v, cmp)] sorts the elements of the vector [v] according to the 77 ordering [cmp]. *) 78 79 val sort: [a, p : perm] duplicable a => (v: vector a, cmp: (a, a | p) -> int | p) -> () 80