Mercurial > hg > Members > Moririn

changeset 540:6a4830c5a514

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
testing
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 11 Jan 2018 11:55:22 +0900
parents 39d465c20e5a
children 429ece770187
files RedBlackTree.agda redBlackTreeTest.agda
diffstat 2 files changed, 18 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/RedBlackTree.agda	Wed Jan 10 18:10:03 2018 +0900
+++ b/RedBlackTree.agda	Thu Jan 11 11:55:22 2018 +0900
@@ -59,9 +59,9 @@
           replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> t 
           replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } )
           replaceNode1 s (Just n1) with compare tree (key n1) (key n0)
-          ... | LT =  replaceNode tree s ( record n1 { left = Just n0 } ) next
+          ... | EQ =  next tree
           ... | GT =  replaceNode tree s ( record n1 { right = Just n0 } ) next
-          ... | EQ =  next tree
+          ... | LT =  replaceNode tree s ( record n1 { left = Just n0 } ) 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 -> Maybe (Node a k) -> Maybe (Node a k) ->
@@ -176,7 +176,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 = popStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n1 } ) )
     ...                                | GT = findNode2 s (right n1)
     ...                                | LT = findNode2 s (left n1)
 
--- a/redBlackTreeTest.agda	Wed Jan 10 18:10:03 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Jan 11 11:55:22 2018 +0900
@@ -44,17 +44,26 @@
     $ \t x -> check1 x 2 ≡ True  
 test3 = refl
 
-test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $  \t -> putTree1 t 2 2  $ \t ->
-  root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
-test4 = refl
+-- test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $  \t -> putTree1 t 2 2  $ \t ->
+--   root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
+-- test4 = refl
 
 
-test5 : Maybe (Node ℕ ℕ)
+-- test5 : Maybe (Node ℕ ℕ)
 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 
     $ \t -> putTree1 t 2 2
-    $ \t -> putTree1 t 3 3 
+    -- $ \t -> putTree1 t 3 3 
+    $ \t ->  clearStack (nodeStack t)
+    $ \s -> findNode1 t s (leafNode 3 3) ( root t )
+    $ \t1 s n1 -> replaceNode t1 s n1 
     $ \t -> getRedBlackTree t 3
-    $ \t x -> root t 
+    $ \t x -> SingleLinkedStack.top (stack s)
+    -- $ \t x -> n1
+    -- $ \t x -> root t1
+  where
+     findNode1 : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
+     findNode1 t s n1 Nothing next = next t s n1
+     findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next
 
 -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t ->
 --   putTree1 t 2 2 $ \t -> putTree1 t 3 3 $ \t -> root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )