Top

This file has been processed with:

ocamlorn --library stdlib.mli \ --library redblack.in.ml --input redblack.in.ml --lifting redblack.lif.ml \ > redblack.out.ml

Red-black trees

We show that red-black trees can be disornamented to simple trees without balancing information. On this occasion, we show that holes can appear during disornamentation, and how one can provides patches for them.

The red-black trees datatype is defined as follows:

type redblack = | Black of redblack * elt * redblack | Red of redblack * elt * redblack | Empty

with several functions to manipulate them:

let rec mem x = function | Empty -> False | (Red(l, y, r) | Black(l, y, r)) -> match compare x y with | Lt -> mem x l | Gt -> mem x r | Eq -> True let singleton x = Black(Empty, x, Empty) let balance_left l x r = match (l, x, r) with | ((Red(Red(a, x, b), y, c), z, d) | (Red(a, x, Red(b, y, c)), z, d)) -> Red(Black(a, x, b), y, Black(c, z, d)) | (l, x, r) -> Black(l, x, r) let balance_right l x r = match (l, x, r) with | ((a, x, Red(Red(b, y, c), z, d)) | (a, x, Red(b, y, Red(c, z, d)))) -> Red(Black(a, x, b), y, Black(c, z, d)) | (l, x, r) -> Black(l, x, r) let add x s = let rec add_aux t = match t with | Empty -> Red(Empty, x, Empty) | Red(l, y, r) -> begin match compare x y with | Lt -> Red(add_aux l, y, r) | Gt -> Red(l, y, add_aux r) | Eq -> t end | Black(l, y, r) -> begin match compare x y with | Lt -> balance_left (add_aux l) y r | Gt -> balance_right l y (add_aux r) | Eq -> t end in match add_aux s with | Red(a, b, c) -> Black(a, b, c) | a -> a

Now, we define a new datatype: the simplest tree type, without balancing information:

type tree = | SEmpty | SNode of tree * elt * tree

We write a relation between this datatype and the red-black trees:

type relation simplification: redblack => tree with | Empty => SEmpty | (Red(a, e, b) | Black(a, e, b)) => SNode(a, e, b) when a b: simplification

This is a disornament. We can use it to disornament the previous functions:

let simpl_mem = lifting mem: elt -> simplification -> bool let simpl_singleton = lifting singleton: elt -> simplification let simpl_add = lifting add: elt -> simplification -> simplification
let rec simpl_mem x = function | SEmpty -> False | SNode(l, y, r) -> begin match compare x y with | Lt -> simpl_mem x l | Gt -> simpl_mem x r | Eq -> True end let simpl_singleton x = SNode(SEmpty, x, SEmpty) let simpl_add x s = let a = (let rec add_aux t = match t with | SEmpty -> SNode(SEmpty, x, SEmpty) | SNode(l, y, r) -> begin match #40 with | Left _ -> begin match compare x y with | Lt -> SNode(add_aux l, y, r) | Gt -> SNode(l, y, add_aux r) | Eq -> t end | Right _ -> begin match compare x y with | Lt -> (lifting #36 of balance_left) (add_aux l) y r | Gt -> (lifting #28 of balance_right) l y (add_aux r) | Eq -> t end end in add_aux) s in match a with | SEmpty -> a | SNode(a1, e, b) -> begin match #8 with | Left _ -> SNode(a1, e, b) | Right _ -> a end

The mem and singleton functions are disornamented without needing user interaction. Intuitively, we understand that these functions do not deal with the balancing information, so it is not surprising that their counterpart for the simple tree type can be computed automatically.

However, for the add function, we notice that there are several holes. They are identified with a number, such as #38 or #8. Each of these two holes are pattern matched towards two branches: this comes from the fact that there were different code for Red and Black constructors. In addition, there are also missing liftings, for instance identified by (lifting #34 of balance_left), as we did not perform the lifting of these functions before lifting add (however, in this case, we are going to see that those liftings are not needed).

They are two ways to select a hole and specify how it must be patched (see the localized expressions example for details). One can directly use its numbered identifier and specify its content, for instance, we could add with #38 <- Left () to select the first branch. However, if the original code is changed afterwards, this number may change as well, and hole may also appear for a similar case. We may solve both problems by using expression patterns (instead of identifiers) to select the holes to which a patch should apply.

In our case, we just write:

let simpl_add = lifting add: elt -> simplification -> simplification with | (match #a with Left _ -> _a) => #a <- Left ()

and get the following code:

let simpl_add x s = let a = (let rec add_aux t = match t with | SEmpty -> SNode(SEmpty, x, SEmpty) | SNode(l, y, r) -> begin match compare x y with | Lt -> SNode(add_aux l, y, r) | Gt -> SNode(l, y, add_aux r) | Eq -> t end in add_aux) s in match a with | SEmpty -> a | SNode(a, e, b) -> SNode(a, e, b)

The code was simplified after replacing the holes by the patches. Therefore, the two Right branches were removed (in particular, the additional lifting requests disappeared).

Note that in this example, the last three line could be further simplified into the variable a but there is no η-reduction implemented at this moment.