# HG changeset patch
# User mir3636
# Date 1507193526 -32400
# Node ID 24c98ca207f4778cec39a1e72507119545ecb52c
# Parent  6f873aad1b067fa9cc4f4a0bd9348a229ffb795b
add RedBlackTree.agda

diff -r 6f873aad1b06 -r 24c98ca207f4 src/parallel_execution/RedBlackTree.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Oct 05 17:52:06 2017 +0900
@@ -0,0 +1,30 @@
+module RedBlackTree where
+
+open import stack
+
+record Tree {a t : Set} (treeImpl : Set) : Set  where
+  field
+    tree : treeImpl
+    put : treeImpl -> a -> (treeImpl -> t) -> t
+    get  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
+
+record RedBlackTree (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+    stack : Stack
+open RedBlackTree
+
+putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
+putRedBlackTree stack datum next = next newtree
+  where
+    element = cons datum (top stack)
+    newtree  = record {top = Just element}
+
+getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
+getRedBlackTree tree cs with (top tree)
+...                                | Nothing = cs tree  Nothing
+...                                | Just d  = cs stack1 (Just data1)
+  where
+    data1  = datum d
+    stack1 = record { top = (next d) }
+