# HG changeset patch # User Shinji KONO # Date 1515509802 -32400 # Node ID ccf98ed4a4f7684e5af93015e6c61fb4cb2c3cf7 # Parent f6060e1bf900150f3b65aa34cef13b597ae57e22 fix red black tree diff -r f6060e1bf900 -r ccf98ed4a4f7 RedBlackTree.agda --- a/RedBlackTree.agda Tue Jan 09 17:26:19 2018 +0900 +++ b/RedBlackTree.agda Tue Jan 09 23:56:42 2018 +0900 @@ -67,83 +67,87 @@ ... | 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) -> 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 -rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent rotateNext = getStack s (\ s n0 -> rotateRight1 tree s n0 parent grandParent rotateNext) +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) -> + (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t +rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext = getStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext) where - rotateRight1 : {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) -> 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 - rotateRight1 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent rotateNext with n0 - ... | Nothing = rotateNext tree s {!!} Nothing grandParent + rotateRight1 : {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) -> + (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t + rotateRight1 {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext with n0 + ... | Nothing = rotateNext tree s Nothing n0 ... | Just n1 with parent - ... | Nothing = rotateNext tree s n1 Nothing grandParent + ... | Nothing = rotateNext tree s (Just n1 ) n0 ... | Just parent1 with left parent1 - ... | Nothing = rotateNext tree s n1 Nothing grandParent + ... | Nothing = rotateNext tree s (Just n1) Nothing ... | Just leftParent with compare tree (key n1) (key leftParent) - ... | EQ = rotateNext tree s n1 parent grandParent - ... | _ = rotateNext tree s n1 parent grandParent + ... | EQ = rotateNext tree s (Just n1) parent + ... | _ = rotateNext tree s (Just n1) parent -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 -> Maybe (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 = getStack s (\ s n0 -> rotateLeft1 tree s n0 parent grandParent rotateNext) +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 -> Maybe (Node a k) -> Maybe (Node a k) -> + (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t +rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext = getStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext) where - rotateLeft1 : {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) -> 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 - rotateLeft1 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent rotateNext with n0 - ... | Nothing = rotateNext tree s {!!} Nothing grandParent + rotateLeft1 : {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) -> + (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t + rotateLeft1 {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext with n0 + ... | Nothing = rotateNext tree s Nothing n0 ... | Just n1 with parent - ... | Nothing = rotateNext tree s n1 Nothing grandParent + ... | Nothing = rotateNext tree s (Just n1) Nothing ... | Just parent1 with right parent1 - ... | Nothing = rotateNext tree s n1 Nothing grandParent + ... | Nothing = rotateNext tree s (Just n1) Nothing ... | Just rightParent with compare tree (key n1) (key rightParent) - ... | EQ = rotateNext tree s n1 parent grandParent - ... | _ = rotateNext tree s n1 parent grandParent + ... | EQ = rotateNext tree s (Just n1) parent + ... | _ = rotateNext tree s (Just n1) parent {-# TERMINATING #-} -insertCase5 : {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 +insertCase5 : {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) -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = pop2Stack s (\ s parent grandParent -> insertCase51 tree s n0 parent grandParent next) where - insertCase51 : {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) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t - insertCase51 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with parent | grandParent - ... | Nothing | _ = next tree - ... | _ | Nothing = next tree - ... | Just parent1 | Just grandParent1 with left parent1 | left grandParent1 - ... | Nothing | _ = next tree - ... | _ | Nothing = next tree - ... | Just leftParent1 | Just leftGrandParent1 - with compare tree (key n0) (key leftParent1) | compare tree (key leftParent1) (key leftGrandParent1) - ... | EQ | EQ = rotateRight tree s {!!} parent grandParent1 - (\ tree s n0 parent grandParent -> insertCase5 tree s n0 parent1 grandParent next) - ... | _ | _ = rotateLeft tree s {!!} parent grandParent1 - (\ tree s n0 parent grandParent -> insertCase5 tree s n0 parent1 grandParent next) + insertCase51 : {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) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t + insertCase51 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with n0 + ... | Nothing = next tree + ... | Just n1 with parent | grandParent + ... | Nothing | _ = next tree + ... | _ | Nothing = next tree + ... | Just parent1 | Just grandParent1 with left parent1 | left grandParent1 + ... | Nothing | _ = next tree + ... | _ | Nothing = next tree + ... | Just leftParent1 | Just leftGrandParent1 + with compare tree (key n1) (key leftParent1) | compare tree (key leftParent1) (key leftGrandParent1) + ... | EQ | EQ = rotateRight tree s n0 parent + (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next) + ... | _ | _ = rotateLeft tree s n0 parent + (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next) 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 | _ = insertCase5 tree s n0 parent grandParent next -... | _ | Nothing = insertCase5 tree s n0 parent grandParent next +... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next +... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next ... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent) -... | EQ | EQ = popStack s (\ s n0 -> rotateLeft tree s n0 {!!} grandParent - (\ tree s n0 parent grandParent -> insertCase5 tree s n0 rightParent grandParent next)) +... | EQ | EQ = popStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent) + (\ tree s n0 parent -> insertCase5 tree s n0 rightParent grandParent next)) ... | _ | _ = insertCase41 tree s n0 parent grandParent next where insertCase41 : {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 insertCase41 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with (left parent) | (right grandParent) - ... | Nothing | _ = insertCase5 tree s n0 parent grandParent next - ... | _ | Nothing = insertCase5 tree s n0 parent grandParent next + ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next + ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next ... | Just leftParent | Just rightGrandParent with compare tree (key n0) (key leftParent) | compare tree (key parent) (key rightGrandParent) - ... | EQ | EQ = popStack s (\ s n0 -> rotateRight tree s n0 {!!} grandParent - (\ tree s n0 parent grandParent -> insertCase5 tree s n0 leftParent grandParent next)) - ... | _ | _ = insertCase5 tree s n0 parent grandParent next + ... | EQ | EQ = popStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent) + (\ tree s n0 parent -> insertCase5 tree s n0 leftParent grandParent next)) + ... | _ | _ = insertCase5 tree s (Just n0) parent grandParent next +colorNode : {n : Level } {a k : Set n} -> Node a k -> Color -> Node a k +colorNode old c = record old { color = c } {-# TERMINATING #-} insertNode : {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 -> (RedBlackTree {n} {m} {t} a k si -> t) -> t -insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 ) +insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (insertCase1 n0) where - insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion + insertCase1 : Node a k -> Stack (Node a k) si -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t insertCase3 s n0 parent grandParent with left grandParent | right grandParent @@ -152,17 +156,17 @@ ... | 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 ( - record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 ) + ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 ( + record grandParent { color = Red ; left = Just ( record parent { color = Black } ) ; right = Just ( record uncle { color = Black } ) }) s 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 insertCase2 s n0 parent grandParent with color parent - ... | Black = replaceNode tree s grandParent n0 next - ... | Red = insertCase3 s n0 parent grandParent - insertCase1 s n0 Nothing Nothing = next tree - insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next - insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next - insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent + ... | Black = replaceNode tree s parent 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) (Just grandParent) = insertCase2 s n0 parent grandParent ---- -- find node potition to insert or to delete, the pass will be in the stack @@ -186,7 +190,7 @@ value = value ; right = Nothing ; left = Nothing ; - color = Black + color = Red } 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