|
7
|
1 module RedBlackTree where
|
|
|
2
|
|
|
3 open import stack
|
|
|
4 open import Level hiding (zero)
|
|
|
5 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
|
|
|
6 field
|
|
|
7 putImpl : treeImpl -> a -> (treeImpl -> t) -> t
|
|
|
8 getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t
|
|
|
9 open TreeMethods
|
|
|
10
|
|
|
11 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
|
|
|
12 field
|
|
|
13 tree : treeImpl
|
|
|
14 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
|
|
|
15 putTree : a -> (Tree treeImpl -> t) -> t
|
|
|
16 putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
|
|
|
17 getTree : (Tree treeImpl -> Maybe a -> t) -> t
|
|
|
18 getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
|
|
|
19
|
|
|
20 open Tree
|
|
|
21
|
|
|
22 data Color {n : Level } : Set n where
|
|
|
23 Red : Color
|
|
|
24 Black : Color
|
|
|
25
|
|
|
26 data CompareResult {n : Level } : Set n where
|
|
|
27 LT : CompareResult
|
|
|
28 GT : CompareResult
|
|
|
29 EQ : CompareResult
|
|
|
30
|
|
|
31 record Node {n : Level } (a k : Set n) : Set n where
|
|
|
32 inductive
|
|
|
33 field
|
|
|
34 key : k
|
|
|
35 value : a
|
|
|
36 right : Maybe (Node a k)
|
|
|
37 left : Maybe (Node a k)
|
|
|
38 color : Color {n}
|
|
|
39 open Node
|
|
|
40
|
|
|
41 record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where
|
|
|
42 field
|
|
|
43 root : Maybe (Node a k)
|
|
|
44 nodeStack : SingleLinkedStack (Node a k)
|
|
|
45 compare : k -> k -> CompareResult {n}
|
|
|
46
|
|
|
47 open RedBlackTree
|
|
|
48
|
|
|
49 open SingleLinkedStack
|
|
|
50
|
|
|
51 --
|
|
|
52 -- put new node at parent node, and rebuild tree to the top
|
|
|
53 --
|
|
|
54 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
|
|
|
55 replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
|
|
|
56 replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s (
|
|
|
57 \s parent -> replaceNode1 s parent)
|
|
|
58 where
|
|
|
59 replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t
|
|
|
60 replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } )
|
|
|
61 replaceNode1 s (Just n1) with compare tree (key n1) (key n0)
|
|
|
62 ... | EQ = replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next
|
|
|
63 ... | GT = replaceNode tree s ( record n1 { left = Just n0 } ) next
|
|
|
64 ... | LT = replaceNode tree s ( record n1 { right = Just n0 } ) next
|
|
|
65
|
|
|
66
|
|
|
67 rotateRight : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) ->
|
|
|
68 (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
|
|
|
69 rotateRight {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext)
|
|
|
70 where
|
|
|
71 rotateRight1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) ->
|
|
|
72 (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
|
|
|
73 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0
|
|
|
74 ... | Nothing = rotateNext tree s Nothing n0
|
|
|
75 ... | Just n1 with parent
|
|
|
76 ... | Nothing = rotateNext tree s (Just n1 ) n0
|
|
|
77 ... | Just parent1 with left parent1
|
|
|
78 ... | Nothing = rotateNext tree s (Just n1) Nothing
|
|
|
79 ... | Just leftParent with compare tree (key n1) (key leftParent)
|
|
|
80 ... | EQ = rotateNext tree s (Just n1) parent
|
|
|
81 ... | _ = rotateNext tree s (Just n1) parent
|
|
|
82
|
|
|
83
|
|
|
84 rotateLeft : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) ->
|
|
|
85 (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
|
|
|
86 rotateLeft {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext)
|
|
|
87 where
|
|
|
88 rotateLeft1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) ->
|
|
|
89 (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
|
|
|
90 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0
|
|
|
91 ... | Nothing = rotateNext tree s Nothing n0
|
|
|
92 ... | Just n1 with parent
|
|
|
93 ... | Nothing = rotateNext tree s (Just n1) Nothing
|
|
|
94 ... | Just parent1 with right parent1
|
|
|
95 ... | Nothing = rotateNext tree s (Just n1) Nothing
|
|
|
96 ... | Just rightParent with compare tree (key n1) (key rightParent)
|
|
|
97 ... | EQ = rotateNext tree s (Just n1) parent
|
|
|
98 ... | _ = rotateNext tree s (Just n1) parent
|
|
|
99
|
|
|
100 {-# TERMINATING #-}
|
|
|
101 insertCase5 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
|
|
|
102 insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent -> insertCase51 tree s n0 parent grandParent next)
|
|
|
103 where
|
|
|
104 insertCase51 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k -> t) -> t
|
|
|
105 insertCase51 {n} {m} {t} {a} {k} tree s n0 parent grandParent next with n0
|
|
|
106 ... | Nothing = next tree
|
|
|
107 ... | Just n1 with parent | grandParent
|
|
|
108 ... | Nothing | _ = next tree
|
|
|
109 ... | _ | Nothing = next tree
|
|
|
110 ... | Just parent1 | Just grandParent1 with left parent1 | left grandParent1
|
|
|
111 ... | Nothing | _ = next tree
|
|
|
112 ... | _ | Nothing = next tree
|
|
|
113 ... | Just leftParent1 | Just leftGrandParent1
|
|
|
114 with compare tree (key n1) (key leftParent1) | compare tree (key leftParent1) (key leftGrandParent1)
|
|
|
115 ... | EQ | EQ = rotateRight tree s n0 parent
|
|
|
116 (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next)
|
|
|
117 ... | _ | _ = rotateLeft tree s n0 parent
|
|
|
118 (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next)
|
|
|
119
|
|
|
120 insertCase4 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
|
|
|
121 insertCase4 {n} {m} {t} {a} {k} tree s n0 parent grandParent next
|
|
|
122 with (right parent) | (left grandParent)
|
|
|
123 ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next
|
|
|
124 ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next
|
|
|
125 ... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent)
|
|
|
126 ... | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent)
|
|
|
127 (\ tree s n0 parent -> insertCase5 tree s n0 rightParent grandParent next))
|
|
|
128 ... | _ | _ = insertCase41 tree s n0 parent grandParent next
|
|
|
129 where
|
|
|
130 insertCase41 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
|
|
|
131 insertCase41 {n} {m} {t} {a} {k} tree s n0 parent grandParent next
|
|
|
132 with (left parent) | (right grandParent)
|
|
|
133 ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next
|
|
|
134 ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next
|
|
|
135 ... | Just leftParent | Just rightGrandParent with compare tree (key n0) (key leftParent) | compare tree (key parent) (key rightGrandParent)
|
|
|
136 ... | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent)
|
|
|
137 (\ tree s n0 parent -> insertCase5 tree s n0 leftParent grandParent next))
|
|
|
138 ... | _ | _ = insertCase5 tree s (Just n0) parent grandParent next
|
|
|
139
|
|
|
140 colorNode : {n : Level } {a k : Set n} -> Node a k -> Color -> Node a k
|
|
|
141 colorNode old c = record old { color = c }
|
|
|
142
|
|
|
143 {-# TERMINATING #-}
|
|
|
144 insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
|
|
|
145 insertNode {n} {m} {t} {a} {k} tree s n0 next = get2SingleLinkedStack s (insertCase1 n0)
|
|
|
146 where
|
|
|
147 insertCase1 : Node a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion
|
|
|
148 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
|
|
|
149 insertCase3 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t
|
|
|
150 insertCase3 s n0 parent grandParent with left grandParent | right grandParent
|
|
|
151 ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
|
|
|
152 ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next
|
|
|
153 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent )
|
|
|
154 ... | EQ = insertCase4 tree s n0 parent grandParent next
|
|
|
155 ... | _ with color uncle
|
|
|
156 ... | Red = pop2SingleLinkedStack s ( \s p0 p1 -> insertCase1 (
|
|
|
157 record grandParent { color = Red ; left = Just ( record parent { color = Black } ) ; right = Just ( record uncle { color = Black } ) }) s p0 p1 )
|
|
|
158 ... | Black = insertCase4 tree s n0 parent grandParent next
|
|
|
159 insertCase2 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t
|
|
|
160 insertCase2 s n0 parent grandParent with color parent
|
|
|
161 ... | Black = replaceNode tree s n0 next
|
|
|
162 ... | Red = insertCase3 s n0 parent grandParent
|
|
|
163 insertCase1 n0 s Nothing Nothing = next tree
|
|
|
164 insertCase1 n0 s Nothing (Just grandParent) = next tree
|
|
|
165 insertCase1 n0 s (Just parent) Nothing = replaceNode tree s (colorNode n0 Black) next
|
|
|
166 insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
|
|
|
167
|
|
|
168 ----
|
|
|
169 -- find node potition to insert or to delete, the path will be in the stack
|
|
|
170 --
|
|
|
171 findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t
|
|
|
172 findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1)
|
|
|
173 where
|
|
|
174 findNode2 : SingleLinkedStack (Node a k) -> (Maybe (Node a k)) -> t
|
|
|
175 findNode2 s Nothing = next tree s n0
|
|
|
176 findNode2 s (Just n) = findNode tree s n0 n next
|
|
|
177 findNode1 : SingleLinkedStack (Node a k) -> (Node a k) -> t
|
|
|
178 findNode1 s n1 with (compare tree (key n0) (key n1))
|
|
|
179 ... | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n0 } ) )
|
|
|
180 ... | GT = findNode2 s (right n1)
|
|
|
181 ... | LT = findNode2 s (left n1)
|
|
|
182
|
|
|
183
|
|
|
184 leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k
|
|
|
185 leafNode k1 value = record {
|
|
|
186 key = k1 ;
|
|
|
187 value = value ;
|
|
|
188 right = Nothing ;
|
|
|
189 left = Nothing ;
|
|
|
190 color = Red
|
|
|
191 }
|
|
|
192
|
|
|
193 putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
|
|
|
194 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree)
|
|
|
195 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
|
|
|
196 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next))
|
|
|
197
|
|
|
198 getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> (RedBlackTree {n} {m} {t} a k -> (Maybe (Node a k)) -> t) -> t
|
|
|
199 getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
|
|
|
200 module GetRedBlackTree where -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html
|
|
|
201 search : Node a k -> t
|
|
|
202 checkNode : Maybe (Node a k) -> t
|
|
|
203 checkNode Nothing = cs tree Nothing
|
|
|
204 checkNode (Just n) = search n
|
|
|
205 search n with compare tree k1 (key n)
|
|
|
206 search n | LT = checkNode (left n)
|
|
|
207 search n | GT = checkNode (right n)
|
|
|
208 search n | EQ = cs tree (Just n)
|
|
|
209
|
|
|
210 open import Data.Nat hiding (compare)
|
|
|
211
|
|
|
212 compareℕ : ℕ → ℕ → CompareResult {Level.zero}
|
|
|
213 compareℕ x y with Data.Nat.compare x y
|
|
|
214 ... | less _ _ = LT
|
|
|
215 ... | equal _ = EQ
|
|
|
216 ... | greater _ _ = GT
|
|
|
217
|
|
|
218 compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
|
|
|
219 compare2 zero zero = EQ
|
|
|
220 compare2 (suc _) zero = GT
|
|
|
221 compare2 zero (suc _) = LT
|
|
|
222 compare2 (suc x) (suc y) = compare2 x y
|
|
|
223
|
|
|
224
|
|
|
225 createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
|
|
|
226 createEmptyRedBlackTreeℕ {m} a {t} = record {
|
|
|
227 root = Nothing
|
|
|
228 ; nodeStack = emptySingleLinkedStack
|
|
|
229 ; compare = compare2
|
|
|
230 }
|
|
|
231
|
