(*
* This example shows that the insert operation maps a balanced
* redblack tree into a balanced redblack tree. Also it increases
* the size of the tree by at most one (note: the inserted key may
* have already existed in the tree).
*)
(* 8 type annotations, which occupy about 20 lines *)
structure RedBlackTree =
struct
type key = int
type answer = key option
datatype order = LESS | EQUAL | GREATER
type 'a entry = int * 'a
datatype 'a dict =
Empty (* considered black *)
| Black of 'a entry * 'a dict * 'a dict
| Red of 'a entry * 'a dict * 'a dict
typeref 'a dict of nat * nat * nat * nat
(* The meaning of the four indices is: (color, black height, red height, size).
* A balenced tree is one such that
* (1) for every node in it, both of its sons are of the same black height.
* (2) the red height of the tree is 0, which means that there exist
* no consecutive red nodes.
*)
with Empty <| 'a dict(0, 0, 0, 0)
| Black <| {cl:nat, cr:nat, bh:nat, sl:nat, sr:nat}
'a entry * 'a dict(cl, bh, 0, sl) * 'a dict(cr, bh, 0, sr)
-> 'a dict(0, bh+1, 0, sl+sr+1)
| Red <| {cl:nat, cr:nat, bh:nat, rhl:nat, rhr:nat, sl:nat, sr:nat}
'a entry * 'a dict(cl, bh, rhl, sl) * 'a dict(cr, bh, rhr, sr)
-> 'a dict(1, bh, cl+cr+rhl+rhr, sl+sr+1)
(* note if the root of a tree is black, then the tree is a balenced red/black tree *)
fun compare (s1:int,s2:int) =
if s1 > s2 then GREATER else if s1 < s2 then LESS else EQUAL
where compare <| int * int -> order
fun('a)
lookup dict key =
let
fun lk (Empty) = NONE
| lk (Red tree) = lk' tree
| lk (Black tree) = lk' tree
where lk <| 'a dict -> answer
and lk' ((key1, datum1), left, right) =
(case compare(key,key1)
of EQUAL => SOME(key1)
| LESS => lk left
| GREATER => lk right)
where lk' <| 'a entry * 'a dict * 'a dict -> answer
in
lk dict
end
where loopup <| 'a dict -> key -> answer
fun('a)
restore_right(e, Red lt, Red (rt as (_,Red _,_))) =
Red(e, Black lt, Black rt) (* re-color *)
| restore_right(e, Red lt, Red (rt as (_,_,Red _))) =
Red(e, Black lt, Black rt) (* re-color *)
| restore_right(e, l as Empty, Red(re, Red(rle, rll, rlr), rr)) =
(* l is black, deep rotate *)
Black(rle, Red(e, l, rll), Red(re, rlr, rr))
| restore_right(e, l as Black _, Red(re, Red(rle, rll, rlr), rr)) =
(* l is black, deep rotate *)
Black(rle, Red(e, l, rll), Red(re, rlr, rr))
| restore_right(e, l as Empty, Red(re, rl, rr as Red _)) =
(* l is black, shallow rotate *)
Black(re, Red(e, l, rl), rr)
| restore_right(e, l as Black _, Red(re, rl, rr as Red _)) =
(* l is black, shallow rotate *)
Black(re, Red(e, l, rl), rr)
| restore_right(e, l, r as Red(_, Empty, Empty))
= Black(e, l, r) (* r must be a red/black tree *)
| restore_right(e, l, r as Red(_, Black _, Black _))
= Black(e, l, r) (* r must be a red/black tree *)
| restore_right(e, l, r as Black _) =
Black(e, l, r) (* r must be a red/black tree *)
where restore_right <|
{cl:nat, cr:nat, bh:nat, rhr:nat, sl:nat, sr:nat | rhr <= 1}
'a entry * 'a dict(cl, bh, 0, sl) * 'a dict(cr, bh, rhr, sr)
-> [c:nat | c <= 1 ] 'a dict(c, bh+1, 0, sl + sr + 1)
fun('a)
restore_left(e, Red (lt as (_,Red _,_)), Red rt) =
Red(e, Black lt, Black rt) (* re-color *)
| restore_left(e, Red (lt as (_,_,Red _)), Red rt) =
Red(e, Black lt, Black rt) (* re-color *)
| restore_left(e, Red(le, ll as Red _, lr), r as Empty) =
(* r is black, shallow rotate *)
Black(le, ll, Red(e, lr, r))
| restore_left(e, Red(le, ll as Red _, lr), r as Black _) =
(* r is black, shallow rotate *)
Black(le, ll, Red(e, lr, r))
| restore_left(e, Red(le, ll, Red(lre, lrl, lrr)), r as Empty) =
(* r is black, deep rotate *)
Black(lre, Red(le, ll, lrl), Red(e, lrr, r))
| restore_left(e, Red(le, ll, Red(lre, lrl, lrr)), r as Black _) =
(* r is black, deep rotate *)
Black(lre, Red(le, ll, lrl), Red(e, lrr, r))
| restore_left(e, l as Red(_, Empty, Empty), r)
= Black(e, l, r) (* l must be a red/black tree *)
| restore_left(e, l as Red(_, Black _, Black _), r)
= Black(e, l, r) (* l must be a red/black tree *)
| restore_left(e, l as Black _, r) =
Black(e, l, r) (* l must be a red/black tree *)
where restore_left <|
{cl:nat, cr:nat, bh:nat, rhl:nat, sl:nat, sr:nat | rhl <= 1}
'a entry * 'a dict(cl, bh, rhl, sl) * 'a dict(cr, bh, 0, sr)
-> [c:nat | c <= 1 ] 'a dict(c, bh+1, 0, sl + sr + 1)
fun('a)
insert (dict, entry as (key,datum)) =
let
(* val ins : 'a dict -> 'a dict inserts entry *)
(* ins (Red _) may violate color invariant at root, having red height 1 *)
(* ins (Black _) or ins (Empty) will be red/black tree *)
(* ins preserves black height *)
fun ins (Empty) = Red(entry, Empty, Empty)
| ins (Red(entry1 as (key1, datum1), left, right)) =
(case compare(key,key1) of
EQUAL => Red(entry, left, right)
| LESS => Red(entry1, ins left, right)
| GREATER => Red(entry1, left, ins right))
| ins(Black(entry1 as (key1, datum1), left, right)) =
(case compare(key,key1) of
EQUAL => Black(entry, left, right)
| LESS => restore_left(entry1, ins left, right)
| GREATER => restore_right(entry1, left, ins right))
where ins <|
{c:nat, bh:nat, s:nat}
'a dict(c, bh, 0, s) ->
[nc:nat, nrh:nat, ns:nat |
((c = 0 /\ nrh = 0 /\ nc <= 1) \/ (c = 1 /\ nrh <= 1 /\ nc = 1))
/\ (ns = s \/ ns = s + 1) ] 'a dict(nc, bh, nrh, ns)
(* ins guarantees
(1) if the root of old tree is black, then the new tree is a red/black tree
(2) if the root of old tree is red, then the root of new tree is also red,
but the red height is at most one.
(3) the size of new tree is either increased by one or stays the same
*)
in
let
val dict = ins dict
in
case dict of
Red (t as (_, Red _, _)) => Black t (* re-color *)
| Red (t as (_, _, Red _)) => Black t (* re-color *)
| Red (t as (_, Black _, Black _)) => dict
| Red (t as (_, Empty, Empty)) => dict
| Black _ => dict
end
end
where insert <|
{c:nat, bh:nat, s:nat}
'a dict(c, bh, 0, s) * 'a entry ->
[nc:nat, nbh:nat, ns:nat | (nbh = bh \/ nbh = bh + 1) /\ (ns = s \/ ns = s + 1) ]
'a dict(nc, nbh, 0, ns)
end