Mercurial > hg > Gears > GearsAgda

changeset 538:5c001e8ba0d5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add redBlackTreeTest.agda test5,test51. but not work
author ryokka
date Wed, 10 Jan 2018 17:38:24 +0900
parents fffeaf0b0024
children 39d465c20e5a
files RedBlackTree.agda redBlackTreeTest.agda stackTest.agda
diffstat 3 files changed, 42 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/RedBlackTree.agda	Wed Jan 10 15:44:13 2018 +0900
+++ b/RedBlackTree.agda	Wed Jan 10 17:38:24 2018 +0900
@@ -52,18 +52,16 @@
 -- put new node at parent node, and rebuild tree to the top
 --
 {-# TERMINATING #-}   -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
-replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s (
-      \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 (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
+replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si ->  Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+replaceNode {n} {m} {t} {a} {k} {si} tree s n0 next = popStack s (
+      \s parent -> replaceNode1 s parent)
+        where
+          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
+          ... | GT =  replaceNode tree s ( record n1 { 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 -> Maybe (Node a k) -> Maybe (Node a k) ->
@@ -160,11 +158,11 @@
     ...                           | 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 parent n0 next
+    ... | Black = replaceNode tree s 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) Nothing = replaceNode tree s (colorNode n0 Black) next
     insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
 
 ----
@@ -205,7 +203,7 @@
     checkNode (Just n) = search n
       where
         search : Node a k -> t
-        search n with compare tree k1 (key n)
+        search n with compare tree (key n) k1
         search n | LT = checkNode (left n)
         search n | GT = checkNode (right n)
         search n | EQ = cs tree (Just n)
--- a/redBlackTreeTest.agda	Wed Jan 10 15:44:13 2018 +0900
+++ b/redBlackTreeTest.agda	Wed Jan 10 17:38:24 2018 +0900
@@ -5,9 +5,6 @@
 open import Level hiding (zero)
 
 open import Data.Nat
-open import Relation.Binary.PropositionalEquality
-open import Relation.Binary.Core
-
 
 open Tree
 open Node
@@ -19,7 +16,7 @@
 putTree1 : {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
 putTree1 {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
 ...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
-...                                | Just n2  = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n2 n1 next))
+...                                | Just n2  = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next))
 
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Core
@@ -41,12 +38,25 @@
     \t x -> check1 x 1 ≡ True   )))
 test2 = refl
 
--- test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 
---     $ \t -> putTree1 t 2 2 
---     $ \t -> getRedBlackTree t 2 
---     $ \t x -> check1 x 2 ≡ True  
--- test3 = {!!}
+test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 
+    $ \t -> putTree1 t 2 2 
+    $ \t -> getRedBlackTree t 2 
+    $ \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 = Nothing ; right = Just ( record { key = 2 ; value = 2 } ) } )
+  root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
 test4 = refl
+
+
+
+-- test5 : Maybe (Node ℕ ℕ)
+-- test5 = putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 
+--     $ \t -> putTree1 t 2 2
+--     $ \t -> putTree1 t 3 3 
+--     $ \t -> getRedBlackTree t 3
+--     $ \t x -> root t 
+
+-- 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} )
+-- test51 = refl
--- a/stackTest.agda	Wed Jan 10 15:44:13 2018 +0900
+++ b/stackTest.agda	Wed Jan 10 17:38:24 2018 +0900
@@ -61,6 +61,15 @@
 testStack05 : testStack04 ≡ True
 testStack05 = refl
 
+testStack06 : {m : Level } -> Maybe (Element ℕ)
+testStack06 = pushStack createSingleLinkedStack 1 (
+   \s -> pushStack s 2 (\s -> top (stack s)))
+
+testStack07 : {m : Level } -> Maybe (Element ℕ)
+testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (
+   \s -> pushSingleLinkedStack s 2 (\s -> top s))
+
+
 ------
 --
 -- proof of properties with indefinite state of stack