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

Diff of /smlnj-lib/branches/rt-transition/Util/redblack-set-fn.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  (* redblack-set-fn.sml  (* redblack-set-fn.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  functor RedBlackSetFn (K : ORD_KEY) :> ORD_SET where Key = K =  functor RedBlackSetFn (K : ORD_KEY) :> ORD_SET where Key = K =
# Line 40  Line 43 
43    
44      val empty = SET(0, E)      val empty = SET(0, E)
45    
46      fun singleton x = SET(1, T(R, E, x, E))      fun singleton x = SET(1, T(B, E, x, E))
47    
48      fun add (SET(nItems, m), x) = let      fun add (SET(nItems, m), x) = let
49            val nItems' = ref nItems            val nItems' = ref nItems
# Line 49  Line 52 
52                   of LESS => (case a                   of LESS => (case a
53                         of T(R, c, z, d) => (case K.compare(x, z)                         of T(R, c, z, d) => (case K.compare(x, z)
54                               of LESS => (case ins c                               of LESS => (case ins c
55                                     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))  
56                                      | c => T(B, T(R,c,z,d), y, b)                                      | c => T(B, T(R,c,z,d), y, b)
57                                    (* end case *))                                    (* end case *))
58                                | EQUAL => T(color, T(R, c, x, d), y, b)                                | EQUAL => T(color, T(R, c, x, d), y, b)
59                                | GREATER => (case ins d                                | GREATER => (case ins d
60                                     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))  
61                                      | d => T(B, T(R,c,z,d), y, b)                                      | d => T(B, T(R,c,z,d), y, b)
62                                    (* end case *))                                    (* end case *))
63                              (* end case *))                              (* end case *))
# Line 66  Line 67 
67                    | GREATER => (case b                    | GREATER => (case b
68                         of T(R, c, z, d) => (case K.compare(x, z)                         of T(R, c, z, d) => (case K.compare(x, z)
69                               of LESS => (case ins c                               of LESS => (case ins c
70                                     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))  
71                                      | c => T(B, a, y, T(R,c,z,d))                                      | c => T(B, a, y, T(R,c,z,d))
72                                    (* end case *))                                    (* end case *))
73                                | EQUAL => T(color, a, y, T(R, c, x, d))                                | EQUAL => T(color, a, y, T(R, c, x, d))
74                                | GREATER => (case ins d                                | GREATER => (case ins d
75                                     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))  
76                                      | d => T(B, a, y, T(R,c,z,d))                                      | d => T(B, a, y, T(R,c,z,d))
77                                    (* end case *))                                    (* end case *))
78                              (* end case *))                              (* end case *))
79                          | _ => T(B, a, y, ins b)                          | _ => T(B, a, y, ins b)
80                        (* end case *))                        (* end case *))
81                  (* end case *))                  (* end case *))
82            val m = ins m            val T(_, a, y, b) = ins m
83            in            in
84              SET(!nItems', m)              SET(!nItems', T(B, a, y, b))
85            end            end
86      fun add' (x, m) = add (m, x)      fun add' (x, m) = add (m, x)
87    
# Line 97  Line 96 
96          | RIGHT of (color * tree * item * zipper)          | RIGHT of (color * tree * item * zipper)
97      in      in
98      fun delete (SET(nItems, t), k) = let      fun delete (SET(nItems, t), k) = let
99            (* zip the zipper *)
100            fun zip (TOP, t) = t            fun zip (TOP, t) = t
101              | 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))
102              | 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))
103          (* bbZip propagates a black deficit up the tree until either the top          (* zip the zipper while resolving a black deficit *)
104           * is reached, or the deficit can be covered.  It returns a boolean            fun fixupZip (TOP, t) = (true, t)
105           * that is true if there is still a deficit and the zipped tree.            (* case 1 from CLR *)
106           *)              | fixupZip (LEFT(B, x, T(R, a, y, b), p), t) = (case a
107            fun bbZip (TOP, t) = (true, t)                   of T(_, T(R, a11, w, a12), z, a2) => (* case 1L ==> case 3L ==> case 4L *)
108              | 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)))
109                  bbZip (LEFT(R, x, c, LEFT(B, y, d, z)), a)                    | T(_, a1, z, T(R, a21, w, t22)) => (* case 1L ==> case 4L *)
110              | 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)))
111                  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 *)
112              | 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)))
113                  (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)
114              | bbZip (LEFT(R, x, T(B, c, y, d), z), a) = (* case 2L *)                  (* end case *))
115                  (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
116              | 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 *)
117                  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)))))
118              | 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 *)
119                  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)))))
120              | 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 *)
121                  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))))
122              | 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)
123                  (false, zip (z, T(color, c, y, T(B, T(R, d, w, e), x, b))))                  (* end case *))
124              | bbZip (RIGHT(R, T(B, c, y, d), x, z), b) = (* case 2R *)            (* case 3 from CLR *)
125                  (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) =
126              | bbZip (RIGHT(B, T(B, c, y, d), x, z), b) = (* case 2R *)                (* case 3L ==> case 4L *)
127                  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))))
128              | bbZip (z, t) = (false, zip(z, t))              | fixupZip (RIGHT(color, T(B, a, x, T(R, b1, y, b2)), z, p), t) =
129            fun delMin (T(R, E, y, b), z) = (y, (false, zip(z, b)))                (* case 3R ==> case 4R; rotate, recolor, plus rotate fixes deficit *)
130              | 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))))
131              (* case 4 from CLR *)
132                | fixupZip (LEFT(color, x, T(B, a, y, T(R, b1, z, b2)), p), t) =
133                    (false, zip (p, T(color, T(B, t, x, a), y, T(B, b1, z, b2))))
134                | fixupZip (RIGHT(color, T(B, T(R, a1, z, a2), x, b), y, p), t) =
135                    (false, zip (p, T(color, T(B, a1, z, a2), x, T(B, b, y, t))))
136              (* case 2 from CLR; note that "a" and "b" are guaranteed to be black, since we did
137               * not match cases 3 or 4.
138               *)
139                | fixupZip (LEFT(R, x, T(B, a, y, b), p), t) =
140                    (false, zip (p, T(B, t, x, T(R, a, y, b))))
141                | fixupZip (LEFT(B, x, T(B, a, y, b), p), t) =
142                    fixupZip (p, T(B, t, x, T(R, a, y, b)))
143                | fixupZip (RIGHT(R, T(B, a, x, b), y, p), t) =
144                    (false, zip (p, T(B, T(R, a, x, b), y, t)))
145                | fixupZip (RIGHT(B, T(B, a, x, b), y, p), t) =
146                    fixupZip (p, T(B, T(R, a, x, b), y, t))
147              (* push deficit up the tree by recoloring a black node as red *)
148                | fixupZip (LEFT(_, y, E, p), t) = fixupZip (p, T(R, t, y, E))
149                | fixupZip (RIGHT(_, E, y, p), t) = fixupZip (p, T(R, E, y, t))
150              (* impossible cases that violate the red invariant *)
151                | fixupZip _ = raise Fail "Red invariant violation"
152            (* delete the minimum value from a non-empty tree, returning a triple
153             * (elem, bd, tr), where elem is the minimum element, tr is the residual
154             * tree with elem removed, and bd is true if tr has a black-depth that is
155             * less than the original tree.
156             *)
157              fun delMin (T(R, E, y, b), p) =
158                  (* replace the node by its right subtree (which must be E) *)
159                    (y, false, zip(p, b))
160                | delMin (T(B, E, y, T(R, a', y', b')), p) =
161                  (* replace the node with its right child, while recoloring the child black to
162                   * preserve the black invariant.
163                   *)
164                    (y, false, zip (p, T(B, a', y', b')))
165                | delMin (T(B, E, y, E), p) = let
166                  (* delete the node, which reduces the black-depth by one, so we attempt to fix
167                   * the deficit on the path back.
168                   *)
169                    val (blkDeficit, t) = fixupZip (p, E)
170                    in
171                      (y, blkDeficit, t)
172                    end
173              | 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))
174              | delMin (E, _) = raise Match              | delMin (E, _) = raise Match
175            fun join (R, E, E, z) = zip(z, E)            fun del (E, z) = raise LibBase.NotFound
176              | join (_, a, E, z) = #2(bbZip(z, a))       (* color = black *)              | del (T(color, a, y, b), p) = (case K.compare(k, y)
177              | join (_, E, b, z) = #2(bbZip(z, b))       (* color = black *)                   of LESS => del (a, LEFT(color, y, b, p))
178              | join (color, a, b, z) = let                    | EQUAL => (case (color, a, b)
179                  val (x, (needB, b')) = delMin(b, TOP)                         of (R, E, E) => zip(p, E)
180                            | (B, E, E) => #2 (fixupZip (p, E))
181                            | (_, T(_, a', y', b'), E) =>
182                              (* node is black and left child is red; we replace the node with its
183                               * left child recolored to black.
184                               *)
185                                zip(p, T(B, a', y', b'))
186                            | (_, E, T(_, a', y', b')) =>
187                              (* node is black and right child is red; we replace the node with its
188                               * right child recolored to black.
189                               *)
190                                zip(p, T(B, a', y', b'))
191                            | _ => let
192                                val (minSucc, blkDeficit, b) = delMin (b, TOP)
193                  in                  in
194                    if needB                                if blkDeficit
195                      then #2(bbZip(z, T(color, a, x, b')))                                  then #2 (fixupZip (RIGHT(color, a, minSucc, p), b))
196                      else zip(z, T(color, a, x, b'))                                  else zip (p, T(color, a, minSucc, b))
197                  end                  end
198            fun del (E, z) = raise LibBase.NotFound                        (* end case *))
199              | del (T(color, a, y, b), z) = (case K.compare(k, y)                    | GREATER => del (b, RIGHT(color, a, y, p))
                  of LESS => del (a, LEFT(color, y, b, z))  
                   | EQUAL => join (color, a, b, z)  
                   | GREATER => del (b, RIGHT(color, a, y, z))  
200                  (* end case *))                  (* end case *))
201            in            in
202              SET(nItems-1, del(t, TOP))              case del(t, TOP)
203                 of T(R, a, x, b) => SET(nItems-1, T(B, a, x, b))
204                  | t => SET(nItems-1, t)
205                (* end case *)
206            end            end
207      end (* local *)      end (* local *)
208    

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