# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1515078078 -32400
# Node ID b118ed3ba5836d0e766442944d4df7fb1a0b0e99
# Parent  0a723e418b2ace2bee686457e97d255b76aaedc9
fix agda

diff -r 0a723e418b2a -r b118ed3ba583 src/parallel_execution/RedBlackTree.agda
--- a/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 23:43:18 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Fri Jan 05 00:01:18 2018 +0900
@@ -42,7 +42,7 @@
 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} (Node a k) {t} si
+    nodeStack : Stack {n} {m} (Node a k) {t} ( SingleLinkedStack (Node a k ) )
     compare : k -> k -> CompareResult {n}
 
 open RedBlackTree
@@ -126,13 +126,13 @@
     color = Black 
   }
 
-putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
+putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree a k (SingleLinkedStack (Node a k)) -> k -> a -> (RedBlackTree a k (SingleLinkedStack (Node a k)) -> t) -> t
+putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
 ...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
 ...                                | Just n2  = findNode tree (nodeStack tree) (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)
 
-getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t
-getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
+getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k (SingleLinkedStack (Node a k)) -> k -> (RedBlackTree a k (SingleLinkedStack (Node a k)) -> (Maybe (Node a k)) -> t) -> t
+getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
   where
     checkNode : Maybe (Node a k) -> t
     checkNode Nothing = cs tree Nothing