--- a/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 18:10:15 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 19:45:32 2018 +0900
@@ -42,55 +42,58 @@
 record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
   field
     root : Maybe (Node a k)
-    nodeStack : Stack {n} {m} {{!!}} {t} si
+    nodeStack : Stack {n} {m} (Node a k) {t} si
     compare : k -> k -> CompareResult {n}
 
 open RedBlackTree
 
 open Stack
 
-insertCase3 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase3 = {!!} -- tree datum parent grandparent next 
 
-insertCase2 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase2 tree datum parent grandparent next with (color parent)
-...                                | Red = insertCase3 tree datum parent grandparent next
-...                                | Black = next (record { root = {!!}; nodeStack = {!!}})
-
-insertCase1 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (Maybe (Node a k) ) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase1 tree datum Nothing grandparent next = next (record { root = {!!}; nodeStack = {!!} })
-insertCase1 tree datum (Just parent) grandparent next = insertCase2 tree datum parent grandparent next
-
-insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertNode tree datum next = get2Stack (nodeStack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; nodeStack = s }) datum d1 d2 next)
+insertNode : {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
+insertNode tree s datum next = get2Stack s (\ s d1 d2 -> {!!} tree s datum d1 d2 next)
 
-findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-findNode {n} {m} {a} {k} {si} {t} tree n0 n1 next = pushStack (nodeStack tree) n1 (\ s -> findNode1 (record tree {nodeStack = s }) n0 n1 next)
+findNode : {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) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
+findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
   where
-    findNode1 : RedBlackTree {n} {m} {t} a k si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-    findNode1 tree n0 n1 next with (compare tree (key n0) (key n1))
-    ...                                | EQ = popStack (nodeStack tree) (\s d -> {!!} d (record tree { root = Just (record n {node = datum}); stack = s }) next)
-    ...                                | GT = {!!} tree datum (right n) next
-    ...                                | LT = findNode2 tree {!!} (left n1) next
+    findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
+    findNode2 s Nothing = next tree s n0
+    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 
+    ...                                | GT = findNode2 s (right n1)
+    ...                                | LT = findNode2 s (left n1)
       where
-        findNode2 : RedBlackTree {n} {m} {t} a k si -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-        findNode2 tree datum Nothing next = insertNode tree {!!} next
-        findNode2 tree datum (Just n) next = findNode (record tree {root = Just n}) datum n next
-        findNode3 : RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-        findNode3 tree nothing next = next tree
-        findNode3 tree (Just n) next = 
-                  popStack (nodeStack tree) (\s d -> findNode3 tree d  {!!} )
+        -- findNode3 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
+        -- findNode3 s nothing = next tree s n0
+        -- findNode3 s (Just n) = 
+        --           popStack (nodeStack tree) (\s d -> findNode3 s d)
 
 
-putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-putRedBlackTree tree datum next with (root tree)
-...                                | Nothing = insertNode tree datum next
-...                                | Just n  = findNode tree {!!} n (\ tree1 -> insertNode tree1 datum next)
+leafNode : {n m : Level } {a k si : Set n} {t : Set m} -> k -> a -> Node a k
+leafNode k1 value = record {
+    key   = k1 ;
+    value = value ;
+    right = Nothing ;
+    left  = Nothing ;
+    color = Black 
+    }
 
-getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> (Code : RedBlackTree {n} {m} {t} a k si -> (Maybe a) -> t) -> t
-getRedBlackTree tree cs with (root tree)
-...                                | Nothing = cs tree  Nothing
-...                                | Just d  = cs stack1 (Just data1)
+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
+putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = findNode tree (nodeStack tree) (leafNode {n} {m} {a} {k} {si} {t} k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)
+
+getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t
+getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
   where
-    data1  = {!!} 
-    stack1 = {!!}
+    checkNode : Maybe (Node a k) -> t
+    checkNode Nothing = cs tree Nothing
+    checkNode (Just n) = search n
+      where
+        search : Node a k -> t
+        search n with compare tree k1 (key n)
+        search n | LT = checkNode (left n)
+        search n | GT = checkNode (right n)
+        search n | EQ = cs tree (Just n)