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/word-redblack-set.sml
ViewVC logotype

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

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

revision 3736, Fri Apr 27 13:11:51 2012 UTC revision 4070, Thu Jun 11 12:33:25 2015 UTC
# Line 1  Line 1 
1  (* word-redblack-set.sml  (* word-redblack-set.sml
2   *   *
3   * COPYRIGHT (c) 2000 Bell Labs, Lucent Technologies.   * 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.
7   *   *
8   * This code is based on Chris Okasaki's implementation of   * This code is based on Chris Okasaki's implementation of
9   * red-black trees.  The linear-time tree construction code is   * red-black trees.  The linear-time tree construction code is
# 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 WordRedBlackSet :> ORD_SET where type Key.ord_key = word =  structure WordRedBlackSet :> ORD_SET where type Key.ord_key = word =
# Line 29  Line 32 
32          val compare = Word.compare          val compare = Word.compare
33        end        end
34    
35      type item = word      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 104  Line 103 
103          | RIGHT of (color * tree * item * 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            fun bbZip (TOP, t) = (true, t)                   of T(_, T(R, a11, w, a12), z, a2) => (* case 1L ==> case 3L ==> case 4L *)
115              | bbZip (LEFT(B, x, T(R, c, y, d), z), a) = (* case 1L *)                        (false, zip (p, T(B, T(R, T(B, t, x, a11), w, T(B, a12, z, a2)), y, b)))
116                  bbZip (LEFT(R, x, c, LEFT(B, y, d, z)), a)                    | T(_, a1, z, T(R, a21, w, t22)) => (* case 1L ==> case 4L *)
117              | bbZip (LEFT(color, x, T(B, T(R, c, y, d), w, e), z), a) = (* case 3L *)                        (false, zip (p, T(B, T(R, T(B, t, x, a1), z, T(B, a21, w, t22)), y, b)))
118                  bbZip (LEFT(color, x, T(B, c, y, T(R, d, w, e)), z), a)                    | T(_, a1, z, a2) => (* case 1L ==> case 2L; rotate + recolor fixes deficit *)
119              | bbZip (LEFT(color, x, T(B, c, y, T(R, d, w, e)), z), a) = (* case 4L *)                        (false, zip (p, T(B, T(B, t, x, T(R, a1, z, a2)), y, b)))
120                  (false, zip (z, T(color, T(B, a, x, c), y, T(B, d, w, e))))                    | _ => fixupZip (LEFT(R, x, a, LEFT(B, y, b, p)), t)
121              | bbZip (LEFT(R, x, T(B, c, y, d), z), a) = (* case 2L *)                  (* end case *))
122                  (false, zip (z, T(B, a, x, T(R, c, y, d))))              | fixupZip (RIGHT(B, T(R, a, x, b), y, p), t) = (case b
123              | bbZip (LEFT(B, x, T(B, c, y, d), z), a) = (* case 2L *)                   of T(_, b1, z, T(R, b21, w, b22)) => (* case 1R ==> case 3R ==> case 4R *)
124                  bbZip (z, T(B, a, x, T(R, c, y, d)))                        (false, zip (p, T(B, a, x, T(R, T(B, b1, z, b21), w, T(B, b22, y, t)))))
125              | bbZip (RIGHT(color, T(R, c, y, d), x, z), b) = (* case 1R *)                    | T(_, T(R, b11, w, b12), z, b2) => (* case 1R ==> case 4R *)
126                  bbZip (RIGHT(R, d, x, RIGHT(B, c, y, z)), b)                        (false, zip (p, T(B, a, x, T(R, T(B, b11, w, b12), z, T(B, b2, y, t)))))
127              | bbZip (RIGHT(color, T(B, T(R, c, w, d), y, e), x, z), b) = (* case 3R *)                    | T(_, b1, z, b2) => (* case 1L ==> case 2L; rotate + recolor fixes deficit *)
128                  bbZip (RIGHT(color, T(B, c, w, T(R, d, y, e)), x, z), b)                        (false, zip (p, T(B, a, x, T(B, T(R, b1, z, b2), y, t))))
129              | bbZip (RIGHT(color, T(B, c, y, T(R, d, w, e)), x, z), b) = (* case 4R *)                    | _ => fixupZip (RIGHT(R, b, y, RIGHT(B, a, x, p)), t)
130                  (false, zip (z, T(color, c, y, T(B, T(R, d, w, e), x, b))))                  (* end case *))
131              | bbZip (RIGHT(R, T(B, c, y, d), x, z), b) = (* case 2R *)            (* case 3 from CLR *)
132                  (false, zip (z, T(B, T(R, c, y, d), x, b)))              | fixupZip (LEFT(color, x, T(B, T(R, a1, y, a2), z, b), p), t) =
133              | bbZip (RIGHT(B, T(B, c, y, d), x, z), b) = (* case 2R *)                (* case 3L ==> case 4L *)
134                  bbZip (z, T(B, T(R, c, y, d), x, b))                  (false, zip (p, T(color, T(B, t, x, a1), y, T(B, a2, z, b))))
135              | bbZip (z, t) = (false, zip(z, t))              | fixupZip (RIGHT(color, T(B, a, x, T(R, b1, y, b2)), z, p), t) =
136            fun delMin (T(R, E, y, b), z) = (y, (false, zip(z, b)))                (* case 3R ==> case 4R; rotate, recolor, plus rotate fixes deficit *)
137              | delMin (T(B, E, y, b), z) = (y, bbZip(z, b))                  (false, zip (p, T(color, T(B, a, x, b1), y, T(B, b2, z, t))))
138              | delMin (T(color, a, y, b), z) = delMin(a, LEFT(color, y, b, z))            (* case 4 from CLR *)
139              | delMin (E, _) = raise Match              | fixupZip (LEFT(color, x, T(B, a, y, T(R, b1, z, b2)), p), t) =
140            fun join (R, E, E, z) = zip(z, E)                  (false, zip (p, T(color, T(B, t, x, a), y, T(B, b1, z, b2))))
141              | join (_, a, E, z) = #2(bbZip(z, a))       (* color = black *)              | fixupZip (RIGHT(color, T(B, T(R, a1, z, a2), x, b), y, p), t) =
142              | join (_, E, b, z) = #2(bbZip(z, b))       (* color = black *)                  (false, zip (p, T(color, T(B, a1, z, a2), x, T(B, b, y, t))))
143              | join (color, a, b, z) = let            (* case 2 from CLR; note that "a" and "b" are guaranteed to be black, since we did
144                  val (x, (needB, b')) = delMin(b, TOP)             * 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 delMin (T(R, E, y, b), p) =
165                  (* replace the node by its right subtree (which must be E) *)
166                    (y, false, zip(p, b))
167                | delMin (T(B, E, y, T(R, a', y', b')), p) =
168                  (* replace the node with its right child, while recoloring the child black to
169                   * preserve the black invariant.
170                   *)
171                    (y, false, zip (p, T(B, a', y', b')))
172                | delMin (T(B, E, y, E), p) = let
173                  (* delete the node, which reduces the black-depth by one, so we attempt to fix
174                   * the deficit on the path back.
175                   *)
176                    val (blkDeficit, t) = fixupZip (p, E)
177                  in                  in
178                    if needB                    (y, blkDeficit, t)
                     then #2(bbZip(z, T(color, a, x, b')))  
                     else zip(z, T(color, a, x, b'))  
179                  end                  end
180                | delMin (T(color, a, y, b), z) = delMin(a, LEFT(color, y, b, z))
181                | delMin (E, _) = raise Match
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    

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

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