# HG changeset patch
# User ryokka
# Date 1515405045 -32400
# Node ID c2d23641845978394082693c2d58f542eac8c7ae
# Parent  0696b9846415ded51d426b7c072e8fe2b22f7a6c
add rotateRight, rotateLeft

diff -r 0696b9846415 -r c2d236418459 RedBlackTree.agda
--- a/RedBlackTree.agda	Mon Jan 08 18:23:55 2018 +0900
+++ b/RedBlackTree.agda	Mon Jan 08 18:50:45 2018 +0900
@@ -66,16 +66,26 @@
         ... | GT =  replaceNode tree s grandParent ( record parent { 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 -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
--- rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with parent
--- ... | Nothing = insertCase5 tree s n0 parent grandParent next
--- ... | Just parent with compare tree (key n0) (key (left parent)))
---                   | EQ = insetCase5 tree s n0 parent grandParent next
---                   | _ = insetCase5 tree s n0 parent grandParent next
 
+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 ->
+  (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 with parent
+... | Nothing = rotateNext tree s n0 Nothing grandParent
+... | Just parent1 with left parent1
+...                | Nothing = rotateNext tree s n0 Nothing grandParent
+...                | Just leftParent with compare tree (key n0) (key leftParent)
+...                                    | 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 -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
+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
+... | Nothing = rotateNext tree s n0 Nothing grandParent
+... | Just parent1 with right parent1
+...                | Nothing = rotateNext tree s n0 Nothing grandParent
+...                | Just rightParent with compare tree (key n0) (key rightParent)
+...                                    | EQ = rotateNext tree s n0 parent grandParent
+...                                    | _ = rotateNext tree s n0 parent grandParent
 
 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} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}