Mercurial > hg > Members > Moririn

comparison RedBlackTree.agda @ 531:f6060e1bf900

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add clearStack
author ryokka
date Tue, 09 Jan 2018 17:26:19 +0900
parents 63f3df7f5448
children ccf98ed4a4f7
comparison
equal deleted inserted replaced
530:63f3df7f5448 531:f6060e1bf900
162 insertCase1 s n0 Nothing Nothing = next tree 162 insertCase1 s n0 Nothing Nothing = next tree
163 insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next 163 insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
164 insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next 164 insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
165 insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent 165 insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
166 166
167 167 ----
168 -- find node potition to insert or to delete, the pass will be in the stack
169 --
168 findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t 170 findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
169 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1) 171 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
170 where 172 where
171 findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t 173 findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
172 findNode2 s Nothing = next tree s n0 174 findNode2 s Nothing = next tree s n0
188 } 190 }
189 191
190 putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t 192 putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
191 putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree) 193 putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
192 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) 194 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
193 ... | Just n2 = findNode tree (nodeStack tree) (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next) 195 ... | Just n2 = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next))
194 196
195 getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t 197 getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t
196 getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree) 198 getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
197 where 199 where
198 checkNode : Maybe (Node a k) -> t 200 checkNode : Maybe (Node a k) -> t