Mercurial > hg > Gears > GearsAgda

diff RedBlackTree.agda @ 530:63f3df7f5448

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add insertCase41, insertCase5
author ryokka
date Tue, 09 Jan 2018 17:04:34 +0900
parents c9be3631cc41
children f6060e1bf900
line wrap: on
line diff
--- a/RedBlackTree.agda	Tue Jan 09 15:43:35 2018 +0900
+++ b/RedBlackTree.agda	Tue Jan 09 17:04:34 2018 +0900
@@ -67,37 +67,76 @@
         ... | 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 ->
+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 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
+rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent rotateNext = getStack s (\ s n0 -> rotateRight1 tree s n0 parent grandParent 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
+        ... | Just n1 with parent
+        ...           | Nothing = rotateNext tree s n1 Nothing grandParent
+        ...           | Just parent1 with left parent1
+        ...                | Nothing = rotateNext tree s n1 Nothing grandParent
+        ...                | Just leftParent with compare tree (key n1) (key leftParent)
+        ...                                    | EQ = rotateNext tree s n1 parent grandParent
+        ...                                    | _ = rotateNext tree s n1 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 -> 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 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
+rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent rotateNext = getStack s (\ s n0 -> rotateLeft1 tree s n0 parent grandParent 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
+        ... | Just n1 with parent
+        ...           | Nothing = rotateNext tree s n1 Nothing grandParent
+        ...           | Just parent1 with right parent1
+        ...                | Nothing = rotateNext tree s n1 Nothing grandParent
+        ...                | Just rightParent with compare tree (key n1) (key rightParent)
+        ...                                    | EQ = rotateNext tree s n1 parent grandParent
+        ...                                    | _ = rotateNext tree s n1 parent grandParent
 
+{-# 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} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
+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)
 
 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 n0 parent grandParent next       
 ...    | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent)
-...                                              | EQ | EQ = rotateLeft tree s n0 (Just parent) grandParent {!!}
-...                                              | _ | _  = insertCase5 tree s n0 parent grandParent next
+...                                              | EQ | EQ = popStack s (\ s n0 -> rotateLeft tree s n0 {!!} grandParent
+   (\ tree s n0 parent grandParent -> 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
+    ...    | 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
 
 
 {-# TERMINATING #-}