Mercurial > hg > Gears > GearsAgda
comparison RedBlackTree.agda @ 570:a6aa2ff5fea4
separate clearStack
| author | ryokka |
|---|---|
| date | Thu, 26 Apr 2018 20:09:55 +0900 |
| parents | 40ab3d39e49d |
| children | 73fc32092b64 |
comparison
equal
deleted
inserted
replaced
| 569:f24a73245f36 | 570:a6aa2ff5fea4 |
|---|---|
| 56 -- | 56 -- |
| 57 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html | 57 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html |
| 58 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 | 58 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 |
| 59 replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s ( | 59 replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s ( |
| 60 \s parent -> replaceNode1 s parent) | 60 \s parent -> replaceNode1 s parent) |
| 61 where | 61 module ReplaceNode where |
| 62 replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t | 62 replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t |
| 63 replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } ) | 63 replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } ) |
| 64 replaceNode1 s (Just n1) with compare tree (key n1) (key n0) | 64 replaceNode1 s (Just n1) with compare tree (key n1) (key n0) |
| 65 ... | EQ = replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next | 65 ... | EQ = replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next |
| 66 ... | GT = replaceNode tree s ( record n1 { left = Just n0 } ) next | 66 ... | GT = replaceNode tree s ( record n1 { left = Just n0 } ) next |
| 171 ---- | 171 ---- |
| 172 -- find node potition to insert or to delete, the path will be in the stack | 172 -- find node potition to insert or to delete, the path will be in the stack |
| 173 -- | 173 -- |
| 174 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 | 174 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 |
| 175 findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1) | 175 findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1) |
| 176 where | 176 module FindNode where |
| 177 findNode2 : SingleLinkedStack (Node a k) -> (Maybe (Node a k)) -> t | 177 findNode2 : SingleLinkedStack (Node a k) -> (Maybe (Node a k)) -> t |
| 178 findNode2 s Nothing = next tree s n0 | 178 findNode2 s Nothing = next tree s n0 |
| 179 findNode2 s (Just n) = findNode tree s n0 n next | 179 findNode2 s (Just n) = findNode tree s n0 n next |
| 180 findNode1 : SingleLinkedStack (Node a k) -> (Node a k) -> t | 180 findNode1 : SingleLinkedStack (Node a k) -> (Node a k) -> t |
| 181 findNode1 s n1 with (compare tree (key n0) (key n1)) | 181 findNode1 s n1 with (compare tree (key n0) (key n1)) |