# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1515112264 -32400
# Node ID e3cd5e3a01b89d1f36ad84147fce56dc97058916
# Parent  b118ed3ba5836d0e766442944d4df7fb1a0b0e99
add stack implement

diff -r b118ed3ba583 -r e3cd5e3a01b8 src/parallel_execution/RedBlackTree.agda
--- a/src/parallel_execution/RedBlackTree.agda	Fri Jan 05 00:01:18 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Fri Jan 05 09:31:04 2018 +0900
@@ -39,25 +39,29 @@
     color : Color {n}
 open Node
 
-record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
+Stak : {n m : Level }  (a k : Set n) (t : Set m ) -> Set (m ⊔ n)
+Stak {n} {m} a k t = Stack {n} {m} (Node a k) {t} (SingleLinkedStack (Node a k))
+open Stack
+
+record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where
   field
     root : Maybe (Node a k)
-    nodeStack : Stack {n} {m} (Node a k) {t} ( SingleLinkedStack (Node a k ) )
+    nodeStack :  Stak a k t 
     compare : k -> k -> CompareResult {n}
 
 open RedBlackTree
 
-open Stack
+
 
 --
 -- put new node at parent node, and rebuild tree to the top
 --
 {-# TERMINATING #-}   -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
-replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s (
+replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k  -> Stak a k t -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k  -> t) -> t
+replaceNode {n} {m} {t} {a} {k} tree s parent n0 next = popStack s (
       \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
   where
-        replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t
+        replaceNode1 : Stak a k t -> Maybe ( Node a k ) -> CompareResult -> t
         replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } )   
         replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
         replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
@@ -66,25 +70,25 @@
         ... | GT =  replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
         ... | EQ =  next tree 
 
-rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
+rotateRight : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+rotateRight {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = {!!}
 
-rotateLeft : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
+rotateLeft : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+rotateLeft {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = {!!}
 
-insertCase5 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
+insertCase5 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+insertCase5 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = {!!}
 
-insertCase4 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
+insertCase4 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+insertCase4 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = {!!}
 
 {-# TERMINATING #-}
-insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
+insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+insertNode {n} {m} {t} {a} {k}  tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
    where
-    insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allow mutual recursion
+    insertCase1 : Stack (Node a k) (SingleLinkedStack (Node a k)) -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allow mutual recursion
           -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
-    insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
+    insertCase3 : Stak a k t -> Node a k -> Node a k -> Node a k -> t
     insertCase3 s n0 parent grandParent with left grandParent | right grandParent
     ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
     ... | Nothing | Just uncle  = insertCase4 tree s n0 parent grandParent next
@@ -94,7 +98,7 @@
     ...                           | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( 
            record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } )  ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
     ...                           | Black = insertCase4 tree s n0 parent grandParent next
-    insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
+    insertCase2 : Stak a k t -> Node a k -> Node a k -> Node a k -> t
     insertCase2 s n0 parent grandParent with color parent
     ... | Black = replaceNode tree s grandParent n0 next
     ... | Red = insertCase3 s n0 parent grandParent
@@ -104,13 +108,13 @@
     insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
       where
 
-findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
-findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
+findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> t) -> t
+findNode {n} {m} {a} {k}  {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
   where
-    findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
+    findNode2 : Stak a k t -> (Maybe (Node a k)) -> t
     findNode2 s Nothing = next tree s n0
     findNode2 s (Just n) = findNode tree s n0 n next
-    findNode1 : Stack (Node a k) si -> (Node a k)  -> t
+    findNode1 : Stak a k t -> (Node a k)  -> t
     findNode1 s n1 with (compare tree (key n0) (key n1))
     ...                                | EQ = next tree s n0 
     ...                                | GT = findNode2 s (right n1)
@@ -126,12 +130,12 @@
     color = Black 
   }
 
-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 : Level } {a k : Set n} {t : Set m} -> RedBlackTree a k  -> k -> a -> (RedBlackTree 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 : 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 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k  -> k -> (RedBlackTree 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