red-black.cd 2.38 KB
Newer Older
beppe's avatar
beppe committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

type RBtree('a) = Btree('a) | Rtree('a)

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

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

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

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

16
(* does not type *)
beppe's avatar
beppe committed
17
18
19
20
21
22
23
let balance ( Unbalanced('a) -> Rtree('a) ; 'b\Unbalanced('a) -> 'b\Unbalanced('a) )
  | <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
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
;;

let balance ( Unbalanced('a) -> Rtree('a) ; 'b & RBtree('a) -> 'b & RBtree('a) )
  | <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 balance ( Unbalanced('a) -> Rtree('a) ; 'b\Unbalanced(Any) -> 'b\Unbalanced(Any) )
  | (<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 ] ] ]) & Unbalanced(Any) ->
        <red (y)>[ <black (x)>[ a b ] <black (z)>[ c d ] ]
  | x -> x
;;

type  UTree = <black (Any)>[ <red (Any)>[ <red (Any)>[ Any Any ] Any ] Any ] 
             | <black (Any)>[ <red (Any)>[ Any <red (Any)>[ Any Any ] ] Any ] 
             | <black (Any)>[ Any <red (Any)>[ <red (Any)>[ Any Any ] Any ] ] 
             | <black (Any)>[ Any <red (Any)>[ Any <red (Any)>[ Any Any ] ] ]
;;

beppe's avatar
beppe committed
50
51
52
53
54
55
56
57
58
59
60
61

let insert (x : 'a) (t : Btree('a)) : Btree('a) =
  let ins_aux ( [] -> Rtree('a);
                Btree('a)\[] -> RBtree('a)\[];
                Rtree('a) -> Rtree('a)|Wrongtree('a) )
    | [] -> <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 ]
62