--- a/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 14:42:21 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 15:10:24 2018 +0900
@@ -24,30 +24,44 @@
   Red   : Color
   Black : Color
 
-record Node (a : Set) : Set where
+data CompareResult {n : Level } : Set n where
+  LT : CompareResult
+  GT : CompareResult
+  EQ : CompareResult
+
+record Node (a k : Set) : Set where
   field
-    node  : Element a
+    key   : k
+    value : a
     right : Maybe (Node a)
     left  : Maybe (Node a)
     color : Color
+open Node
 
-record RedBlackTree (a si : Set) : Set where
+record RedBlackTree (a  k si : Set) : Set where
   field
-    root : Maybe (Node a)
+    root : Maybe (Node a k )
     stack : Stack si
+    compare : k -> k -> CompareResult
 
 open RedBlackTree
 
-insertNode : ?
-insertNode tree datum next = get2 (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next)
+open Stack
+
+insertCase3 : ?
+insertCase3 = ? -- tree datum parent grandparent next 
 
-putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
-putRedBlackTree tree datum next with (root tree)
-...                                | Nothing = insertNode tree datum next
-...                                | Just n  = findNode tree datum n (\ tree1 -> insertNode tree1 datum next)
+insertCase2 : {n m : Level } {t : Set m } {a : Set n} -> RedBlackTree ? ? -> a (Node a) (Node a) ? -> t
+insertCase2 tree datum parent grandparent next with (color parent)
+...                                | Red = insertCase3 tree datum parent grandparent next
+...                                | Black = next (record { root = ?; stack = createSingleLinkedStack })
 
-findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
-findNode tree datum n next = pushStack (stack tree) n (\ s -> findNode1 (record tree {stack = s }) datum n next)
+insertCase1 : {n m : Level } {t : Set m } {a : Set n} -> RedBlackTree ? ? -> a (Maybe (Node a) ) (Node a) ? -> t
+insertCase1 tree datum Nothing grandparent next = next (record { root = ?; stack = createSingleLinkedStack })
+insertCase1 tree datum (Just parent) grandparent next = insertCase2 tree datum parent grandparent next
+
+insertNode : ?
+insertNode tree datum next = get2Stack (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 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)
@@ -57,19 +71,18 @@
   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 : ?
     findNode3 nothing tree next = next tree
     findNode3 (just n) tree next = 
            popStack (tree stack) (\s d -> findNode3 d (record { root = record n {right = ? } }))
 
-
-insertCase1 tree datum nothing grandparent next = next (record { root = ?; stack = createSingleLinkedStack })
-insertCase1 tree datum (just parent) grandparent next = insertCase2 tree datum parent grandparent next
+findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
+findNode tree datum n next = pushStack (stack tree) n (\ s -> findNode1 (record tree {stack = s }) datum n next)
 
-insertCase2 tree datum parent grandparent next with (color parent)
-...                                | Red = insertCase3 tree datum parent grandparent next
-...                                | Black = next (record { root = ?; stack = createSingleLinkedStack })
-
-insertCase3 tree datum parent grandparent next 
+putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
+putRedBlackTree tree datum next with (root tree)
+...                                | Nothing = insertNode tree datum next
+...                                | Just n  = findNode tree datum n (\ tree1 -> insertNode tree1 datum next)
 
 getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
 getRedBlackTree tree cs with (root tree)