多くのプログラマは、データ観型の値を操作するコードを書くことを幾分複雑に感じると思います。 込み入ったデータ構造を扱う時、しばしば私はデータ型をはじめに使おうとすることがあります。 そのデータ構造をモデリングして、データ型を用いてそのデータ構造のいくつかの機能を実装してみるのです。 それからそのデータ型を対応するデータ観型に変換し、データ観型として動作するようにその実装を修正します。 ここでは、以前の implementation of functional red-black trees を元にした線形赤黒木の実装を次に示します。 これはデータ型からデータ観型への漸進的な翻訳を具体的に説明しています。 データ観型を直接用いてプログラミングしようとする際の難易度を大きく減少させることができるのです。
次のデータ観型 rbtree 宣言は以前のデータ型 rbtree 宣言とほぼ一致しています。 違うのはキーワード datatype の代わりに、キーワード datavtype を使っている点です:
#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)
ひと目見たところ、次の関数テンプレート insfix_l は (関数的な赤黒木の) 同じ名前の関数よりもはるかに複雑です:
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]
予想されることですが、本質的に次の関数テンプレート rbtree_insert は、関数的な赤黒木に要素を挿入する同じ名前の実装の直接的な翻訳です:
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]
私は文字通り以前の関数的な赤黒木の rbtree_insert 実装をコピーし、それから型検査を通るように適切に修正して、上記の rbtree_insert を実装しました。 このコピーして修正する作業は外見的には難しく見えますが、型検査して起きるエラーメッセージに従えばそのほとんどはかなり単純です。
この章のコード全体と追加のテストコードは オンライン から入手できます。 与えられた線形赤黒木から要素を削除する操作を実装することは、読者にとってやりがいのある練習問題でしょう。