--- a/src/parallel_execution/RedBlackTree.agda	Fri Oct 06 19:48:42 2017 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Sat Oct 07 18:22:31 2017 +0900
@@ -5,8 +5,16 @@
 record Tree {a t : Set} (treeImpl : Set) : Set  where
   field
     tree : treeImpl
-    put : treeImpl -> a -> (treeImpl -> t) -> t
-    get  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
+    putImpl : treeImpl -> a -> (treeImpl -> t) -> t
+    getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
+
+putTree : {a t : Set} -> Tree -> a -> (Tree -> t) -> t
+putTree {a} {t} t0 d next = (putImpl t0) (tree t0) d (\t1 -> next (record t0 {tree = t1;} ))
+
+
+getTree : {a t : Set} -> Tree -> (Tree -> t) -> t
+getTree {a} {t} t0  next = (getImpl t0) (tree t0) (\t1 -> next t0)
+
 
 data Color : Set where
   Red   : Color
@@ -32,16 +40,16 @@
 ...                                | Just n  = findNode tree datum n (\ tree1 -> insertNode tree1 datum next)
 
 findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
-findNode tree datum n next = push (stack tree) n (\ s -> findNode1 (record { root = root tree; stack = s }) datum n next)
+findNode tree datum n next = push (stack tree) n (\ s -> findNode1 (record tree {stack = s }) datum n next)
 
 findNode1 : {Data t : Set} -> RedBlackTree Data -> Data -> Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
 findNode1 tree datum n next with (compare datum n)
-...                                | EQ = next (record { root = root tree; stack = createSingleLinkedStack })
+...                                | EQ = next (record tree { root = just n })
 ...                                | GT = findNode2 tree datum (right n) next
 ...                                | LT = findNode2 tree datum (left n) next
   where
     findNode2 tree datum nothing next = insertNode tree datum next
-    findNode2 tree datum (just n) next = findNode tree datum n next
+    findNode2 tree datum (just n) next = findNode (record tree {root = just n}) datum n next
 
 insertNode tree datum next = get2 (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next)
 

--- a/src/parallel_execution/stack.agda	Fri Oct 06 19:48:42 2017 +0900
+++ b/src/parallel_execution/stack.agda	Sat Oct 07 18:22:31 2017 +0900
@@ -20,6 +20,13 @@
     push : stackImpl -> a -> (stackImpl -> t) -> t
     pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
 
+pushStack : {a t : Set} -> Stack -> a -> (Stack -> t) -> t
+pushStack {a} {t} s0 d next = (stackImpl s0) (stack s0) d (\s1 -> next (record s0 {stack = s1;} ))
+
+popStack : {a t : Set} -> Stack -> (Stack -> t) -> t
+popStack {a} {t} s0  next = (stackImpl s0) (stack s0) (\s1 -> next s0)
+
+
 data Element (a : Set) : Set where
   cons : a -> Maybe (Element a) -> Element a