Mercurial > hg > Gears > GearsAgda

changeset 529:c9be3631cc41

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix insertCase4
author ryokka
date Tue, 09 Jan 2018 15:43:35 +0900
parents 7719f40e1367
children 63f3df7f5448
files RedBlackTree.agda
diffstat 1 files changed, 13 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/RedBlackTree.agda	Tue Jan 09 07:57:52 2018 +0900
+++ b/RedBlackTree.agda	Tue Jan 09 15:43:35 2018 +0900
@@ -58,13 +58,13 @@
       \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
   where
         replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t
-        replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } )   
-        replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
-        replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
+        replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } )
+        replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )
+        replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )
         replaceNode1 s (Just grandParent) result with result
         ... | LT =  replaceNode tree s grandParent ( record parent { left = Just n0 } ) next
         ... | GT =  replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
-        ... | EQ =  next tree 
+        ... | 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 ->
@@ -77,9 +77,9 @@
 ...                                    | 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 -> 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 -> 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
+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
@@ -93,11 +93,11 @@
 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 | _ = {!!}
-...    | _ | Nothing = {!!}
+...    | 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 = {!!}
-...                                              | _ | _  = {!!}
+...                                              | EQ | EQ = rotateLeft tree s n0 (Just parent) grandParent {!!}
+...                                              | _ | _  = insertCase5 tree s n0 parent grandParent next
 
 
 {-# TERMINATING #-}
@@ -113,7 +113,7 @@
     ... | 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 ( 
+    ...                           | 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 )
     ...                           | Black = insertCase4 tree s n0 parent grandParent next
     insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
@@ -134,7 +134,7 @@
     findNode2 s (Just n) = findNode tree s n0 n next
     findNode1 : Stack (Node a k) si -> (Node a k)  -> t
     findNode1 s n1 with (compare tree (key n0) (key n1))
-    ...                                | EQ = next tree s n0 
+    ...                                | EQ = next tree s n0
     ...                                | GT = findNode2 s (right n1)
     ...                                | LT = findNode2 s (left n1)
 
@@ -145,7 +145,7 @@
     value = value ;
     right = Nothing ;
     left  = Nothing ;
-    color = Black 
+    color = Black
   }
 
 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