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:

primplement 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 primplement (instead of implement) should be used for implementing proof functions. Clearly, the proof function split directly encodes a proof based on mathematical induction. Following is an implementation of array_v_unsplit:

primplement 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]

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:

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} 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:

primplement 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)

primplement 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.