Linear Arrays

Given a viewtype VT and integer I, the special static term @[VT][I] is a viewtype for an array of elements of the type VT (and thus the size of @[VT][I] is I times the size of VT). If VT happens to be a type (instead of viewtype), then @[VT][I] is also a type. If a linear proof of the view (@[VT][I]) @ L is available, then we say that a linear array of size I is stored at the location L in which each element is of the type VT. A view of the form @[VT][I] @ L is often referred to as an array view.

The interfaces for various functions on linear arrays can be found in the file prelude/SATS/array.sats. In particular, we have the following functions for manipulating array views:

viewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l

praxi array_v_nil :
  {a:viewt@ype} {l:addr} () -<prf> array_v (a, 0, l)

praxi array_v_unnil :
  {a:viewt@ype} {l:addr} array_v (a, 0, l) -<prf> void

praxi array_v_cons : {a:viewt@ype} {n:nat} {l:addr}
  (a @ l, array_v (a, n, l+sizeof a)) -<prf> array_v (a, n+1, l)

praxi array_v_uncons : {a:viewt@ype} {n:int | n > 0} {l:addr}
  array_v (a, n, l) -<prf> (a @ l, array_v (a, n-1, l+sizeof a))

Linear Array Creation

The following function template array_ptr_alloc can be called to allocate memory for storing an array of elements:

fun{a:viewt@ype}
  array_ptr_alloc {n:nat} (asz: int n):<>
    [l:addr | l <> null] (free_gc_v (a, n, l), array_v (a?, n, l) | ptr l)

The view constructor free_gc_v is abstract, and a proof of the view free_gc_v (a, n, l) can be thought of as a certificate that must be provided when the allocated array is to be freed. The array view array_v (a?, n, l) is for an uninitialized array of size n in which each element should be of the type a if initialized.

Linear Array Initialization

After an uninitialized array is created, it needs to be initialized for use. There are various functions for initializing linear arrays in prelude/SATS/array.sats. As an example, we implement as follows a function that initializes an array with a list of elements:

fn{a:t@ype}
  array_ptr_initialize_list {n:nat}
  (A: &(@[a?][n]) >> @[a][n], xs: list (a, n))
  :<> void = loop (view@ A | &A, xs) where {
  fun loop {n: nat} {l:addr} .<n>. ( // [loop] is tail-recursive!
      pf_arr: !array_v (a?, n, l) >> array_v (a, n, l) | p_arr: ptr l, xs: list (a, n)
    ) :<> void = case+ xs of
    | list_cons (x, xs) => let
        prval (pf1_at, pf2_arr) = array_v_uncons {a?} (pf_arr)
        val () = !p_arr := x
        val () = loop (pf2_arr | p_arr + sizeof<a>, xs)
      in
        pf_arr := array_v_cons {a} (pf1_at, pf2_arr)
      end // end of [list_cons]
    | list_nil () => let
        prval () = array_v_unnil {a?} (pf_arr) in pf_arr := array_v_nil {a} ()
      end // end of [list_nil]
  // end of [loop]
} // end of [array_ptr_initialize_list]

Note that the first argument of the function array_ptr_initialize_list is passed as a reference (call-by-reference). We use the expression view@ A for some particular left-value in which a proof of the view associated with the variable A is stored, and the expression &A for the address of the variable A.

Linear Array Subscription

Let A be an array of the type @[T][I] for some type (but not viewtype) T and integer I. For each natural number less than I, the expression A.[i], which can be used as a left-value, refers to the ith elemement of the array (where counting starts from 0). A function template array_ptr_swap is implemented as follows for swapping two elements in a given array:

fn{a:t@ype} array_ptr_swap
  {n:nat} {i,j:nat | i < n; j < n}
  (A: &(@[a][n]), i: int i, j: int j):<> void = begin
  let val tmp = A.[i] in A.[i] := A.[j]; A.[j] := tmp end
end // endof [array_ptr_swap]

The following two function templates are also available:

fun{a:t@ype} array_ptr_get_elt_at
  {n:nat} (A: &(@[a][n]), i: natLt n):<> a

fun{a:t@ype} array_ptr_set_elt_at
  {n:nat} (A: &(@[a][n]), i: natLt n, x:a):<> void

overload [] with array_ptr_get_elt_at
overload [] with array_ptr_set_elt_at

Because of the overloading of [] with both array_ptr_get_elt_at and array_ptr_set_elt_at, the function array_ptr_swap can also be implemented as follows:

fn{a:t@ype} array_ptr_swap
  {n:nat} {i,j:nat | i < n; j < n}
  (A: &(@[a][n]), i: int i, j: int j):<> void = begin
  let val tmp = A[i] in A[i] := A[j]; A[j] := tmp end
end // endof [array_ptr_swap]

The use of [i] for .[i] possibly makes the code look more conventional.

For accessing an array of linear elements, the following function template array_ptr_takeout can be used:

fun{a:viewt@ype}
  array_ptr_takeout {n,i:nat | i < n} {l0:addr} (
    pf: array_v (a, n, l0) | base: ptr l0, offset: int i
  ) :<> [l:addr] (
      a @ l
    , a @ l -<lin,prf> array_v (a, n, l0)
    | ptr l
    )
// end of [array_ptr_takeout]

Linear Array Destruction

The following function is for freeing the memory occupied by a linear array:

fun array_ptr_free {a:viewt@ype} {n:int} {l:addr}
  (pf_gc: free_gc_v (a, n, l), pf_arr: array_v (a?, n, l) | _: ptr l):<> void

Note that in order to free an array of I elements allocated at an address L, a proof of the view free_gc_v (VT, I, L) must be provided, where the viewtype VT is employed for specifying the size of each element in the array.

An Example

Linear arrays are used extensively in this implementation of FFT: fft.dats

The code used for illustration is available here.