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-map-fn.sml
ViewVC logotype

Diff of /smlnj-lib/branches/rt-transition/Util/redblack-map-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-map-fn.sml  (* redblack-map-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 RedBlackMapFn (K : ORD_KEY) :> ORD_MAP where Key = K =  functor RedBlackMapFn (K : ORD_KEY) :> ORD_MAP where Key = K =
# Line 26  Line 29 
29      structure Key = K      structure Key = K
30    
31      datatype color = R | B      datatype color = R | B
32      and 'a tree  
33        datatype 'a tree
34        = E        = E
35        | T of (color * 'a tree * K.ord_key * 'a * 'a tree)        | T of (color * 'a tree * K.ord_key * 'a * 'a tree)
36    
# Line 37  Line 41 
41    
42      val empty = MAP(0, E)      val empty = MAP(0, E)
43    
44      fun singleton (xk, x) = MAP(1, T(R, E, xk, x, E))      fun singleton (xk, x) = MAP(1, T(B, E, xk, x, E))
45    
46      fun insert (MAP(nItems, m), xk, x) = let      fun insert (MAP(nItems, m), xk, x) = let
47            val nItems' = ref nItems            val nItems' = ref nItems
# Line 77  Line 81 
81                          | _ => T(B, a, yk, y, ins b)                          | _ => T(B, a, yk, y, ins b)
82                        (* end case *))                        (* end case *))
83                  (* end case *))                  (* end case *))
84            val m = ins m            val T(_, a, yk, y, b) = ins m
85            in            in
86              MAP(!nItems', m)              MAP(!nItems', T(B, a, yk, y, b))
87            end            end
88      fun insert' ((xk, x), m) = insert (m, xk, x)      fun insert' ((xk, x), m) = insert (m, xk, x)
89    
# Line 129  Line 133 
133          | RIGHT of (color * 'a tree * K.ord_key * 'a * 'a zipper)          | RIGHT of (color * 'a tree * K.ord_key * 'a * 'a zipper)
134      in      in
135      fun remove (MAP(nItems, t), k) = let      fun remove (MAP(nItems, t), k) = let
136            (* zip the zipper *)
137            fun zip (TOP, t) = t            fun zip (TOP, t) = t
138              | zip (LEFT(color, xk, x, b, z), a) = zip(z, T(color, a, xk, x, b))              | zip (LEFT(color, xk, x, b, z), a) = zip(z, T(color, a, xk, x, b))
139              | zip (RIGHT(color, a, xk, x, z), b) = zip(z, T(color, a, xk, x, b))              | zip (RIGHT(color, a, xk, x, z), b) = zip(z, T(color, a, xk, x, b))
140          (* bbZip propagates a black deficit up the tree until either the top          (* zip the zipper while resolving a black deficit *)
141           * is reached, or the deficit can be covered.  It returns a boolean            fun fixupZip (TOP, t) = (true, t)
142           * that is true if there is still a deficit and the zipped tree.            (* case 1 from CLR *)
143           *)              | fixupZip (LEFT(B, xk, x, T(R, a, yk, y, b), p), t) = (case a
144            fun bbZip (TOP, t) = (true, t)                   of T(_, T(R, a11, wk, w, a12), zk, z, a2) => (* case 1L ==> case 3L ==> case 4L *)
145              | bbZip (LEFT(B, xk, x, T(R, c, yk, y, d), z), a) = (* case 1L *)                        (false, zip (p, T(B, T(R, T(B, t, xk, x, a11), wk, w, T(B, a12, zk, z, a2)), yk, y, b)))
146                  bbZip (LEFT(R, xk, x, c, LEFT(B, yk, y, d, z)), a)                    | T(_, a1, zk, z, T(R, a21, wk, w, t22)) => (* case 1L ==> case 4L *)
147              | bbZip (LEFT(color, xk, x, T(B, T(R, c, yk, y, d), wk, w, e), z), a) =                        (false, zip (p, T(B, T(R, T(B, t, xk, x, a1), zk, z, T(B, a21, wk, w, t22)), yk, y, b)))
148                (* case 3L *)                    | T(_, a1, zk, z, a2) => (* case 1L ==> case 2L; rotate + recolor fixes deficit *)
149                  bbZip (LEFT(color, xk, x, T(B, c, yk, y, T(R, d, wk, w, e)), z), a)                        (false, zip (p, T(B, T(B, t, xk, x, T(R, a1, zk, z, a2)), yk, y, b)))
150              | bbZip (LEFT(color, xk, x, T(B, c, yk, y, T(R, d, wk, w, e)), z), a) =                    | _ => fixupZip (LEFT(R, xk, x, a, LEFT(B, yk, y, b, p)), t)
151                (* case 4L *)                  (* end case *))
152                  (false, zip (z, T(color, T(B, a, xk, x, c), yk, y, T(B, d, wk, w, e))))              | fixupZip (RIGHT(B, T(R, a, xk, x, b), yk, y, p), t) = (case b
153              | bbZip (LEFT(R, xk, x, T(B, c, yk, y, d), z), a) = (* case 2L *)                   of T(_, b1, zk, z, T(R, b21, wk, w, b22)) => (* case 1R ==> case 3R ==> case 4R *)
154                  (false, zip (z, T(B, a, xk, x, T(R, c, yk, y, d))))                        (false, zip (p, T(B, a, xk, x, T(R, T(B, b1, zk, z, b21), wk, w, T(B, b22, yk, y, t)))))
155              | bbZip (LEFT(B, xk, x, T(B, c, yk, y, d), z), a) = (* case 2L *)                    | T(_, T(R, b11, wk, w, b12), zk, z, b2) => (* case 1R ==> case 4R *)
156                  bbZip (z, T(B, a, xk, x, T(R, c, yk, y, d)))                        (false, zip (p, T(B, a, xk, x, T(R, T(B, b11, wk, w, b12), zk, z, T(B, b2, yk, y, t)))))
157              | bbZip (RIGHT(color, T(R, c, yk, y, d), xk, x, z), b) = (* case 1R *)                    | T(_, b1, zk, z, b2) => (* case 1L ==> case 2L; rotate + recolor fixes deficit *)
158                  bbZip (RIGHT(R, d, xk, x, RIGHT(B, c, yk, y, z)), b)                        (false, zip (p, T(B, a, xk, x, T(B, T(R, b1, zk, z, b2), yk, y, t))))
159              | bbZip (RIGHT(color, T(B, T(R, c, wk, w, d), yk, y, e), xk, x, z), b) =                    | _ => fixupZip (RIGHT(R, b, yk, y, RIGHT(B, a, xk, x, p)), t)
160                (* case 3R *)                  (* end case *))
161                  bbZip (RIGHT(color, T(B, c, wk, w, T(R, d, yk, y, e)), xk, x, z), b)            (* case 3 from CLR *)
162              | bbZip (RIGHT(color, T(B, c, yk, y, T(R, d, wk, w, e)), xk, x, z), b) =              | fixupZip (LEFT(color, xk, x, T(B, T(R, a1, yk, y, a2), zk, z, b), p), t) =
163                (* case 4R *)                (* case 3L ==> case 4L *)
164                  (false, zip (z, T(color, c, yk, y, T(B, T(R, d, wk, w, e), xk, x, b))))                  (false, zip (p, T(color, T(B, t, xk, x, a1), yk, y, T(B, a2, zk, z, b))))
165              | bbZip (RIGHT(R, T(B, c, yk, y, d), xk, x, z), b) = (* case 2R *)              | fixupZip (RIGHT(color, T(B, a, xk, x, T(R, b1, yk, y, b2)), zk, z, p), t) =
166                  (false, zip (z, T(B, T(R, c, yk, y, d), xk, x, b)))                (* case 3R ==> case 4R; rotate, recolor, plus rotate fixes deficit *)
167              | bbZip (RIGHT(B, T(B, c, yk, y, d), xk, x, z), b) = (* case 2R *)                  (false, zip (p, T(color, T(B, a, xk, x, b1), yk, y, T(B, b2, zk, z, t))))
168                  bbZip (z, T(B, T(R, c, yk, y, d), xk, x, b))            (* case 4 from CLR *)
169              | bbZip (z, t) = (false, zip(z, t))              | fixupZip (LEFT(color, xk, x, T(B, a, yk, y, T(R, b1, zk, z, b2)), p), t) =
170            fun delMin (T(R, E, yk, y, b), z) = (yk, y, (false, zip(z, b)))                  (false, zip (p, T(color, T(B, t, xk, x, a), yk, y, T(B, b1, zk, z, b2))))
171              | delMin (T(B, E, yk, y, b), z) = (yk, y, bbZip(z, b))              | fixupZip (RIGHT(color, T(B, T(R, a1, zk, z, a2), xk, x, b), yk, y, p), t) =
172                    (false, zip (p, T(color, T(B, a1, zk, z, a2), xk, x, T(B, b, yk, y, t))))
173              (* case 2 from CLR; note that "a" and "b" are guaranteed to be black, since we did
174               * not match cases 3 or 4.
175               *)
176                | fixupZip (LEFT(R, xk, x, T(B, a, yk, y, b), p), t) =
177                    (false, zip (p, T(B, t, xk, x, T(R, a, yk, y, b))))
178                | fixupZip (LEFT(B, xk, x, T(B, a, yk, y, b), p), t) =
179                    fixupZip (p, T(B, t, xk, x, T(R, a, yk, y, b)))
180                | fixupZip (RIGHT(R, T(B, a, xk, x, b), yk, y, p), t) =
181                    (false, zip (p, T(B, T(R, a, xk, x, b), yk, y, t)))
182                | fixupZip (RIGHT(B, T(B, a, xk, x, b), yk, y, p), t) =
183                    fixupZip (p, T(B, T(R, a, xk, x, b), yk, y, t))
184              (* push deficit up the tree by recoloring a black node as red *)
185                | fixupZip (LEFT(_, yk, y, E, p), t) = fixupZip (p, T(R, t, yk, y, E))
186                | fixupZip (RIGHT(_, E, yk, y, p), t) = fixupZip (p, T(R, E, yk, y, t))
187              (* impossible cases that violate the red invariant *)
188                | fixupZip _ = raise Fail "Red invariant violation"
189            (* delete the minimum value from a non-empty tree, returning a 4-tuple
190             * (key, elem, bd, tr), where key is the minimum key, elem is the element
191             * named by key, tr is the residual tree with elem removed, and bd is true
192             * if tr has a black-depth that is less than the original tree.
193             *)
194              fun delMin (T(R, E, yk, y, b), p) =
195                  (* replace the node by its right subtree (which must be E) *)
196                    (yk, y, false, zip(p, b))
197                | delMin (T(B, E, yk, y, T(R, a', yk', y', b')), p) =
198                  (* replace the node with its right child, while recoloring the child black to
199                   * preserve the black invariant.
200                   *)
201                    (yk, y, false, zip (p, T(B, a', yk', y', b')))
202                | delMin (T(B, E, yk, y, E), p) = let
203                  (* delete the node, which reduces the black-depth by one, so we attempt to fix
204                   * the deficit on the path back.
205                   *)
206                    val (blkDeficit, t) = fixupZip (p, E)
207                    in
208                      (yk, y, blkDeficit, t)
209                    end
210              | delMin (T(color, a, yk, y, b), z) = delMin(a, LEFT(color, yk, y, b, z))              | delMin (T(color, a, yk, y, b), z) = delMin(a, LEFT(color, yk, y, b, z))
211              | delMin (E, _) = raise Match              | delMin (E, _) = raise Match
212            fun join (R, E, E, z) = zip(z, E)            fun del (E, p) = raise LibBase.NotFound
213              | join (_, a, E, z) = #2(bbZip(z, a))       (* color = black *)              | del (T(color, a, yk, y, b), p) = (case K.compare(k, yk)
214              | join (_, E, b, z) = #2(bbZip(z, b))       (* color = black *)                   of LESS => del (a, LEFT(color, yk, y, b, p))
215              | join (color, a, b, z) = let                    | EQUAL => (case (color, a, b)
216                  val (xk, x, (needB, b')) = delMin(b, TOP)                         of (R, E, E) => (y, zip(p, E))
217                  in                          | (B, E, E) => (y, #2 (fixupZip (p, E)))
218                    if needB                          | (_, T(_, a', yk', y', b'), E) =>
219                      then #2(bbZip(z, T(color, a, xk, x, b')))                            (* node is black and left child is red; we replace the node with its
220                      else zip(z, T(color, a, xk, x, b'))                             * left child recolored to black.
221                  end                             *)
222            fun del (E, z) = raise LibBase.NotFound                              (y, zip(p, T(B, a', yk', y', b')))
223              | del (T(color, a, yk, y, b), z) = (case K.compare(k, yk)                          | (_, E, T(_, a', yk', y', b')) =>
224                   of LESS => del (a, LEFT(color, yk, y, b, z))                            (* node is black and right child is red; we replace the node with its
225                    | EQUAL => (y, join (color, a, b, z))                             * right child recolored to black.
226                    | GREATER => del (b, RIGHT(color, a, yk, y, z))                             *)
227                                (y, zip(p, T(B, a', yk', y', b')))
228                            | _ => let
229                                val (minKey, minElem, blkDeficit, b) = delMin (b, TOP)
230                                in
231                                  if blkDeficit
232                                    then (y, #2 (fixupZip (RIGHT(color, a, minKey, minElem, p), b)))
233                                    else (y, zip (p, T(color, a, minKey, minElem, b)))
234                                end
235                          (* end case *))
236                      | GREATER => del (b, RIGHT(color, a, yk, y, p))
237                  (* end case *))                  (* end case *))
238            val (item, t) = del(t, TOP)            val (item, t) = del(t, TOP)
239            in            in
240              (MAP(nItems-1, t), item)              case t
241                 of T(R, a, xk, x, b) => (MAP(nItems-1, T(B, a, xk, x, b)), item)
242                  | t => (MAP(nItems-1, t), item)
243                (* end case *)
244            end            end
245      end (* local *)      end (* local *)
246    
# Line 506  Line 562 
562              foldli f' empty              foldli f' empty
563            end            end
564    
565      (* check the elements of a map with a predicate and return true if
566       * any element satisfies the predicate. Return false otherwise.
567       * Elements are checked in key order.
568       *)
569        fun exists pred = let
570              fun exists' E = false
571                | exists' (T(_, a, _, x, b)) = exists' a orelse pred x orelse exists' b
572              in
573                fn (MAP(_, m)) => exists' m
574              end
575        fun existsi pred = let
576              fun exists' E = false
577                | exists' (T(_, a, k, x, b)) = exists' a orelse pred(k, x) orelse exists' b
578              in
579                fn (MAP(_, m)) => exists' m
580              end
581    
582      (* check the elements of a map with a predicate and return true if
583       * they all satisfy the predicate. Return false otherwise.  Elements
584       * are checked in key order.
585       *)
586        fun all pred = let
587              fun all' E = true
588                | all' (T(_, a, _, x, b)) = all' a andalso pred x andalso all' b
589              in
590                fn (MAP(_, m)) => all' m
591              end
592        fun alli pred = let
593              fun all' E = true
594                | all' (T(_, a, k, x, b)) = all' a andalso pred(k, x) andalso all' b
595              in
596                fn (MAP(_, m)) => all' m
597              end
598    
599    end;    end;

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