red-black.cd 7.67 KB
Newer Older
1 2 3 4 5 6 7 8 9 10

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) ]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
11
                                     | [ Btree('a) Rtree('a) ])
12 13

type Unbalanced('a) = <black elem='a>( [ Wrongtree('a) RBtree('a) ]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
14
                                     | [ RBtree('a) Wrongtree('a) ])
15
;;
16

17 18 19 20
(***************
	 ill typed, see rb-fail.cd


21 22 23 24 25 26 27
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
28
;;
29 30
************)

Giuseppe Castagna's avatar
Giuseppe Castagna committed
31 32 33
(*                                                                               *)
(* Version 1: restrict the domain of balance to trees (ie, RBtree | Unbalanced)  *)
(*                                                                               *)
34 35 36 37 38 39 40 41 42 43

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
;;

44

Giuseppe Castagna's avatar
Giuseppe Castagna committed
45 46 47 48 49 50
(*                                                                               *)
(* Version 2: restrict the first branch to Unbalanced trees whatever             *)
(*            type it contains                                                   *)
(*                                                                               *)


51 52 53 54 55 56 57 58 59
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
;;

Giuseppe Castagna's avatar
Giuseppe Castagna committed
60 61 62 63 64 65 66

(*                                                                               *)
(* Version 3: Use the accepted type of the first branch (i.e. UTree)             *)
(*            to specify the behavious when the second branch is taken           *)
(*                                                                               *)


67 68 69 70 71 72
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 ] ] ]
;;

73 74 75 76 77 78 79 80 81
let balance ( Unbalanced('a) -> Rtree('a) ; 'b\UTree -> 'b\UTree )
  | <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
;;

82 83


84

85 86
(* Here we start the definition of         *)
(* standard operations for red-black trees *)
87

88
let insert (x : 'a) (t : Btree('a)) : Btree('a)\[]=
89 90 91 92 93 94 95 96 97 98
  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 ]
99
 
100

Giuseppe Castagna's avatar
Giuseppe Castagna committed
101 102 103
let is_empty (RBtree('a) -> Bool)  (*better type (Any\[] -> `false ; [] ->`true ) *)
  | [] -> `true
  | _ -> `false
104 105 106


let member (x : 'a) (t : RBtree('a)) : Bool =
Giuseppe Castagna's avatar
Giuseppe Castagna committed
107
(* better type: 'a -> ([] -> `false) & (RBtree('a) -> Bool) *) 
108 109 110 111 112 113 114 115 116
  match t with
   | [] -> `false
   | <_ elem=y>[ left right ] ->
       (y = x) || ( member x (if x<<y then left else right) ) 


let singleton (x : 'a): Btree('a)  = <black elem=x>[ [] [] ]


Giuseppe Castagna's avatar
Giuseppe Castagna committed
117
let cardinal ( RBtree('a) -> Int )   (* better type: [] -> 0, Any\[] -> [1--*] *)
118
  | [] -> 0
Giuseppe Castagna's avatar
Giuseppe Castagna committed
119 120 121 122 123 124
  | <_ ..>[ l r ] -> cardinal l + cardinal r + 1

(* The though case: deletion *)


   (* remove the rightmost leave of the tree and return a flag to state
125 126
      whether the resulting tree decreased the the depth of black nodes *)
      
Giuseppe Castagna's avatar
Giuseppe Castagna committed
127 128 129 130 131 132 133 134 135
   let remove_min (RBtree('a)\[] -> [RBtree('a) Bool 'a])
       (* black leaf: remove it and flag the depth decrease *)
     | <black elem=x>[ [] [] ] ->                 
          [ [] `true x ]
       (* black node with red child: promote the child to black *)
     | <black elem=x>[ ([] <red elem=y>[ l r ])
                     | (<red elem=y>[ l r ] [] )] ->
          [ <black elem=y>[ l r ] `false x ]
       (* you cannot have a red node with one empty sibling *)  
136
     | <black elem=Any>[ ([] <red ..>Any)
Giuseppe Castagna's avatar
Giuseppe Castagna committed
137
                     | (<red ..>Any []) ] ->
138
          raise "impossible"
Giuseppe Castagna's avatar
Giuseppe Castagna committed
139 140 141 142
       (* red node with at least on empty child : remove it without any flag *)
     | <red elem=x>[ ([] n) | (n []) ] ->
          [ n `false x ]
       (* general case of a node with two non empty childs *)
143
     | <(c) elem=x>[ l\[] r\[] ] ->
Giuseppe Castagna's avatar
Giuseppe Castagna committed
144
         let [ ll d e ] = remove_min l in
145
	 let tree = <(c) elem=x>[ ll r ] in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
146 147 148 149
	 if d then
            (bubble_left tree)@[e]
	 else
	    [ tree `false e ]
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
     | _ -> raise "impossible"

   let blackify( (<_ ('a)>'b)  -> <black ('a)>'b )
     | <_ (x)>y -> <black (x)>y

   let redify( (<_ ('a)>'b)  -> <red ('a)>'b )
     | <_ (x)>y -> <red (x)>y



  (* increase the black depth of the right child of the argument and
     flag whether the black depth of the tree is still to be incremented  *)

   let bubble_right ( RBtree('a)\[] -> (Btree('a) , Bool) )
     | <black elem=y>[<red elem=x>[ ll\[] <black elem=re>[c d]] (e&<black ..>_) ] ->
         ( <black elem=re>[ <black elem=x>[(balance (redify ll)) c]
                            <black elem=y>[d e]
                	  ] , `true)
     | <_ ..>[ [] _ ] ->
          raise "impossible"
     | <(c) elem=e>[ l r ] ->
          (<black elem=e>[ (balance(redify l)) r ] , (c = `black))


  (* increase the right depth of the right child of the argument and
     flag whether the black depth of the tree is still to be incremented  *)  

    let bubble_left ( RBtree('a)\[] -> (Btree('a) , Bool) )
      | <black elem=z>[ (e&<black ..>_) <red elem=x>[ <black elem=w>[a b] ll\[] ] ] ->
         ( <black elem=w>[ <black elem=z>[ e a ]
                           <black elem=x>[ b (balance (redify ll)) ]
                	 ] , `true )
      | <_ ..>[ _ [] ] -> 
          raise "impossible"
      | <(c) elem=e>[ l r ] ->
          (<black elem=e>[ l (balance (redify r)) ], (c = `black))
  

let remove(x : 'a)(t : RBtree('a) ) : RBtree('a) =
  let remove_aux(RBtree('a) -> (RBtree('a),Bool) )
    | [] ->
         ([],`false)
    | <(c) elem=y>[ l r ] & tree ->
        if (x << y ) then
	  let (ll,d) = remove_aux l in
	  let tree = <(c) elem=y>[ ll r ] in   (* we must prove that tree is well-formed *)
	  if d then bubble_left tree else (tree,`false)
	else if (x >> y) then
	  let (rr,d) = remove_aux r in
	  let tree = <(c) elem=y>[ l rr ] in
	  if d then bubble_right tree else (tree,`false)
	else (* x = y *)
	   match tree with
	     | <(c) ..>[ [] [] ] -> ([], (c = `black))
	     | <black ..>[ ([] y) | (y []) ] -> (blackify y,`false)
	     | <(c) ..>[ l r ] ->
	          let [ ll d z ] = remove_min l in
		  let tree = <(c) elem=z>[ ll r] in
		  if d then bubble_left tree else (tree, `false)
   in
   let (sol,_) = remove_aux t in sol