--- a/src/parallel_execution/RedBlackTree.agda	Wed Jan 03 18:22:38 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 14:42:21 2018 +0900
@@ -1,23 +1,25 @@
 module RedBlackTree where
 
 open import stack
+open import Level
 
-record Tree {a t : Set} (treeImpl : Set) : Set  where
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
+  field
+    putImpl : treeImpl -> a -> (treeImpl -> t) -> t
+    getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
   field
     tree : treeImpl
-    putImpl : treeImpl -> a -> (treeImpl -> t) -> t
-    getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
+    treeMethods : TreeMethods {a} {t}
+  putTree : a -> (Tree -> t) -> t
+  putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
+  getTree : (Tree -> Maybe a -> t) -> t
+  getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
 
 open Tree
 
-
-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
   Black : Color
@@ -29,10 +31,10 @@
     left  : Maybe (Node a)
     color : Color
 
-record RedBlackTree (a : Set) : Set where
+record RedBlackTree (a si : Set) : Set where
   field
     root : Maybe (Node a)
-    stack : Stack
+    stack : Stack si
 
 open RedBlackTree
 

--- a/src/parallel_execution/stack.agda	Wed Jan 03 18:22:38 2018 +0900
+++ b/src/parallel_execution/stack.agda	Thu Jan 04 14:42:21 2018 +0900
@@ -95,7 +95,7 @@
     pop2SingleLinkedStack' : {n m : Level } {t : Set m }  -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
     pop2SingleLinkedStack' stack cs with (next d)
     ...              | Nothing = cs stack Nothing Nothing
-    ...              | Just d1 = cs (record {top = (next d)}) (Just (datum d)) (Just (datum d1))
+    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
     
 
 getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t