Dataview for Linear Arrays

Unlike in most programming languages, arrays are not a primitive data structure in ATS. More specifically, persistent arrays can be implemented based on linear arrays, which allow for being freed safely by the programmer, and linear arrays can be implemented based on at-views. Intuitively, the view for an array storing N elements of type T consists of N at-views: T@L₀, T@L₁, ..., and T@L_N-1, where L₀ is the starting address of the array and each subsequent L equals the previous one plus the size of T, that is, the number of bytes needed to store a value of the type T. The following declared dataview array_v precisely captures this intuituion:

dataview
array_v (
  a:t@ype+ // covariant argument
, addr(*beg*)
, int(*size*)
) = // array_v
  | {l:addr}
    array_v_nil (a, l, 0)
  | {l:addr}{n:nat}
    array_v_cons (a, l, n+1) of (a @ l, array_v (a, l+sizeof(a), n))
// end of [array_v]

Given a type T, an address L and an integer N, array_v(T, L, N) is a view for the array starting at L that stores N elements of the type T. As can be readily expected, the function templates for array-accessing and array-updating are given the following interfaces:

//
fun{
a:t@ype
} arrget{l:addr}{n,i:nat | i < n}
  (pf: !array_v (a, l, n) | p: ptr l, i: int i): a
// end of [arrget] // end of [fun]
//
fun{
a:t@ype
} arrset{l:addr}{n,i:nat | i < n}
  (pf: !array_v (a, l, n) | p: ptr l, i: int i, x: a): void
// end of [arrset] // end of [fun]
//

Before implementing arrget and arrset, I present as follows some code that implements a function template to access the first element of a nonempty array:

fun{
a:t@ype
} arrgetfst{l:addr}{n:pos}
(
  pf: !array_v (a, l, n) | p: ptr l
) : a = x where {
  prval array_v_cons (pf1, pf2) = pf
  // pf1: a @ l; pf2: array_v (a, l+sizeof(a), n-1)
  val x = !p
  prval () = pf := array_v_cons (pf1, pf2)
} // end of [arrgetfst]

Obviously, the function template arrget can be implemented based on arrgetfst:

implement
{a}(*tmp*)
arrget (pf | p, i) =
  if i > 0 then let
    prval array_v_cons (pf1, pf2) = pf
    val x = arrget (pf2 | ptr_succ<a> (p), i-1)
    prval () = pf := array_v_cons (pf1, pf2)
  in
    x
  end else
    arrgetfst (pf | p)
  // end of [if]

This is a tail-recursive implementation of time-complexity O(n). However, the very point of having arrays is to support O(1)-time accessing and updating operations. My initial effort spent on implementing such operations immediately dawned on me the need to construct proof functions for supporting view-changes (of no run-time cost).

Clearly, an array starting at L that stores N elements of type T can also be thought of as two arrays: one starting at L that stores I elements while the other starting at L+I*sizeof(T) that stores N-I elements, where I is an natural number less that or equal to N. Formally, this statement can be encoded in the type of the proof function array_v_split:

prfun
array_v_split
  {a:t@ype}
  {l:addr}{n,i:nat | i <= n}
(
  pfarr: array_v (a, l, n)
) : (array_v (a, l, i), array_v (a, l+i*sizeof(a), n-i))

The other direction of the above statement can be encoded in the type of the proof function array_v_unsplit:

prfun
array_v_unsplit
  {a:t@ype}
  {l:addr}{n1,n2:nat}
(
  pf1arr: array_v (a, l, n1), pf2arr: array_v (a, l+n1*sizeof(a), n2)
) : array_v (a, l, n1+n2)

With array_v_split and array_v_unsplit, we can readily give implementations of arrget and arrset that are O(1)-time:

implement
{a}(*tmp*)
arrget{l}{n,i}
  (pf | p, i) = x where {
  prval (pf1, pf2) = array_v_split{a}{l}{n,i}(pf)
  prval array_v_cons (pf21, pf22) = pf2
  val x = ptr_get1<a> (pf21 | ptr_add<a> (p, i))
  prval pf2 = array_v_cons (pf21, pf22)
  prval () = pf := array_v_unsplit{a}{l}{i,n-i}(pf1, pf2)
} (* end of [arrget] *)

implement
{a}(*tmp*)
arrset{l}{n,i}
  (pf | p, i, x) = () where {
  prval (pf1, pf2) = array_v_split{a}{l}{n,i}(pf)
  prval array_v_cons (pf21, pf22) = pf2
  val () = ptr_set1<a> (pf21 | ptr_add<a> (p, i), x)
  prval pf2 = array_v_cons (pf21, pf22)
  prval () = pf := array_v_unsplit{a}{l}{i,n-i}(pf1, pf2)
} (* end of [arrset] *)

Of course, the proof functions array_v_split and array_v_split are still to be implemented, which I will do when covering the topic of view-change.

Given a type T, an address L and a natural number N, a proof of the view array_v(T?, L, N) can be obtained and released by calling the functions malloc and free, respectively, which are to be explained in details elsewhere. I now give as follows an implemention of a function template for array intialization:

typedef natLt (n:int) = [i:nat | i < n] int (i)

fun{a:t@ype}
array_ptr_tabulate
  {l:addr}{n:nat}
(
  pf: !array_v (a?,l,n) >> array_v (a,l,n)
| p: ptr (l), n: int (n), f: natLt(n) -<cloref1> a
) : void = let
  fun loop{l:addr}
    {i:nat | i <= n} .<n-i>.
  (
    pf: !array_v (a?,l,n-i) >> array_v (a,l,n-i)
  | p: ptr l, n: int n, f: natLt(n) -<cloref1> a, i: int i
  ) : void =
    if i < n then let
      prval array_v_cons (pf1, pf2) = pf
      val () = !p := f (i)
      val () = loop (pf2 | ptr_succ<a> (p), n, f, i+1)
    in
      pf := array_v_cons (pf1, pf2)
    end else let
      prval array_v_nil () = pf in pf := array_v_nil {a} ()
    end // end of [if]
  // end of [loop]
in
  loop (pf | p, n, f, 0)
end // end of [array_ptr_tabulate]

Given a natural number n, the type natLt(n) is for all natural numbers less than n. Given a type T, the function array_ptr_tabulate<T> takes a pointer to an uninitialized array, the size of the array and a function f that maps each natural number less than n to a value of the type T, and it initializes the array with the sequence of values of f(0), f(1), ..., and f(n-1). In other words, the array stores a tabulation of the given function f after the initialization is over.

Given a type T and an integer N, @[T][N] is a built-in type in ATS for N consecutive values of the type T. Therefore, the at-view @[T][N]@L for any given address L is equivalent to the array-view array_v(T, L, N). By making use of the feature of call-by-reference, we can also assign the following interfaces to the previously presented functions arrget and arrset:

//
fun{
a:t@ype
} arrget {n,i:nat | i < n} (A: &(@[a][n]), i: int i): (a)
//
fun{
a:t@ype
} arrset {n,i:nat | i < n} (A: &(@[a][n]), i: int i, x: a): void
//

Please find the entirety of the above presented code on-line.