Mercurial > hg > Gears > GearsAgda

changeset 526:c2d236418459

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add rotateRight, rotateLeft
author ryokka
date Mon, 08 Jan 2018 18:50:45 +0900
parents 0696b9846415
children a829a367cf7d
files RedBlackTree.agda
diffstat 1 files changed, 18 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!}