red-black-non-constructed.cd 1.17 KB
Newer Older
Giuseppe Castagna's avatar
Giuseppe Castagna committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36

type RBtree = Btree | Rtree

(* Black rooted RB tree: *)
type Btree = [] | <black elem='a>[ RBtree RBtree ]

(* Red rooted RB tree: *)
type Rtree = <red elem='a>[ Btree Btree ]

type Wrongtree =    <red elem='a>( [ Rtree Btree ]
                                   | [ Btree Rtree ])

type Unbalanced = <black elem='a>( [ Wrongtree RBtree ]
                                   | [ RBtree Wrongtree ])

let balance ( Unbalanced -> Rtree ; 'b\Unbalanced -> 'b\Unbalanced )
  | <black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
  | <black (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ]
  | <black (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ]
  | <black (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ] ->
        <red (y)>[ <black (x)>[ a b ] <black (z)>[ c d ] ]
  | x -> x


let insert (x : 'a) (t : Btree) : Btree =
  let ins_aux ( [] -> Rtree;
                Btree\[] -> RBtree\[];
                Rtree -> Rtree|Wrongtree )
    | [] -> <red elem=x>[ [] [] ]
    | (<(color) elem=y>[ a b ]) & z ->
           if x << y then balance <(color) elem=y>[ (ins_aux a) b ]
	   else if x >> y then balance <(color) elem=y>[ a (ins_aux b) ]
	   else z
    in match ins_aux t with
       | <_ (y)>[ a b ] -> <black (y)>[ a b ]