Dataviews

A view is a linear prop, where the meaning of the word linear is in the sense of linear logic. Dataviews are often declared to encode recursively defined relations on linear resources. As an example, we declare a dataview as follows to describe and then reason about the probably most common data structure in use: arrays.

dataview array_v (a: viewt@ype+, int, addr) =
  | {l:addr} array_v_none (a, 0, l)
  | {n:nat} {l:addr} array_v_some (a, n+1, l) of (a @ l, array_v (a, n, l+sizeof a))

The syntax introduces a view constructor array_v and two proof constructors array_v_none and array_v_some associated with array_v, which are assigned the following props:

array_v_none : {a:viewt@ype} {l:addr} () -> array_v (a, 0, l)
array_v_some : {a:viewt@ype} {n:nat} {l:addr} (a @ l, array_v (a, n, l+sizeof a)) -> array_v_some (a, n+1, l)

Given a viewtype VT, an integer I and an address L, the view array_v(VT, I, L) indicates that an array of size I is located at the address L and each element in the array is of viewtype VT.

The prop assigned to array_v_none indicates that we can assume an array of size 0 located at any given address, while the prop assigned to array_v_some states that an array of I+1 elements of viewtype VT is located at some address L if an element of viewtype VT is located at L and also an array of I elements of viewtype VT is located at L+sizeof(VT), where sizeof(VT) is the size of VT, or more precisely, the size of an element of viewtype VT.

Let us establish some propoerties on arrays. The following proof function array_v_split shows that an array of size N can be decomposed into two adjacently located arrays of sizes I and N - I, respectively, where I can be any natural number satisfying I <= N.

(*
 * array_v_split
 *   {a:viewt@ype} {n,i:nat | i <= n} {l:addr} {off: int} .<i>.
 *   (pf_arr: array_v (a, n, l), pf_mul: MUL (i, sizeof a, off))
 *   : (array_v (a, i, l), array_v (a, n-i, l+off))
 *)

prfun array_v_split
  {a:viewt@ype} {n,i:nat | i <= n} {l:addr} {off: int} .<i>.
  (pf_arr: array_v (a, n, l), pf_mul: MUL (i, sizeof a, off))
  : (array_v (a, i, l), array_v (a, n-i, l+off)) =
  sif i > 0 then let
    prval array_v_some (pf_at, pf_arr) = pf_arr
    prval MULind pf_mul = pf_mul
    prval (pf_arr1, pf_arr2) = array_v_split (pf_arr, pf_mul)
  in
    (array_v_some (pf_at, pf_arr1), pf_arr2)
  end else let
    prval MULbas () = pf_mul
  in
    (array_v_none (), pf_arr)
  end

The next proof function array_v_unsplit is the inverse of array_v_split: It states that two adjacently located arrays of sizes N_1 and N_2 can be combined into a single array of sizes N_1+N_2.

(*
 * array_v_unsplit
 *   {a:viewt@ype} {n1,n2:nat} {l:addr} {off: int} .<n1>.
 *   (pf_arr1: array_v (a, n1, l),
 *    pf_arr2: array_v (a, n2, l+off),
 *    pf_mul: MUL (n1, sizeof a, off))
 *   : array_v (a, n1+n2, l)
 *)

prfun array_v_unsplit
  {a:viewt@ype} {n1,n2:nat} {l:addr} {off: int} .<n1>.
  (pf_arr1: array_v (a, n1, l), pf_arr2: array_v (a, n2, l+off), pf_mul: MUL (n1, sizeof a, off))
  : array_v (a, n1+n2, l) =
  sif n1 > 0 then let
    prval array_v_some (pf_at, pf_arr1) = pf_arr1
    prval MULind pf_mul = pf_mul
    prval pf_arr = array_v_unsplit (pf_arr1, pf_arr2, pf_mul)
  in
    array_v_some (pf_at, pf_arr)
  end else let
    prval array_v_none () = pf_arr1
    prval MULbas () = pf_mul
  in
    pf_arr2
  end

The following proof function states that given an array of size N and a natural number I satisfying I < N, the element indexed by I can be taken out of the array, leaving the array with a hole inside.

(*
 * array_v_takeout
 *   {n,i:nat | i < n} {l:addr} {off: int}
 *   (pf_arr: array_v (a, n, l), pf_mul: MUL (i, sizeof a, off))
 *   : (a @ (l+off), a @ (l+off) -<lin> array_v (a, n, l))
 *)

prfun array_v_takeout
  {a:viewt@ype} {n,i:nat | i < n} {l:addr} {off: int} .<i>.
  (pf_arr: array_v (a, n, l), pf_mul: MUL (i, sizeof a, off))
  : (a @ (l+off), a @ (l+off) -<lin> array_v (a, n, l)) =
  sif i > 0 then let
    prval array_v_some (pf_at, pf_arr) = pf_arr
    prval MULind pf_mul = pf_mul
    prval (pf_out, pf_rst) = array_v_takeout (pf_arr, pf_mul)
  in
    (pf_out, llam pf_out => array_v_some (pf_at, pf_rst pf_out))
  end else let
    prval MULbas () = pf_mul
    prval array_v_some (pf_at, pf_arr)  = pf_arr
  in
    (pf_at, llam pf_at => array_v_some (pf_at, pf_arr))
  end

The following code shows how the proof function array_v_takeout can be used to implement functions for accessing and updating arrays.

extern // a template function for read through a pointer
fun{a:t@ype} ptr_get {l:addr} (pf: a @ l | p: ptr l): (a @ l | a)

extern // a template function for write through a pointer
fun{a:t@ype} ptr_set {l:addr} (pf: a @ l | p: ptr l, x: a): (a @ l | void)

fn{a:t@ype} // a template function for array read
  array_ptr_get_at {n,i:nat | i < n} {l:addr}
  (pf_arr: array_v (a, n, l) | p: ptr l, i: size_t i)
  : (array_v (a, n, l) | a) =
  let
    val (pf_mul | off) = mul2_size1_size1 (i, sizeof<a>)
    prval (pf_elt, pf_rst) = array_v_takeout {a} (pf_arr, pf_mul)
    val (pf_elt | x) = ptr_get<a> (pf_elt | p + off)
  in
    (pf_rst pf_elt | x)
  end

fn{a:t@ype} // a template function for array write
  array_ptr_set_at {n,i:nat | i < n} {l:addr}
  (pf_arr: array_v (a, n, l) | p: ptr l, i: size_t i, x: a)
  : (array_v (a, n, l) | void) =
  let
    val (pf_mul | off) = mul2_size1_size1 (i, sizeof<a>)
    prval (pf_elt, pf_rst) = array_v_takeout {a} (pf_arr, pf_mul)
    val (pf_elt | ()) = ptr_set<a> (pf_elt | p + off, x)
  in
    (pf_rst pf_elt | ())
  end

Note that the code here is primarily for the purpose of illustration. In practice, array access and update functions in ATS/Anairiats are implemented as primtives for the sake of efficiency.

The code used for illustration is available here.