# HG changeset patch
# User ryokka
# Date 1515749405 -32400
# Node ID b180dc78abcf6eb0d2ada7205d6516bf6c1c71bd
# Parent  4f692df9b3db78367e7aac583d6d9e9dead87966
add someTest

diff -r 4f692df9b3db -r b180dc78abcf RedBlackTree.agda
--- a/RedBlackTree.agda	Thu Jan 11 18:54:56 2018 +0900
+++ b/RedBlackTree.agda	Fri Jan 12 18:30:05 2018 +0900
@@ -209,15 +209,17 @@
 
 open import Data.Nat hiding (compare)
 
+compareℕ :  ℕ → ℕ → CompareResult {Level.zero}
+compareℕ x y with Data.Nat.compare x y
+... | less _ _ = LT
+... | equal _ = EQ
+... | greater _ _ = GT
+
+
 createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
 createEmptyRedBlackTreeℕ  {m} a {t} = record {
         root = Nothing
      ;  nodeStack = emptySingleLinkedStack
-     ;  compare = compare1
-   } where
-       compare1 :  ℕ → ℕ → CompareResult {Level.zero}
-       compare1 x y with Data.Nat.compare x y
-       ... | less _ _ = LT
-       ... | equal _ = EQ
-       ... | greater _ _ = GT
-
+     ;  compare = compareℕ
+   }
+ 
diff -r 4f692df9b3db -r b180dc78abcf redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Thu Jan 11 18:54:56 2018 +0900
+++ b/redBlackTreeTest.agda	Fri Jan 12 18:30:05 2018 +0900
@@ -38,13 +38,18 @@
     \t x -> check1 x 1 ≡ True   )))
 test2 = refl
 
+open ≡-Reasoning
 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 
     $ \t -> putTree1 t 2 2
     $ \t -> putTree1 t 3 3
     $ \t -> putTree1 t 4 4    
-    $ \t -> getRedBlackTree t 4
-    $ \t x -> check1 x 4 ≡ True  
-test3 = refl
+    $ \t -> getRedBlackTree t 1
+    $ \t x -> check1 x 1 ≡ True  
+test3 = begin
+    check1 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
+  ≡⟨ refl ⟩
+    True
+  ∎
 
 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 
     $ \t -> putTree1 t 2 2
@@ -103,3 +108,19 @@
     $ \t -> putRedBlackTree t 3 3
     $ \t -> getRedBlackTree t 2
     $ \t x -> root t
+
+
+redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
+redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareℕ }
+
+putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
+         -> (k : ℕ) (x : ℕ) 
+         -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
+         (\ t -> getRedBlackTree t k (\ t x1 -> check1 x1 x  ≡ True)) 
+putTest1 n k x = {!!}
+
+-- begin
+--     ?
+--   ≡⟨ ? ⟩
+--     True
+--   ∎