# HG changeset patch
# User ryokka
# Date 1507370422 -32400
# Node ID ff4ab9add9596af0edee07eb0cff97897c0da739
# Parent  07ccd411ad70a03ad4c52c3f5078ba107aa81199
fix findNode

diff -r 07ccd411ad70 -r ff4ab9add959 src/parallel_execution/RedBlackTree.agda
--- a/src/parallel_execution/RedBlackTree.agda	Sat Oct 07 18:22:31 2017 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Sat Oct 07 19:00:22 2017 +0900
@@ -44,12 +44,15 @@
 
 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 tree { root = just n })
+...                                | EQ = popStack (tree stack) (\s d -> findNode3 d (record tree { root = just (record n {node = datum}); stack = s }) next)
 ...                                | 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 (record tree {root = just n}) datum n next
+    findNode3 nothing tree next = next tree
+    findNode3 (just n) tree next = 
+           popStack (tree stack) (\s d -> findNode3 d (record { root = record n {right = } })
 
 insertNode tree datum next = get2 (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next)