# HG changeset patch # User ryokka # Date 1515480215 -32400 # Node ID c9be3631cc4133fa8bede5f6784a64cf1c6f6842 # Parent 7719f40e136783f8445adaf5cfac4209d2b1380c fix insertCase4 diff -r 7719f40e1367 -r c9be3631cc41 RedBlackTree.agda --- a/RedBlackTree.agda Tue Jan 09 07:57:52 2018 +0900 +++ b/RedBlackTree.agda Tue Jan 09 15:43:35 2018 +0900 @@ -58,13 +58,13 @@ \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 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 + ... | 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 -> Node a k -> Maybe (Node a k) -> Node a k -> @@ -77,9 +77,9 @@ ... | EQ = rotateNext tree s n0 parent grandParent ... | _ = rotateNext tree s n0 parent grandParent -rotateleft : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Maybe (Node a k) -> Node a k -> +rotateLeft : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Maybe (Node a k) -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Maybe (Node a k) -> Node a k -> t) -> t -rotateleft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent rotateNext with parent +rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent rotateNext with parent ... | Nothing = rotateNext tree s n0 Nothing grandParent ... | Just parent1 with right parent1 ... | Nothing = rotateNext tree s n0 Nothing grandParent @@ -93,11 +93,11 @@ insertCase4 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with (right parent) | (left grandParent) -... | Nothing | _ = {!!} -... | _ | Nothing = {!!} +... | Nothing | _ = insertCase5 tree s n0 parent grandParent next +... | _ | Nothing = insertCase5 tree s n0 parent grandParent next ... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent) -... | EQ | EQ = {!!} -... | _ | _ = {!!} +... | EQ | EQ = rotateLeft tree s n0 (Just parent) grandParent {!!} +... | _ | _ = insertCase5 tree s n0 parent grandParent next {-# TERMINATING #-} @@ -113,7 +113,7 @@ ... | Just uncle | _ with compare tree ( key uncle ) ( key parent ) ... | EQ = insertCase4 tree s n0 parent grandParent next ... | _ with color uncle - ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( + ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 ) ... | Black = insertCase4 tree s n0 parent grandParent next insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t @@ -134,7 +134,7 @@ findNode2 s (Just n) = findNode tree s n0 n next findNode1 : Stack (Node a k) si -> (Node a k) -> t findNode1 s n1 with (compare tree (key n0) (key n1)) - ... | EQ = next tree s n0 + ... | EQ = next tree s n0 ... | GT = findNode2 s (right n1) ... | LT = findNode2 s (left n1) @@ -145,7 +145,7 @@ value = value ; right = Nothing ; left = Nothing ; - color = Black + color = Black } 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