Introduction to Programming in ATS:
PrevChapter 14. Dataviews as Linear DatapropsNext

Proof Functions for View-Changes

By the phrase view-change, I mean applying a function to proofs of a set of views to turn them into proofs of another set of views. As this function itself is a proof function, there is no run-time cost associated with each view-change. For instance, a proof of the at-view int32@L for any address L can be turned into a proof of a tuple of 4 at-views: int8@L, int8@L+1, int8@L+2 and int8@L+3, where int32 and int8 are types for 32-bit and 8-bit integers, respectively. Often more interesting view-changes involve recursively defined proof functions, and I present several of such cases in the rest of this section.

When implementing an array subscripting operation of O(1)-time, we need a proof function to change the view of one array into the views of two adjacently located arrays and another proof function to do precisely the opposite. Formally speaking, we need to construct the following two proof functions array_v_split and array_v_unsplit: 

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

An implementation of array_v_split is given as follows: 

primplmnt
array_v_split
  {a}{l}{n,i}(pfarr) = let
  prfun split
    {l:addr}{n,i:nat | i <= n} .<i>.
  (
    pfarr: array_v (a, l, n)
  ) : (
    array_v (a, l, i)
  , array_v (a, l+i*sizeof(a), n-i)
  ) =
    sif i > 0 then let
      prval array_v_cons (pf1, pf2arr) = pfarr
      prval (pf1res1, pf1res2) = split{..}{n-1,i-1} (pf2arr)
    in
      (array_v_cons (pf1, pf1res1), pf1res2)
    end else let
      prval EQINT () = eqint_make{i,0}((*void*))
    in
      (array_v_nil (), pfarr)
    end // end of [sif]
in
  split (pfarr)
end // end of [array_v_split]

Note that the keyword primplmnt (instead of implement) should be used for implementing proof functions. One can also choose to use the keyword primplement in place of primplmnt. Clearly, the proof function split directly encodes a proof based on mathematical induction. Following is an implementation of array_v_unsplit: 

primplmnt
array_v_unsplit
  {a}{l}{n1,n2}
  (pf1arr, pf2arr) = let
  prfun unsplit
    {l:addr}{n1,n2:nat} .<n1>.
  (
    pf1arr: array_v (a, l, n1)
  , pf2arr: array_v (a, l+n1*sizeof(a), n2)
  ) : array_v (a, l, n1+n2) =
    sif n1 > 0 then let
      prval
      array_v_cons (pf1, pf1arr) = pf1arr
      prval pfres = unsplit (pf1arr, pf2arr)
    in
      array_v_cons (pf1, pfres)
    end else let
      prval array_v_nil () = pf1arr in pf2arr
    end // end of [sif]
in
  unsplit (pf1arr, pf2arr)
end // end of [array_v_unsplit]

The proof function unsplit also directly encodes a proof based on mathematical induction.

Let us now see an even more interesting proof function for performing view-change. The interface of the proof function array_v_takeout is given as follows: 

//
prfun
array_v_takeout
  {a:t@ype}
  {l:addr}{n,i:nat | i < n}
(
  pfarr: array_v (a, l, n)
) : (a @ l+i*sizeof(a), a @ l+i*sizeof(a) -<lin,prf> array_v (a, l, n))
//

Note that the following type is for a linear proof function that takes a proof of an at-view to return a proof of an array-view: 

a @ l+i*sizeof(a) -<lin,prf> array_v (a, l, n)

As such a function essentially represents an array with one missing cell, we may simply say that array_v_takeout turns the view of an array into an at-view (for one cell) and a view for the rest of the array. By making use of array_v_takeout, we can give another implementation of arrget: 

implement
{a}(*tmp*)
arrget{l}{n,i}
  (pf | p, i) = x where {
  prval (pf1, fpf2) =
  array_v_takeout{a}{l}{n,i} (pf)
  val x = ptr_get1<a> (pf1 | ptr_add<a> (p, i))
  prval () = pf := fpf2 (pf1) // putting the cell and the rest together
} (* end of [arrget] *)

The proof function array_v_takeout can be implemented as follows: 

primplmnt
array_v_takeout
  {a}{l}{n,i}(pfarr) = let
  prfun takeout
    {l:addr}{n,i:nat | i < n} .<i>.
  (
    pfarr: array_v (a, l, n)
  ) : (
    a @ l+i*sizeof(a)
  , a @ l+i*sizeof(a) -<lin,prf> array_v (a, l, n)
  ) = let
    prval array_v_cons (pf1at, pf1arr) = pfarr
  in
    sif i > 0 then let
      prval (pfres, fpfres) = takeout{..}{n-1,i-1}(pf1arr)
    in
      (pfres, llam (pfres) => array_v_cons (pf1at, fpfres (pfres)))
    end else let
      prval EQINT () = eqint_make{i,0}((*void*))
    in
      (pf1at, llam (pf1at) => array_v_cons (pf1at, pf1arr))
    end // end of [sif]
  end // end of [takeout]
in
  takeout{l}{n,i}(pfarr)
end // end of [array_v_takeout]

Note that llam is a keyword for forming linear functons. Once a linear function is applied, it is consumed and the resource in it, if not reclaimed, moves into the result it returns.

The proof functions presented so far for view-changes are all manipulating array-views. The following one is different in this regard as it combines two views for singly-linked list segments into one: 

//
prfun
slseg_v_unsplit
  {a:t@ype}
  {l1,l2,l3:addr}{n1,n2:nat}
(
  pf1lst: slseg_v (a, l1, l2, n1), pf2lst: slseg_v (a, l2, l3, n2)
) : slseg_v (a, l1, l3, n1+n2)
//

The type of slseg_v_unsplit essentially states that a list segment from L1 to L2 that is of length N1 and another list segment from L2 to L3 that is of length N2 can be thought of as a list segment from L1 to L3 that is of length N1+N2. The following implementation of slseg_v_unsplit is largely parallel to that of array_v_unsplit: 

primplmnt
slseg_v_unsplit
  {a}(pf1lst, pf2lst) = let
  prfun unsplit
    {l1,l2,l3:addr}{n1,n2:nat} .<n1>.
  (
    pf1lst: slseg_v (a, l1, l2, n1), pf2lst: slseg_v (a, l2, l3, n2)
  ) : slseg_v (a, l1, l3, n1+n2) =
    sif n1 > 0 then let
      prval slseg_v_cons (pf1at, pf1lst) = pf1lst
    in
      slseg_v_cons (pf1at, unsplit (pf1lst, pf2lst))
    end else let
      prval slseg_v_nil () = pf1lst in pf2lst
    end // end of [sif]
in
  unsplit (pf1lst, pf2lst)
end // end of [slseg_v_unsplit]

The reader may find it interesting to give an implementation of slist_ptr_append by making use of slseg_v_unsplit.

Please find on-line the files array.dats and slist.dats, which contains the code employed for illustration in this section.

PrevHomeNext
Dataview for Singly-Linked ListsUpDataviewtypes as Linear Datatypes