Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Diff of /smlnj-lib/branches/rt-transition/Util/int-redblack-set.sml
ViewVC logotype

Diff of /smlnj-lib/branches/rt-transition/Util/int-redblack-set.sml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 4069, Tue Jun 9 20:52:48 2015 UTC revision 4070, Thu Jun 11 12:33:25 2015 UTC
# Line 1  Line 1 
1  (* int-redblack-set.sml  (* int-redblack-set.sml
2   *   *
3     * COPYRIGHT (c) 2014 The Fellowship of SML/NJ (http://www.smlnj.org)
4     * All rights reserved.
5     *
6   * COPYRIGHT (c) 1999 Bell Labs, Lucent Technologies.   * COPYRIGHT (c) 1999 Bell Labs, Lucent Technologies.
7   *   *
8   * This code is based on Chris Okasaki's implementation of   * This code is based on Chris Okasaki's implementation of
# Line 10  Line 13 
13   *   *
14   * A red-black tree should satisfy the following two invariants:   * A red-black tree should satisfy the following two invariants:
15   *   *
16   *   Red Invariant: each red node has a black parent.   *   Red Invariant: each red node has black children (empty nodes are
17     *      considered black).
18   *   *
19   *   Black Condition: each path from the root to an empty node has the   *   Black Invariant: each path from the root to an empty node has the
20   *     same number of black nodes (the tree's black height).   *     same number of black nodes (the tree's black height).
21   *   *
22   * The Red condition implies that the root is always black and the Black   * The Black invariant implies that any node with only one child
23   * condition implies that any node with only one child will be black and   * will be black and its child will be a red leaf.
  * its child will be a red leaf.  
24   *)   *)
25    
26  structure IntRedBlackSet :> ORD_SET where type Key.ord_key = int =  structure IntRedBlackSet :> ORD_SET where type Key.ord_key = int =
# Line 29  Line 32 
32          val compare = Int.compare          val compare = Int.compare
33        end        end
34    
35      type item = int      type item = Key.ord_key
36    
37      datatype color = R | B      datatype color = R | B
38    
# Line 44  Line 47 
47    
48      val empty = SET(0, E)      val empty = SET(0, E)
49    
50      fun singleton x = SET(1, T(R, E, x, E))      fun singleton x = SET(1, T(B, E, x, E))
51    
52      fun add (SET(nItems, m), x) = let      fun add (SET(nItems, m), x) = let
53            val nItems' = ref nItems            val nItems' = ref nItems
# Line 55  Line 58 
58                       of T(R, c, z, d) =>                       of T(R, c, z, d) =>
59                            if (x < z)                            if (x < z)
60                              then (case ins c                              then (case ins c
61                                 of T(R, e, w, f) =>                                 of T(R, e, w, f) => T(R, T(B,e,w,f), z, T(B,d,y,b))
                                     T(R, T(B,e,w,f), z, T(B,d,y,b))  
62                                  | c => T(B, T(R,c,z,d), y, b)                                  | c => T(B, T(R,c,z,d), y, b)
63                                (* end case *))                                (* end case *))
64                            else if (x = z)                            else if (x = z)
65                              then T(color, T(R, c, x, d), y, b)                              then T(color, T(R, c, x, d), y, b)
66                              else (case ins d                              else (case ins d
67                                 of T(R, e, w, f) =>                                 of T(R, e, w, f) => T(R, T(B,c,z,e), w, T(B,f,y,b))
                                     T(R, T(B,c,z,e), w, T(B,f,y,b))  
68                                  | d => T(B, T(R,c,z,d), y, b)                                  | d => T(B, T(R,c,z,d), y, b)
69                                (* end case *))                                (* end case *))
70                        | _ => T(B, ins a, y, b)                        | _ => T(B, ins a, y, b)
# Line 74  Line 75 
75                       of T(R, c, z, d) =>                       of T(R, c, z, d) =>
76                            if (x < z)                            if (x < z)
77                              then (case ins c                              then (case ins c
78                                 of T(R, e, w, f) =>                                 of T(R, e, w, f) => T(R, T(B,a,y,e), w, T(B,f,z,d))
                                     T(R, T(B,a,y,e), w, T(B,f,z,d))  
79                                  | c => T(B, a, y, T(R,c,z,d))                                  | c => T(B, a, y, T(R,c,z,d))
80                                (* end case *))                                (* end case *))
81                            else if (x = z)                            else if (x = z)
82                              then T(color, a, y, T(R, c, x, d))                              then T(color, a, y, T(R, c, x, d))
83                              else (case ins d                              else (case ins d
84                                 of T(R, e, w, f) =>                                 of T(R, e, w, f) => T(R, T(B,a,y,c), z, T(B,e,w,f))
                                     T(R, T(B,a,y,c), z, T(B,e,w,f))  
85                                  | d => T(B, a, y, T(R,c,z,d))                                  | d => T(B, a, y, T(R,c,z,d))
86                                (* end case *))                                (* end case *))
87                        | _ => T(B, a, y, ins b)                        | _ => T(B, a, y, ins b)
88                      (* end case *))                      (* end case *))
89            val m = ins m            val T(_, a, y, b) = ins m
90            in            in
91              SET(!nItems', m)              SET(!nItems', T(B, a, y, b))
92            end            end
93      fun add' (x, m) = add (m, x)      fun add' (x, m) = add (m, x)
94    
# Line 100  Line 99 
99      local      local
100        datatype zipper        datatype zipper
101          = TOP          = TOP
102          | LEFT of (color * int * tree * zipper)          | LEFT of (color * item * tree * zipper)
103          | RIGHT of (color * tree * int * zipper)          | RIGHT of (color * tree * item * zipper)
104      in      in
105      fun delete (SET(nItems, t), k) = let      fun delete (SET(nItems, t), k) = let
106            (* zip the zipper *)
107            fun zip (TOP, t) = t            fun zip (TOP, t) = t
108              | zip (LEFT(color, x, b, z), a) = zip(z, T(color, a, x, b))              | zip (LEFT(color, x, b, p), a) = zip(p, T(color, a, x, b))
109              | zip (RIGHT(color, a, x, z), b) = zip(z, T(color, a, x, b))              | zip (RIGHT(color, a, x, p), b) = zip(p, T(color, a, x, b))
110          (* bbZip propagates a black deficit up the tree until either the top          (* zip the zipper while resolving a black deficit *)
111           * is reached, or the deficit can be covered.  It returns a boolean            fun fixupZip (TOP, t) = (true, t)
112           * that is true if there is still a deficit and the zipped tree.            (* case 1 from CLR *)
113                | fixupZip (LEFT(B, x, T(R, a, y, b), p), t) = (case a
114                     of T(_, T(R, a11, w, a12), z, a2) => (* case 1L ==> case 3L ==> case 4L *)
115                          (false, zip (p, T(B, T(R, T(B, t, x, a11), w, T(B, a12, z, a2)), y, b)))
116                      | T(_, a1, z, T(R, a21, w, t22)) => (* case 1L ==> case 4L *)
117                          (false, zip (p, T(B, T(R, T(B, t, x, a1), z, T(B, a21, w, t22)), y, b)))
118                      | T(_, a1, z, a2) => (* case 1L ==> case 2L; rotate + recolor fixes deficit *)
119                          (false, zip (p, T(B, T(B, t, x, T(R, a1, z, a2)), y, b)))
120                      | _ => fixupZip (LEFT(R, x, a, LEFT(B, y, b, p)), t)
121                    (* end case *))
122                | fixupZip (RIGHT(B, T(R, a, x, b), y, p), t) = (case b
123                     of T(_, b1, z, T(R, b21, w, b22)) => (* case 1R ==> case 3R ==> case 4R *)
124                          (false, zip (p, T(B, a, x, T(R, T(B, b1, z, b21), w, T(B, b22, y, t)))))
125                      | T(_, T(R, b11, w, b12), z, b2) => (* case 1R ==> case 4R *)
126                          (false, zip (p, T(B, a, x, T(R, T(B, b11, w, b12), z, T(B, b2, y, t)))))
127                      | T(_, b1, z, b2) => (* case 1L ==> case 2L; rotate + recolor fixes deficit *)
128                          (false, zip (p, T(B, a, x, T(B, T(R, b1, z, b2), y, t))))
129                      | _ => fixupZip (RIGHT(R, b, y, RIGHT(B, a, x, p)), t)
130                    (* end case *))
131              (* case 3 from CLR *)
132                | fixupZip (LEFT(color, x, T(B, T(R, a1, y, a2), z, b), p), t) =
133                  (* case 3L ==> case 4L *)
134                    (false, zip (p, T(color, T(B, t, x, a1), y, T(B, a2, z, b))))
135                | fixupZip (RIGHT(color, T(B, a, x, T(R, b1, y, b2)), z, p), t) =
136                  (* case 3R ==> case 4R; rotate, recolor, plus rotate fixes deficit *)
137                    (false, zip (p, T(color, T(B, a, x, b1), y, T(B, b2, z, t))))
138              (* case 4 from CLR *)
139                | fixupZip (LEFT(color, x, T(B, a, y, T(R, b1, z, b2)), p), t) =
140                    (false, zip (p, T(color, T(B, t, x, a), y, T(B, b1, z, b2))))
141                | fixupZip (RIGHT(color, T(B, T(R, a1, z, a2), x, b), y, p), t) =
142                    (false, zip (p, T(color, T(B, a1, z, a2), x, T(B, b, y, t))))
143              (* case 2 from CLR; note that "a" and "b" are guaranteed to be black, since we did
144               * not match cases 3 or 4.
145               *)
146                | fixupZip (LEFT(R, x, T(B, a, y, b), p), t) =
147                    (false, zip (p, T(B, t, x, T(R, a, y, b))))
148                | fixupZip (LEFT(B, x, T(B, a, y, b), p), t) =
149                    fixupZip (p, T(B, t, x, T(R, a, y, b)))
150                | fixupZip (RIGHT(R, T(B, a, x, b), y, p), t) =
151                    (false, zip (p, T(B, T(R, a, x, b), y, t)))
152                | fixupZip (RIGHT(B, T(B, a, x, b), y, p), t) =
153                    fixupZip (p, T(B, T(R, a, x, b), y, t))
154              (* push deficit up the tree by recoloring a black node as red *)
155                | fixupZip (LEFT(_, y, E, p), t) = fixupZip (p, T(R, t, y, E))
156                | fixupZip (RIGHT(_, E, y, p), t) = fixupZip (p, T(R, E, y, t))
157              (* impossible cases that violate the red invariant *)
158                | fixupZip _ = raise Fail "Red invariant violation"
159            (* delete the minimum value from a non-empty tree, returning a triple
160             * (elem, bd, tr), where elem is the minimum element, tr is the residual
161             * tree with elem removed, and bd is true if tr has a black-depth that is
162             * less than the original tree.
163           *)           *)
164            fun bbZip (TOP, t) = (true, t)            fun delMin (T(R, E, y, b), p) =
165              | bbZip (LEFT(B, x, T(R, c, y, d), z), a) = (* case 1L *)                (* replace the node by its right subtree (which must be E) *)
166                  bbZip (LEFT(R, x, c, LEFT(B, y, d, z)), a)                  (y, false, zip(p, b))
167              | bbZip (LEFT(color, x, T(B, T(R, c, y, d), w, e), z), a) = (* case 3L *)              | delMin (T(B, E, y, T(R, a', y', b')), p) =
168                  bbZip (LEFT(color, x, T(B, c, y, T(R, d, w, e)), z), a)                (* replace the node with its right child, while recoloring the child black to
169              | bbZip (LEFT(color, x, T(B, c, y, T(R, d, w, e)), z), a) = (* case 4L *)                 * preserve the black invariant.
170                  (false, zip (z, T(color, T(B, a, x, c), y, T(B, d, w, e))))                 *)
171              | bbZip (LEFT(R, x, T(B, c, y, d), z), a) = (* case 2L *)                  (y, false, zip (p, T(B, a', y', b')))
172                  (false, zip (z, T(B, a, x, T(R, c, y, d))))              | delMin (T(B, E, y, E), p) = let
173              | bbZip (LEFT(B, x, T(B, c, y, d), z), a) = (* case 2L *)                (* delete the node, which reduces the black-depth by one, so we attempt to fix
174                  bbZip (z, T(B, a, x, T(R, c, y, d)))                 * the deficit on the path back.
175              | bbZip (RIGHT(color, T(R, c, y, d), x, z), b) = (* case 1R *)                 *)
176                  bbZip (RIGHT(R, d, x, RIGHT(B, c, y, z)), b)                  val (blkDeficit, t) = fixupZip (p, E)
177              | bbZip (RIGHT(color, T(B, T(R, c, w, d), y, e), x, z), b) = (* case 3R *)                  in
178                  bbZip (RIGHT(color, T(B, c, w, T(R, d, y, e)), x, z), b)                    (y, blkDeficit, t)
179              | bbZip (RIGHT(color, T(B, c, y, T(R, d, w, e)), x, z), b) = (* case 4R *)                  end
                 (false, zip (z, T(color, c, y, T(B, T(R, d, w, e), x, b))))  
             | bbZip (RIGHT(R, T(B, c, y, d), x, z), b) = (* case 2R *)  
                 (false, zip (z, T(B, T(R, c, y, d), x, b)))  
             | bbZip (RIGHT(B, T(B, c, y, d), x, z), b) = (* case 2R *)  
                 bbZip (z, T(B, T(R, c, y, d), x, b))  
             | bbZip (z, t) = (false, zip(z, t))  
           fun delMin (T(R, E, y, b), z) = (y, (false, zip(z, b)))  
             | delMin (T(B, E, y, b), z) = (y, bbZip(z, b))  
180              | delMin (T(color, a, y, b), z) = delMin(a, LEFT(color, y, b, z))              | delMin (T(color, a, y, b), z) = delMin(a, LEFT(color, y, b, z))
181              | delMin (E, _) = raise Match              | delMin (E, _) = raise Match
           fun join (R, E, E, z) = zip(z, E)  
             | join (_, a, E, z) = #2(bbZip(z, a))       (* color = black *)  
             | join (_, E, b, z) = #2(bbZip(z, b))       (* color = black *)  
             | join (color, a, b, z) = let  
                 val (x, (needB, b')) = delMin(b, TOP)  
                 in  
                   if needB  
                     then #2(bbZip(z, T(color, a, x, b')))  
                     else zip(z, T(color, a, x, b'))  
                 end  
182            fun del (E, z) = raise LibBase.NotFound            fun del (E, z) = raise LibBase.NotFound
183              | del (T(color, a, y, b), z) =              | del (T(color, a, y, b), p) =
184                  if (k < y)                  if (k < y)
185                    then del (a, LEFT(color, y, b, z))                    then del (a, LEFT(color, y, b, p))
186                  else if (k = y)                  else if (k = y)
187                    then join (color, a, b, z)                    then (case (color, a, b)
188                    else del (b, RIGHT(color, a, y, z))                       of (R, E, E) => zip(p, E)
189                          | (B, E, E) => #2 (fixupZip (p, E))
190                          | (_, T(_, a', y', b'), E) =>
191                            (* node is black and left child is red; we replace the node with its
192                             * left child recolored to black.
193                             *)
194                              zip(p, T(B, a', y', b'))
195                          | (_, E, T(_, a', y', b')) =>
196                            (* node is black and right child is red; we replace the node with its
197                             * right child recolored to black.
198                             *)
199                              zip(p, T(B, a', y', b'))
200                          | _ => let
201                              val (minSucc, blkDeficit, b) = delMin (b, TOP)
202                              in
203                                if blkDeficit
204                                  then #2 (fixupZip (RIGHT(color, a, minSucc, p), b))
205                                  else zip (p, T(color, a, minSucc, b))
206                              end
207                        (* end case *))
208                      else del (b, RIGHT(color, a, y, p))
209            in            in
210              SET(nItems-1, del(t, TOP))              case del(t, TOP)
211                 of T(R, a, x, b) => SET(nItems-1, T(B, a, x, b))
212                  | t => SET(nItems-1, t)
213                (* end case *)
214            end            end
215      end (* local *)      end (* local *)
216    
# Line 250  Line 305 
305     *)     *)
306      datatype digit      datatype digit
307        = ZERO        = ZERO
308        | ONE of (int * tree * digit)        | ONE of (item * tree * digit)
309        | TWO of (int * tree * int * tree * digit)        | TWO of (item * tree * item * tree * digit)
310    (* add an item that is guaranteed to be larger than any in l *)    (* add an item that is guaranteed to be larger than any in l *)
311      fun addItem (a, l) = let      fun addItem (a, l) = let
312            fun incr (a, t, ZERO) = ONE(a, t, ZERO)            fun incr (a, t, ZERO) = ONE(a, t, ZERO)

Legend:
Removed from v.4069  
changed lines
  Added in v.4070

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0