--- a/RedBlackTree.agda	Tue Jan 09 17:04:34 2018 +0900
+++ b/RedBlackTree.agda	Tue Jan 09 17:26:19 2018 +0900
@@ -164,7 +164,9 @@
     insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
     insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
 
-
+----
+-- find node potition to insert or to delete, the pass will be in the stack
+-- 
 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
@@ -190,7 +192,7 @@
 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 k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)
+...                                | Just n2  = clearStack (nodeStack tree) (\ s -> findNode tree s (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)

--- a/stack.agda	Tue Jan 09 17:04:34 2018 +0900
+++ b/stack.agda	Tue Jan 09 17:26:19 2018 +0900
@@ -28,6 +28,7 @@
     pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
     get  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
     get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
+    clear : stackImpl -> (stackImpl -> t) -> t 
 open StackMethods
 
 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
@@ -44,6 +45,8 @@
   getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
   get2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
   get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  clearStack : (Stack a si -> t) -> t
+  clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
 
 open Stack
 
@@ -115,6 +118,8 @@
     ...              | Nothing = cs stack Nothing Nothing
     ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
 
+clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t
+clearSingleLinkedStack stack next = next (record {top = Nothing})
 
 
 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
@@ -130,6 +135,7 @@
                                  ; pop2 = pop2SingleLinkedStack
                                  ; get  = getSingleLinkedStack
                                  ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
                            }
 
 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)