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

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

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

revision 2980, Sat Apr 12 15:01:15 2008 UTC revision 4070, Thu Jun 11 12:33:25 2015 UTC
# Line 1  Line 1 
1  (* int-redblack-map.sml  (* int-redblack-map.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 IntRedBlackMap :> ORD_MAP where type Key.ord_key = int =  structure IntRedBlackMap :> ORD_MAP where type Key.ord_key = int =
# Line 30  Line 33 
33        end        end
34    
35      datatype color = R | B      datatype color = R | B
36      and 'a tree  
37        datatype 'a tree
38        = E        = E
39        | T of (color * 'a tree * int * 'a * 'a tree)        | T of (color * 'a tree * Key.ord_key * 'a * 'a tree)
40    
41      datatype 'a map = MAP of (int * 'a tree)      datatype 'a map = MAP of (int * 'a tree)
42    
# Line 41  Line 45 
45    
46      val empty = MAP(0, E)      val empty = MAP(0, E)
47    
48      fun singleton (xk, x) = MAP(1, T(R, E, xk, x, E))      fun singleton (xk, x) = MAP(1, T(B, E, xk, x, E))
49    
50      fun insert (MAP(nItems, m), xk, x) = let      fun insert (MAP(nItems, m), xk, x) = let
51            val nItems' = ref nItems            val nItems' = ref nItems
# Line 52  Line 56 
56                       of T(R, c, zk, z, d) =>                       of T(R, c, zk, z, d) =>
57                            if (xk < zk)                            if (xk < zk)
58                              then (case ins c                              then (case ins c
59                                 of T(R, e, wk, w, f) =>                                 of T(R, e, wk, w, f) => T(R, T(B,e,wk,w,f), zk, z, T(B,d,yk,y,b))
                                     T(R, T(B,e,wk,w,f), zk, z, T(B,d,yk,y,b))  
60                                  | c => T(B, T(R,c,zk,z,d), yk, y, b)                                  | c => T(B, T(R,c,zk,z,d), yk, y, b)
61                                (* end case *))                                (* end case *))
62                            else if (xk = zk)                            else if (xk = zk)
63                              then T(color, T(R, c, xk, x, d), yk, y, b)                              then T(color, T(R, c, xk, x, d), yk, y, b)
64                              else (case ins d                              else (case ins d
65                                 of T(R, e, wk, w, f) =>                                 of T(R, e, wk, w, f) => T(R, T(B,c,zk,z,e), wk, w, T(B,f,yk,y,b))
                                     T(R, T(B,c,zk,z,e), wk, w, T(B,f,yk,y,b))  
66                                  | d => T(B, T(R,c,zk,z,d), yk, y, b)                                  | d => T(B, T(R,c,zk,z,d), yk, y, b)
67                                (* end case *))                                (* end case *))
68                        | _ => T(B, ins a, yk, y, b)                        | _ => T(B, ins a, yk, y, b)
# Line 71  Line 73 
73                       of T(R, c, zk, z, d) =>                       of T(R, c, zk, z, d) =>
74                            if (xk < zk)                            if (xk < zk)
75                              then (case ins c                              then (case ins c
76                                 of T(R, e, wk, w, f) =>                                 of T(R, e, wk, w, f) => T(R, T(B,a,yk,y,e), wk, w, T(B,f,zk,z,d))
                                     T(R, T(B,a,yk,y,e), wk, w, T(B,f,zk,z,d))  
77                                  | c => T(B, a, yk, y, T(R,c,zk,z,d))                                  | c => T(B, a, yk, y, T(R,c,zk,z,d))
78                                (* end case *))                                (* end case *))
79                            else if (xk = zk)                            else if (xk = zk)
80                              then T(color, a, yk, y, T(R, c, xk, x, d))                              then T(color, a, yk, y, T(R, c, xk, x, d))
81                              else (case ins d                              else (case ins d
82                                 of T(R, e, wk, w, f) =>                                 of T(R, e, wk, w, f) => T(R, T(B,a,yk,y,c), zk, z, T(B,e,wk,w,f))
                                     T(R, T(B,a,yk,y,c), zk, z, T(B,e,wk,w,f))  
83                                  | d => T(B, a, yk, y, T(R,c,zk,z,d))                                  | d => T(B, a, yk, y, T(R,c,zk,z,d))
84                                (* end case *))                                (* end case *))
85                        | _ => T(B, a, yk, y, ins b)                        | _ => T(B, a, yk, y, ins b)
86                      (* end case *))                      (* end case *))
87            val m = ins m            val T(_, a, yk, y, b) = ins m
88            in            in
89              MAP(!nItems', m)              MAP(!nItems', T(B, a, yk, y, b))
90            end            end
91      fun insert' ((xk, x), m) = insert (m, xk, x)      fun insert' ((xk, x), m) = insert (m, xk, x)
92    
# Line 131  Line 131 
131      local      local
132        datatype 'a zipper        datatype 'a zipper
133          = TOP          = TOP
134          | LEFT of (color * int * 'a * 'a tree * 'a zipper)          | LEFT of (color * Key.ord_key * 'a * 'a tree * 'a zipper)
135          | RIGHT of (color * 'a tree * int * 'a * 'a zipper)          | RIGHT of (color * 'a tree * Key.ord_key * 'a * 'a zipper)
136      in      in
137      fun remove (MAP(nItems, t), k) = let      fun remove (MAP(nItems, t), k) = let
138            (* zip the zipper *)
139            fun zip (TOP, t) = t            fun zip (TOP, t) = t
140              | 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))
141              | 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))
142          (* bbZip propagates a black deficit up the tree until either the top          (* zip the zipper while resolving a black deficit *)
143           * is reached, or the deficit can be covered.  It returns a boolean            fun fixupZip (TOP, t) = (true, t)
144           * that is true if there is still a deficit and the zipped tree.            (* case 1 from CLR *)
145           *)              | fixupZip (LEFT(B, xk, x, T(R, a, yk, y, b), p), t) = (case a
146            fun bbZip (TOP, t) = (true, t)                   of T(_, T(R, a11, wk, w, a12), zk, z, a2) => (* case 1L ==> case 3L ==> case 4L *)
147              | 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)))
148                  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 *)
149              | 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)))
150                (* case 3L *)                    | T(_, a1, zk, z, a2) => (* case 1L ==> case 2L; rotate + recolor fixes deficit *)
151                  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)))
152              | 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)
153                (* case 4L *)                  (* end case *))
154                  (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
155              | 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 *)
156                  (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)))))
157              | 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 *)
158                  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)))))
159              | 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 *)
160                  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))))
161              | 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)
162                (* case 3R *)                  (* end case *))
163                  bbZip (RIGHT(color, T(B, c, wk, w, T(R, d, yk, y, e)), xk, x, z), b)            (* case 3 from CLR *)
164              | 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) =
165                (* case 4R *)                (* case 3L ==> case 4L *)
166                  (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))))
167              | 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) =
168                  (false, zip (z, T(B, T(R, c, yk, y, d), xk, x, b)))                (* case 3R ==> case 4R; rotate, recolor, plus rotate fixes deficit *)
169              | 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))))
170                  bbZip (z, T(B, T(R, c, yk, y, d), xk, x, b))            (* case 4 from CLR *)
171              | 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) =
172            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))))
173              | 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) =
174                    (false, zip (p, T(color, T(B, a1, zk, z, a2), xk, x, T(B, b, yk, y, t))))
175              (* case 2 from CLR; note that "a" and "b" are guaranteed to be black, since we did
176               * not match cases 3 or 4.
177               *)
178                | fixupZip (LEFT(R, xk, x, T(B, a, yk, y, b), p), t) =
179                    (false, zip (p, T(B, t, xk, x, T(R, a, yk, y, b))))
180                | fixupZip (LEFT(B, xk, x, T(B, a, yk, y, b), p), t) =
181                    fixupZip (p, T(B, t, xk, x, T(R, a, yk, y, b)))
182                | fixupZip (RIGHT(R, T(B, a, xk, x, b), yk, y, p), t) =
183                    (false, zip (p, T(B, T(R, a, xk, x, b), yk, y, t)))
184                | fixupZip (RIGHT(B, T(B, a, xk, x, b), yk, y, p), t) =
185                    fixupZip (p, T(B, T(R, a, xk, x, b), yk, y, t))
186              (* push deficit up the tree by recoloring a black node as red *)
187                | fixupZip (LEFT(_, yk, y, E, p), t) = fixupZip (p, T(R, t, yk, y, E))
188                | fixupZip (RIGHT(_, E, yk, y, p), t) = fixupZip (p, T(R, E, yk, y, t))
189              (* impossible cases that violate the red invariant *)
190                | fixupZip _ = raise Fail "Red invariant violation"
191            (* delete the minimum value from a non-empty tree, returning a 4-tuple
192             * (key, elem, bd, tr), where key is the minimum key, elem is the element
193             * named by key, tr is the residual tree with elem removed, and bd is true
194             * if tr has a black-depth that is less than the original tree.
195             *)
196              fun delMin (T(R, E, yk, y, b), p) =
197                  (* replace the node by its right subtree (which must be E) *)
198                    (yk, y, false, zip(p, b))
199                | delMin (T(B, E, yk, y, T(R, a', yk', y', b')), p) =
200                  (* replace the node with its right child, while recoloring the child black to
201                   * preserve the black invariant.
202                   *)
203                    (yk, y, false, zip (p, T(B, a', yk', y', b')))
204                | delMin (T(B, E, yk, y, E), p) = let
205                  (* delete the node, which reduces the black-depth by one, so we attempt to fix
206                   * the deficit on the path back.
207                   *)
208                    val (blkDeficit, t) = fixupZip (p, E)
209                    in
210                      (yk, y, blkDeficit, t)
211                    end
212              | 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))
213              | delMin (E, _) = raise Match              | delMin (E, _) = raise Match
214            fun join (R, E, E, z) = zip(z, E)            fun del (E, p) = raise LibBase.NotFound
215              | join (_, a, E, z) = #2(bbZip(z, a))       (* color = black *)              | del (T(color, a, yk, y, b), p) =
             | join (_, E, b, z) = #2(bbZip(z, b))       (* color = black *)  
             | join (color, a, b, z) = let  
                 val (xk, x, (needB, b')) = delMin(b, TOP)  
                 in  
                   if needB  
                     then #2(bbZip(z, T(color, a, xk, x, b')))  
                     else zip(z, T(color, a, xk, x, b'))  
                 end  
           fun del (E, z) = raise LibBase.NotFound  
             | del (T(color, a, yk, y, b), z) =  
216                  if (k < yk)                  if (k < yk)
217                    then del (a, LEFT(color, yk, y, b, z))                    then del (a, LEFT(color, yk, y, b, p))
218                  else if (k = yk)                  else if (k = yk)
219                    then (y, join (color, a, b, z))                    then (case (color, a, b)
220                    else del (b, RIGHT(color, a, yk, y, z))                       of (R, E, E) => (y, zip(p, E))
221                          | (B, E, E) => (y, #2 (fixupZip (p, E)))
222                          | (_, T(_, a', yk', y', b'), E) =>
223                            (* node is black and left child is red; we replace the node with its
224                             * left child recolored to black.
225                             *)
226                              (y, zip(p, T(B, a', yk', y', b')))
227                          | (_, E, T(_, a', yk', y', b')) =>
228                            (* node is black and right child is red; we replace the node with its
229                             * right child recolored to black.
230                             *)
231                              (y, zip(p, T(B, a', yk', y', b')))
232                          | _ => let
233                              val (minKey, minElem, blkDeficit, b) = delMin (b, TOP)
234                              in
235                                if blkDeficit
236                                  then (y, #2 (fixupZip (RIGHT(color, a, minKey, minElem, p), b)))
237                                  else (y, zip (p, T(color, a, minKey, minElem, b)))
238                              end
239                        (* end case *))
240                      else del (b, RIGHT(color, a, yk, y, p))
241            val (item, t) = del(t, TOP)            val (item, t) = del(t, TOP)
242            in            in
243              (MAP(nItems-1, t), item)              case t
244                 of T(R, a, xk, x, b) => (MAP(nItems-1, T(B, a, xk, x, b)), item)
245                  | t => (MAP(nItems-1, t), item)
246                (* end case *)
247            end            end
248      end (* local *)      end (* local *)
249    
# Line 288  Line 340 
340     *)     *)
341      datatype 'a digit      datatype 'a digit
342        = ZERO        = ZERO
343        | ONE of (int * 'a * 'a tree * 'a digit)        | ONE of (Key.ord_key * 'a * 'a tree * 'a digit)
344        | TWO of (int * 'a * 'a tree * int * 'a * 'a tree * 'a digit)        | TWO of (Key.ord_key * 'a * 'a tree * Key.ord_key * 'a * 'a tree * 'a digit)
345    (* 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 *)
346      fun addItem (ak, a, l) = let      fun addItem (ak, a, l) = let
347            fun incr (ak, a, t, ZERO) = ONE(ak, a, t, ZERO)            fun incr (ak, a, t, ZERO) = ONE(ak, a, t, ZERO)
# Line 511  Line 563 
563              foldli f' empty              foldli f' empty
564            end            end
565    
566      (* check the elements of a map with a predicate and return true if
567       * any element satisfies the predicate. Return false otherwise.
568       * Elements are checked in key order.
569       *)
570        fun exists pred = let
571              fun exists' E = false
572                | exists' (T(_, a, _, x, b)) = exists' a orelse pred x orelse exists' b
573              in
574                fn (MAP(_, m)) => exists' m
575              end
576        fun existsi pred = let
577              fun exists' E = false
578                | exists' (T(_, a, k, x, b)) = exists' a orelse pred(k, x) orelse exists' b
579              in
580                fn (MAP(_, m)) => exists' m
581              end
582    
583      (* check the elements of a map with a predicate and return true if
584       * they all satisfy the predicate. Return false otherwise.  Elements
585       * are checked in key order.
586       *)
587        fun all pred = let
588              fun all' E = true
589                | all' (T(_, a, _, x, b)) = all' a andalso pred x andalso all' b
590              in
591                fn (MAP(_, m)) => all' m
592              end
593        fun alli pred = let
594              fun all' E = true
595                | all' (T(_, a, k, x, b)) = all' a andalso pred(k, x) andalso all' b
596              in
597                fn (MAP(_, m)) => all' m
598              end
599    
600    end;    end;

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

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