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]
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
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]
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 //
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] *)
Please find on-line the entirety of the code used in this chapter.