Mercurial > hg > Gears > GearsAgda

changeset 532:ccf98ed4a4f7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix red black tree
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 Jan 2018 23:56:42 +0900
parents f6060e1bf900
children 2d6ccbf429ad
files RedBlackTree.agda
diffstat 1 files changed, 60 insertions(+), 56 deletions(-) [+]
line wrap: on
line diff
--- 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