Mercurial > hg > Gears > GearsAgda

changeset 551:8bc39f95c961

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix findNode
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Jan 2018 18:28:25 +0900
parents 2476f7123dc3
children 5f4c5a663219
files RedBlackTree.agda redBlackTreeTest.agda
diffstat 2 files changed, 22 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/RedBlackTree.agda	Wed Jan 17 17:31:41 2018 +0900
+++ b/RedBlackTree.agda	Wed Jan 17 18:28:25 2018 +0900
@@ -59,7 +59,7 @@
           replaceNode1 : SingleLinkedStack (Node a k) -> 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)
-          ... | EQ =  next tree
+          ... | EQ =  replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next
           ... | GT =  replaceNode tree s ( record n1 { left = Just n0 } ) next
           ... | LT =  replaceNode tree s ( record n1 { right = Just n0 } ) next
 
@@ -176,7 +176,7 @@
     findNode2 s (Just n) = findNode tree s n0 n next
     findNode1 : SingleLinkedStack (Node a k) -> (Node a k)  -> t
     findNode1 s n1 with (compare tree (key n0) (key n1))
-    ...                                | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n1 } ) )
+    ...                                | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n0 } ) )
     ...                                | GT = findNode2 s (right n1)
     ...                                | LT = findNode2 s (left n1)
 
@@ -197,7 +197,7 @@
 
 getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> (RedBlackTree {n} {m} {t} a k -> (Maybe (Node a k)) -> t) -> t
 getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
-  where
+  module GetRedBlackTree where                     -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html
     search : Node a k -> t
     checkNode : Maybe (Node a k) -> t
     checkNode Nothing = cs tree Nothing
--- a/redBlackTreeTest.agda	Wed Jan 17 17:31:41 2018 +0900
+++ b/redBlackTreeTest.agda	Wed Jan 17 18:28:25 2018 +0900
@@ -153,11 +153,11 @@
 putTest1Lemma3 : (k : ℕ)  -> compareℕ k k ≡ EQ
 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  ) 
 
-compareLemma1 : (x  y : ℕ)  -> compare2 x y ≡ EQ -> x  ≡ y
-compareLemma1 zero zero refl = refl
-compareLemma1 zero (suc _) () 
-compareLemma1 (suc _) zero () 
-compareLemma1 (suc x) (suc y) eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 x y ( trans lemma2 eq ) )
+compareLemma1 : {x  y : ℕ}  -> compare2 x y ≡ EQ -> x  ≡ y
+compareLemma1 {zero} {zero} refl = refl
+compareLemma1 {zero} {suc _} () 
+compareLemma1 {suc _} {zero} () 
+compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
    where
       lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
       lemma2 = refl
@@ -168,7 +168,20 @@
          -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
          (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x  ≡ True)) 
 putTest1 n k x with n
-...  | Just n1 = {!!}
+...  | Just n1 = lemma2
+   where
+     lemma2 : putTree1 (record { root = Just n1 ; nodeStack = record { top = Nothing } ; compare = compare2 }) k x (λ t →
+         GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
+     lemma2 with compare2 k (key n1)
+     ... |  EQ = {!!}
+        where 
+           lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
+               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
+               } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y  } ) k ( \ t x1 -> check2 x1 x  ≡ True)
+           lemma3 with compare2 x x | putTest1Lemma2 x 
+           ... | EQ | refl  = {!!}
+     ... |  GT = {!!}
+     ... |  LT = {!!}
 ...  | Nothing =  lemma1  
    where 
      lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {