--- a/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 19:51:14 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 23:15:32 2018 +0900
@@ -49,9 +49,45 @@
 
 open Stack
 
+--
+-- put new node at parent node, and rebuild tree to the top
+--
+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 
 
 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)
+insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
+   where
+    insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allo mutual recursion
+    insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
+    insertCase3 s n0 parent grandParent with left grandParent | right grandParent
+    ... | Nothing | Nothing = {!!}     -- insertCase4
+    ... | Nothing | Just uncle  = {!!} -- insertCase4
+    ... | Just uncle | _  with compare tree ( key uncle ) ( key parent )
+    ...                   | EQ = {!!} -- insertCase4
+    ...                   | _ with color uncle
+    ...                           | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( 
+           record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } )  ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
+    ...                           | Black = {!!} -- insertCase4
+    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 grandParent n0 next
+    ... | Red = insertCase3 s n0 parent grandParent
+    insertCase1 s n0 Nothing Nothing = next tree
+    insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
+    insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
+    insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
+      where
 
 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)
@@ -64,26 +100,21 @@
     ...                                | EQ = next tree s n0 
     ...                                | GT = findNode2 s (right n1)
     ...                                | LT = findNode2 s (left n1)
-      where
-        -- 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)
 
 
-leafNode : {n m : Level } {a k si : Set n} {t : Set m} -> k -> a -> Node a k
+leafNode : {n : Level } {a k : Set n}  -> k -> a -> Node a k
 leafNode k1 value = record {
     key   = k1 ;
     value = value ;
     right = Nothing ;
     left  = Nothing ;
     color = Black 
-    }
+  }
 
 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)
+...                                | Just n2  = findNode tree (nodeStack tree) (leafNode 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)