Chapter 16. Persistent Arrays

A persistent array of size n is just n heap-allocated cells (or references) in a row. It is persistent in the sense that the memory allocated for the array cannot be freed manually. Instead, it can only be safely reclaimed through systematic garbage collection (GC).

Given a viewtype VT, the type for persistent arrays containing N values of viewtype VT is arrayref(VT, N). Note that arrays in ATS are the same as those in C: There is no size information attached to them. The interfaces for various functions on persistent arrays can be found in the SATS file prelude/SATS/arrayref.sats, which is automatically loaded by atsopt.

There are various functions in ATSLIB for array creation. For instance, the following two are commonly used:

fun{a:t@ype} arrayref_make_elt {n:nat} (asz: size_t n, elt: a):<!wrt> arrayref(a, n) // end of [arrayref_make_elt] fun{a:t@ype} arrayref_make_listlen {n:int} (xs: list(a, n), n: int n):<!wrt> arrayref(a, n) // end of [arrayref_make_listlen]

Applied to a size and an element, arrayref_make_elt returns an array of the given size in which each cell is initialized with the given element. Applied to a list of elements and the length of the list, arrayref_make_listlen returns an array of size equal to the given length in which each cell is initialized with the corresponding element in the given list.

For reading from and writing to an array, the function templates arrayref_get_at and arrayref_set_at can be used, respectively, which are assigned the following interfaces:

fun{a:t@ype} arrayref_get_at {n:int} (A: arrayref(a, n), i: sizeLt (n)):<!ref> a fun{a:t@ype} arrayref_set_at {n:int} (A: arrayref(a, n), i: sizeLt (n), x: a):<!ref> void

Given an array A, an index i and a value v, arrayref_get_at(A, i) and arrayref_set_at(A, i, v) can be written as A[i] and A[i] := v, respectively.

As an example, the following function template reverses the content of a given array:

fun{a:t@ype} arrayref_reverse{n:nat} ( A: arrayref(a, n), n: size_t(n) ) : void = let // fun loop {i: nat | i <= n} .<n-i>. ( A: arrayref(a, n), n: size_t n, i: size_t i ) : void = let val n2 = half (n) in if i < n2 then let val tmp = A[i] val ni = pred(n)-i in A[i] := A[ni]; A[ni] := tmp; loop(A, n, succ(i)) end else () // end of [if] end // end of [loop] // in loop(A, n, i2sz(0)) end // end of [arrayref_reverse]

If the test i < n2 is changed to i <= n2, a type-error is to be reported. Why? The reason is that A[n-1-i] becomes out-of-bounds array subscripting in the case where n and i both equal zero. Given that it is very unlikely to encounter a case where an array of size 0 is involved, a bug like this, if not detected early, can be buried so scarily deep!

The careful reader may have already noticed that the sort t@ype is assigned to the template parameter a. In other words, the above implementation of arrayref_reverse cannot handle a case where the values stored in a given array are of some linear type. The reason for choosing the sort t@ype is that both arrayref_get_at and arrayref_set_at can only be applied to an array containing values of a nonlinear type. In the following implementation, the template parameter is given the sort vt@ype so that an array containing linear values, that is, values of some linear type can be handled:

fun{a:vt@ype} arrayref_reverse{n:nat} ( A: arrayref(a, n), n: size_t(n) ) : void = let // fun loop {i: nat | i <= n} .<n-i>. ( A: arrayref(a, n), n: size_t n, i: size_t i ) : void = let val n2 = half (n) in if i < n2 then let val () = arrayref_interchange(A, i, pred(n)-i) in loop(A, n, succ(i)) end else () // end of [if] end // end of [loop] // in loop(A, n, i2sz(0)) end // end of [arrayref_reverse]

The interface for the function template arrayref_interchange is given below:

fun{a:vt@ype} arrayref_interchange{n:int} (A: arrayref(a, n), i: sizeLt n, j: sizeLt n):<!ref> void // end of [arrayref_interchange]

Note that arrayref_interchange can not be implemented in terms of arrayref_get_at and arrayref_set_at (unless some form of type-unsafe code is employed).

There are various functions available for traversing an array from left to right or from right to left. Also, the following two functions can be conveniently called to traverse an array from left to right:

// fun{a:t0p} arrayref_head{n:pos} (A: arrayref(a, n)): (a) // A[0] fun{a:t0p} arrayref_tail{n:pos} (A: arrayref(a, n)): arrayref(a, n-1) // overload .head with arrayref_head overload .tail with arrayref_tail //

For instance, the fold-left function for arrays can be implemented as follows:

fun{a,b:t@ype} arrayref_foldleft{n:int} ( f: (a, b) -> a, x: a, A: arrayref(b, n), n: size_t(n) ) : a = ( if n > 0 then arrayref_foldleft<a,b> (f, f (x, A.head()), A.tail(), pred(n)) else x // end of [if] ) (* end of [arrayref_foldleft] *)

As can be expected, A.head and A.tail translate into A[0] and ptr_succ<T>(p0), respectively, where T is the type for the elements stored in A and p0 is the starting address of A.

Please find on-line the entirety of the code used in this chapter.