``` 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
```