Arrays

I mentioned earlier that a reference is just an array of size 1. I would now like to state that an array of size n is just n references allocated consecutively. These references can also be called cells, and they are numbered from 0 until n-1, inclusive.

Given an array of size n, an integer is a valid index for this array if it is a natural number strictly less than n. Otherwise, the integer is out of the bounds of the array. For an array named A, the expression A[i] means to fetch the content of the cell in A that is numbered i if i is a valid index for A. The expression A[i] can also be used as a left value. For instance, the assignment (A[i] := exp) means to evaluate exp to a value and then store the value into the cell in A that is numbered i if i is a valid index.

What happens if the index i in A[i] is invalid, that is, it is out of the bounds of the array A? In this case, A[i] is referred to as out-of-bounds array subscription and evaluating A[i] leads to a raised exception where the exception is ArraySubscriptExn(). One simple and reliable way to tell whether an integer is a valid index for a given array is to compare it with the size of the array at run-time. Given a type T, the type arrszref(T) is for an array paired with its size in which elements of the type T are stored. I will loosely refer to values of the type arrszref(T) as arrays from now on. In case there is a clear need to avoid potential confusion, I may also refer to them as array0-values.

Various functions and function templates on array0-values are declared in the file arrayref.sats, which is automatically loaded by atsopt. For instance, three function templates and one polymorphic function on arrays are depicted by the following interfaces:

//
fun{a:t@ype} // template
arrszref_make_elt
  (asz: size_t, x: a): arrszref a // array creation
//
// polymorphic fun:
//
fun arrszref_get_size
  {a:t@ype} (A: arrszref a): size_t // size of an array
//
fun{a:t@ype} // template
arrszref_get_elt_at (A: arrszref a, i: size_t): a // A[i]
//
fun{a:t@ype} // template
arrszref_set_elt_at (A: arrszref a, i: size_t, x: a): void // A[i] := x
//

Like in C, there are many types of integer values in ATS. The type size_t is essentially for unsigned long integers. The functions for converting between the type int and the type size_t are g0int2uint_int_size and g0uint2int_size_int. Given a type T and two values asz and init of the types size_t and T, respectively, arrszref_make_elt<T> (asz, init) returns an array of the type arrszref(T) such that the size of the array is asz and each cell in the array is initialized with the value init. Given an array A of the type arrszref(T) for some T, arrszref_get_size(A) returns the size of A, which is of the type size_t. For convenience, arrszref_get_size(A) can be written as A.size(). As for array access and update, the functions arrszref_get_elt_at and arrszref_set_elt_at can be called. For convenience, the bracket notation can be used to call these functions.

In the following program, the function template insertion_sort implements the standard insertion sort on arrays:

fun{
a:t@ype
} insertion_sort
(
  A: arrszref (a)
, cmp: (a, a) -> int
) : void = let
  val n = g0uint2int_size_int(A.size())
  fun ins (x: a, i: int):<cloref1> void =
    if i >= 0 then
    (
      if cmp (x, A[i]) < 0
        then (A[i+1] := A[i]; ins (x, i-1)) else A[i+1] := x
      // end of [if]
    ) else A[0] := x // end of [if]
  // end of [ins]
  fun loop (i: int):<cloref1> void =
    if i < n then (ins (A[i], i-1); loop (i+1)) else ()
  // end of [loop]
in
  loop (1)
end // end of [insertion_sort]

Note that the entire code in this section plus some additional code for testing is available on-line.