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, inclusively.

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 ArraySubscriptException(). 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 array0(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 array0(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 prelude/SATS/array0.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} // a template
array0_make_elt (asz: size_t, x: a): array0 a // array creation

// a polymorphic function
fun array0_size {a:t@ype} (A: array0 a): size_t // size of an array

fun{a:t@ype} // a template
array0_get_elt_at (A: array0 a, i: size_t): a // A[i]

fun{a:t@ype} // a template
array0_set_elt_at (A: array0 a, i: size_t, x: a): void // A[i] := x

staload _(*anon*) = "prelude/DATS/array.dats"
staload _(*anon*) = "prelude/DATS/array0.dats"

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 int_of_size and size_of_int. Given a type T and two values asz and init of the types size_t and T, respectively, array0_make_elt<T> (asz, init) returns an array of the type array0 (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 array0 (T) for some T, array0_size(A) returns the size of A, which is of the type size_t.

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

fun{a:t@ype}
insertion_sort (
  A: array0 (a), cmp: (a, a) -> int
) : void = let
  val asz = array0_size (A)
  val n = int_of_size (asz)
  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.