Mercurial > hg > Gears > GearsAgda
diff RedBlackTree.agda @ 538:5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
| author | ryokka |
|---|---|
| date | Wed, 10 Jan 2018 17:38:24 +0900 |
| parents | fffeaf0b0024 |
| children | 6a4830c5a514 |
line wrap: on
line diff
--- a/RedBlackTree.agda Wed Jan 10 15:44:13 2018 +0900 +++ b/RedBlackTree.agda Wed Jan 10 17:38:24 2018 +0900 @@ -52,18 +52,16 @@ -- put new node at parent node, and rebuild tree to the top -- {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html -replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> 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 -> t) -> t -replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s ( - \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) ) - where - replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t - replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } ) - replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } ) - replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } ) - replaceNode1 s (Just grandParent) result with result - ... | LT = replaceNode tree s grandParent ( record parent { left = Just n0 } ) next - ... | GT = replaceNode tree s grandParent ( record parent { right = Just n0 } ) next - ... | EQ = next tree +replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t +replaceNode {n} {m} {t} {a} {k} {si} tree s n0 next = popStack s ( + \s parent -> replaceNode1 s parent) + where + replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> t + replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } ) + replaceNode1 s (Just n1) with compare tree (key n1) (key n0) + ... | LT = replaceNode tree s ( record n1 { left = Just n0 } ) next + ... | GT = replaceNode tree s ( record n1 { right = Just n0 } ) next + ... | EQ = next tree rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> @@ -160,11 +158,11 @@ ... | Black = insertCase4 tree s n0 parent grandParent next insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t insertCase2 s n0 parent grandParent with color parent - ... | Black = replaceNode tree s parent n0 next + ... | Black = replaceNode tree s n0 next ... | Red = insertCase3 s n0 parent grandParent insertCase1 n0 s Nothing Nothing = next tree insertCase1 n0 s Nothing (Just grandParent) = next tree - insertCase1 n0 s (Just parent) Nothing = replaceNode tree s parent (colorNode n0 Black) next + insertCase1 n0 s (Just parent) Nothing = replaceNode tree s (colorNode n0 Black) next insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent ---- @@ -205,7 +203,7 @@ checkNode (Just n) = search n where search : Node a k -> t - search n with compare tree k1 (key n) + search n with compare tree (key n) k1 search n | LT = checkNode (left n) search n | GT = checkNode (right n) search n | EQ = cs tree (Just n)