--- a/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 17:46:59 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 18:10:15 2018 +0900
@@ -36,58 +36,58 @@
     value : a
     right : Maybe (Node a k)
     left  : Maybe (Node a k)
-    color : Color
+    color : Color {n}
 open Node
 
-record RedBlackTree {n m : Level } (a  k si : Set n) : Set (m Level.⊔ n) where
+record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
   field
-    root : Maybe (Node a k )
-    nodeStack : Stack {n} {m} si
-    compare : k -> k -> CompareResult
+    root : Maybe (Node a k)
+    nodeStack : Stack {n} {m} {{!!}} {t} si
+    compare : k -> k -> CompareResult {n}
 
 open RedBlackTree
 
 open Stack
 
-insertCase3 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {!!} {!!} {!!} -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {!!} {!!} {!!} -> t) -> t
+insertCase3 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
 insertCase3 = {!!} -- tree datum parent grandparent next 
 
-insertCase2 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {!!} {!!} {!!} -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {!!} {!!} {!!} -> t) -> t
+insertCase2 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
 insertCase2 tree datum parent grandparent next with (color parent)
 ...                                | Red = insertCase3 tree datum parent grandparent next
-...                                | Black = next (record { root = {!!}; nodeStack = createSingleLinkedStack })
+...                                | Black = next (record { root = {!!}; nodeStack = {!!}})
 
-insertCase1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {!!} {!!} {!!} -> a -> (Maybe (Node a k) ) -> (Maybe (Node a k)) -> (RedBlackTree {!!} {!!} {!!} -> t) -> t
-insertCase1 tree datum Nothing grandparent next = next (record { root = {!!}; nodeStack = createSingleLinkedStack })
+insertCase1 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (Maybe (Node a k) ) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+insertCase1 tree datum Nothing grandparent next = next (record { root = {!!}; nodeStack = {!!} })
 insertCase1 tree datum (Just parent) grandparent next = insertCase2 tree datum parent grandparent next
 
-insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {!!} {!!} {!!} -> a -> (RedBlackTree {!!} {!!} {!!} -> t) -> t
+insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
 insertNode tree datum next = get2Stack (nodeStack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; nodeStack = s }) datum d1 d2 next)
 
-findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree a k {!!} -> (Node a k) -> (Node a k) -> (RedBlackTree a k {!!} -> t) -> t
-findNode {n} {m} {a} {k} {t} tree n1 next = pushStack (nodeStack tree) n1 (\ s -> findNode1 (record tree {nodeStack = s }) n1 next)
+findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+findNode {n} {m} {a} {k} {si} {t} tree n0 n1 next = pushStack (nodeStack tree) n1 (\ s -> findNode1 (record tree {nodeStack = s }) n0 n1 next)
   where
-    findNode1 : RedBlackTree a k {!!} -> (Node a k) -> (Node a k) -> (RedBlackTree a k {!!} -> t) -> t
+    findNode1 : RedBlackTree {n} {m} {t} a k si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
     findNode1 tree n0 n1 next with (compare tree (key n0) (key n1))
     ...                                | EQ = popStack (nodeStack tree) (\s d -> {!!} d (record tree { root = Just (record n {node = datum}); stack = s }) next)
     ...                                | GT = {!!} tree datum (right n) next
     ...                                | LT = findNode2 tree {!!} (left n1) next
       where
-        findNode2 : RedBlackTree a k {!!} -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree a k {!!} -> t) -> t
-        findNode2 tree datum Nothing next = insertNode tree datum next
+        findNode2 : RedBlackTree {n} {m} {t} a k si -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+        findNode2 tree datum Nothing next = insertNode tree {!!} next
         findNode2 tree datum (Just n) next = findNode (record tree {root = Just n}) datum n next
-        findNode3 : RedBlackTree a k {!!} -> (Maybe (Node a k)) -> (RedBlackTree a k {!!} -> t) -> t
+        findNode3 : RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
         findNode3 tree nothing next = next tree
         findNode3 tree (Just n) next = 
                   popStack (nodeStack tree) (\s d -> findNode3 tree d  {!!} )
 
 
-putRedBlackTree : {a t : Set} -> RedBlackTree {!!} {!!} {!!} -> a -> (RedBlackTree {!!} {!!} {!!} -> t) -> t
+putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
 putRedBlackTree tree datum next with (root tree)
 ...                                | Nothing = insertNode tree datum next
 ...                                | Just n  = findNode tree {!!} n (\ tree1 -> insertNode tree1 datum next)
 
-getRedBlackTree : {a t : Set} -> RedBlackTree {!!} {!!} {!!} -> (Code : RedBlackTree {!!} {!!} {!!} -> (Maybe a) -> t) -> t
+getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> (Code : RedBlackTree {n} {m} {t} a k si -> (Maybe a) -> t) -> t
 getRedBlackTree tree cs with (root tree)
 ...                                | Nothing = cs tree  Nothing
 ...                                | Just d  = cs stack1 (Just data1)