Introduction to Programming in ATS:
<<< PreviousDataviewtypes as Linear DatatypesNext >>>

Transition from Datatypes to Dataviewtypes

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 dataviewtype being now used instead of the keyword datatype: 

#define BLK 0; #define RED 1
sortdef clr = {c:int | 0 <= c; c <= 1}

dataviewtype
rbtree (
  a: t@ype, int(*c*), int(*bh*), int(*v*)
) = // element type, color, black height, violations
  | rbtree_nil (a, BLK, 0, 0) of ()
  | {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_cons]
// 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_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_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 cons rbtree_cons
in
  case+ !p_tl of
  | cons (!p_cl as R, !p_tll as cons (!p_cll as R, _, _, _), _, !p_tlr) => let
//
      val () = !p_cll := B
      val () = fold@ (!p_tll)
//
      val tl = !p_tl
      val () = !p_tl := !p_tlr
      val () = fold@ (t)
//
      val () = !p_tlr := t
    in
      fold@ (tl); tl
    end // end of [cons (R, cons (R, ...), ...)]
  | cons (!p_cl as R, !p_tll, _, !p_tlr as cons (!p_clr as R, !p_tlrl, _, !p_tlrr)) => let
//
      val tl = !p_tl
      val () = !p_tl := !p_tlrr
      val () = fold@ (t)
      val () = !p_tlrr := t
//
      val tlr = !p_tlr
      val () = !p_tlr := !p_tlrl
      val () = !p_cl := B
      val () = fold@ (tl)
      val () = !p_tlrl := tl
//
    in
      fold@ (tlr); tlr
    end // end of [cons (R, ..., cons (R, ...))]
  | _ =>> (fold@ (t); t)
end // end of [insfix_l]

However, I would like to point out that the interface for the above insfix_l is a direct translation of the interface for the previous infix_l. In other words, the previously captured relation between a tree being rotated and the one obtained from applying infix_l to it also holds in the setting of linear red-black trees. The very same statement can be made about the following function template insfix_r, which is precisely a mirror image of insfix_l: 

fn{a:t@ype}
insfix_r // left rotation
  {cl,cr:clr}
  {bh:nat}
  {v:nat}
  {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_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 cons rbtree_cons
in
  case+ !p_tr of
  | cons (!p_cr as R, !p_trl, _, !p_trr as cons (!p_crr as R, _, _, _)) => let
//
      val () = !p_crr := B
      val () = fold@ (!p_trr)
//
      val tr = !p_tr
      val () = !p_tr := !p_trl
      val () = fold@ (t)
//
      val () = !p_trl := t
    in
      fold@ (tr); tr
    end // end of [cons (R, ..., cons (R, ...))]
  | cons (!p_cr as R, !p_trl as cons (!p_crr as R, !p_trll, _, !p_trlr), _, !p_trr) => let
//
      val tr = !p_tr
      val () = !p_tr := !p_trll
      val () = fold@ (t)
      val () = !p_trll := t
//
      val trl = !p_trl
      val () = !p_trl := !p_trlr
      val () = !p_cr := B
      val () = fold@ (tr)
      val () = !p_trlr := tr
//
    in
      fold@ (trl); trl
    end // end of [cons (R, cons (R, ...), ...)]
  | _ =>> (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
) :<cloref1> [cl:clr; v:nat | v <= c] rbtree (a, cl, bh, v) =
  case+ t of
  | cons (
      !p_c, !p_tl, !p_x, !p_tr
    ) => let
      val sgn = compare<a> (x0, !p_x, cmp)
    in
      if sgn < 0 then let
        val [cl,v:int] tl = ins (!p_tl, x0)
        val () = !p_tl := tl
      in
        if !p_c = B then
          insfix_l (view@(!p_c), view@(!p_tl), view@(!p_x), view@(!p_tr) | t, p_tl)
        else let
          val () = !p_c := R in fold@ {a}{..}{..}{cl} (t); t
        end // end of [if]
      end else if sgn > 0 then let
        val [cr,v:int] tr = ins (!p_tr, x0)
        val () = !p_tr := tr
      in
        if !p_c = B then
          insfix_r (view@(!p_c), view@(!p_tl), view@(!p_x), view@(!p_tr) | t, p_tr)
        else let
          val () = !p_c := R in fold@ {a}{..}{..}{cr} (t); t
        end // end of [if]
      end else (fold@ {a}{..}{..}{0} (t); t) // end of [if]
    end // end of [cons]
  | ~nil () => cons {..}{..}{..}{0} (R, nil, x0, nil)
// end of [ins]
val t = ins (t, x0)
//
in
//
case+ t of cons (!p_c as R, _, _, _) => (!p_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 received 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 to delete an element from a given linear red-black tree.

<<< PreviousHomeNext >>>
Linear Binary Search TreesUpAbstract Views and Viewtypes