Many programmers are likely to find it a rather involved task to write code manipulating values of dataviewtypes. When handling a complex data structure, I myself often try to first use a datatype to model the data structure and implement some functionalities of the data structure based the datatype. I then change the datatype into a corresponding dataviewtype and modify the implementation accordingly to make it work with the dataviewtype. I now present as follows an implementation of linear red-black trees that is directly based on a previous implementation of functional red-black trees, illustrating concretely a kind of gradual transition from datatypes to dataviewtypes that can greatly reduce the level of difficulty one may otherwise encounter in an attempt to program with dataviewtypes directly.
The following declaration of dataviewtype rbtree is identical to the previous declaration of datatype rbtree except the keyword datavtype being now used instead of the keyword datatype:
#define BLK 0; #define RED 1 sortdef clr = {c:int | 0 <= c; c <= 1} datavtype rbtree ( a: t@ype+, int(*c*), int(*bh*), int(*v*) ) = // element type, color, black height, violations | rbtree_nil (a, BLK, 0, 0) of ((*void*)) | {c,cl,cr:clr}{bh:nat}{v:int} {c==BLK && v==0 || c == RED && v==cl+cr} rbtree_cons (a, c, bh+1-c, v) of (int c, rbtree0 (a, cl, bh), a, rbtree0 (a, cr, bh)) // end of [rbtree] where rbtree0 (a:t@ype, c:int, bh:int) = rbtree (a, c, bh, 0)
At the first sight, the following function template insfix_l is greatly more involved that a previous version of the same name (for manipulating functional red-black trees):
fn{ a:t@ype } insfix_l // right rotation {cl,cr:clr} {bh:nat}{v:nat} {l,l_c,l_tl,l_x,l_tr:addr} ( pf_c: int(BLK) @ l_c , pf_tl: rbtree (a, cl, bh, v) @ l_tl , pf_x: a @ l_x , pf_tr: rbtree (a, cr, bh, 0) @ l_tr | t: rbtree_cons_unfold (l, l_c, l_tl, l_x, l_tr) , p_tl: ptr (l_tl) ) : [c:clr] rbtree0 (a, c, bh+1) = let #define B BLK #define R RED #define nil rbtree_nil #define cons rbtree_cons in case+ !p_tl of | @cons (cl as R, tll as @cons (cll as R, _, _, _), _, tlr) => let // val () = cll := B prval () = fold@ (tll) // val tl = !p_tl val () = !p_tl := tlr prval () = fold@ (t) val () = tlr := t // in fold@ (tl); tl end // end of [cons (R, cons (R, ...), ...)] | @cons (cl as R, tll, _, tlr as @cons (clr as R, tlrl, _, tlrr)) => let // val tl = !p_tl val () = !p_tl := tlrr prval () = fold@ (t) val () = tlrr := t // val tlr_ = tlr val () = tlr := tlrl val () = cl := B prval () = fold@ (tl) val () = tlrl := tl // in fold@ (tlr_); tlr_ end // end of [cons (R, ..., cons (R, ...))] | _ (*rest-of-cases*) =>> (fold@ (t); t) end // end of [insfix_l]
fn{ a:t@ype } insfix_r // left rotation {cl,cr:clr} {bh:nat}{v:nat} {l,l_c,l_tl,l_x,l_tr:addr} ( pf_c: int(BLK) @ l_c , pf_tl: rbtree (a, cl, bh, 0) @ l_tl , pf_x: a @ l_x , pf_tr: rbtree (a, cr, bh, v) @ l_tr | t: rbtree_cons_unfold (l, l_c, l_tl, l_x, l_tr) , p_tr: ptr (l_tr) ) : [c:clr] rbtree0 (a, c, bh+1) = let #define B BLK #define R RED #define nil rbtree_nil #define cons rbtree_cons in case+ !p_tr of | @cons (cr as R, trl, _, trr as @cons (crr as R, _, _, _)) => let // val () = crr := B prval () = fold@ (trr) // val tr = !p_tr val () = !p_tr := trl prval () = fold@ (t) val () = trl := t // in fold@ (tr); tr end // end of [cons (R, ..., cons (R, ...))] | @cons (cr as R, trl as @cons (crr as R, trll, _, trlr), _, trr) => let // val tr = !p_tr val () = !p_tr := trll prval () = fold@ (t) val () = trll := t // val trl_ = trl val () = trl := trlr val () = cr := B prval () = fold@ (tr) val () = trlr := tr // in fold@ (trl_); trl_ end // end of [cons (R, cons (R, ...), ...)] | _ (*rest-of-cases*) =>> (fold@ (t); t) end // end of [insfix_r]
As can be expected, the following function template rbtree_insert is essentially a direct translation of the one of the same name for inserting an element into a functional red-black tree:
extern fun{a:t@ype} rbtree_insert {c:clr}{bh:nat} ( t: rbtree0 (a, c, bh), x0: &a, cmp: cmp a ) : [bh1:nat] rbtree0 (a, BLK, bh1) implement{a} rbtree_insert (t, x0, cmp) = let // #define B BLK #define R RED #define nil rbtree_nil #define cons rbtree_cons // fun ins {c:clr}{bh:nat} .<bh,c>. ( t: rbtree0 (a, c, bh), x0: &a ) : [cl:clr; v:nat | v <= c] rbtree (a, cl, bh, v) = ( case+ t of | @cons ( c, tl, x, tr ) => let prval pf_c = view@c prval pf_tl = view@tl prval pf_x = view@x prval pf_tr = view@tr val sgn = compare<a> (x0, x, cmp) in if sgn < 0 then let val [cl:int,v:int] tl_ = ins (tl, x0) val () = tl := tl_ in if (c = B) then ( insfix_l<a> (pf_c, pf_tl, pf_x, pf_tr | t, addr@tl) // end of [insfix_l] ) else let val () = c := R in fold@{a}{..}{..}{cl}(t); t end // end of [if] end else if sgn > 0 then let val [cr:int,v:int] tr_ = ins (tr, x0) val () = tr := tr_ in if (c = B) then ( insfix_r<a> (pf_c, pf_tl, pf_x, pf_tr | t, addr@tr) // end of [insfix_r] ) else let val () = c := R in fold@{a}{..}{..}{cr}(t); t end // end of [if] end else (fold@{a}{..}{..}{0} (t); t) end // end of [cons] | ~nil () => cons{a}{..}{..}{0}(R, nil, x0, nil) ) (* end of [ins] *) // val t = ins (t, x0) // in // case+ t of @cons(c as R, _, _, _) => (c := B; fold@ (t); t) | _ =>> t // end // end of [rbtree_insert]
I literally implemented the above rbtree_insert by making a copy of the previous implementation of rbtree_insert for functional red-black trees and then properly modifying it to make it pass typechecking. Although this process of copying-and-modifying is difficult to be described formally, it is fairly straightforward to follow in practice as it is almost entirely guided by the error messages issued during typechecking.
Please find the entire code in this section plus some additional code for testing on-line. A challenging as well as rewarding exercise is for the reader to implement an operation that deletes an element from a given linear red-black tree.