--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/RedBlackTree.agda	Fri Jan 05 16:39:43 2018 +0900
@@ -0,0 +1,145 @@
+module RedBlackTree where
+
+open import stack
+open import Level
+
+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
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+  putTree : a -> (Tree treeImpl -> t) -> t
+  putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
+  getTree : (Tree treeImpl -> Maybe a -> t) -> t
+  getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+
+open Tree
+
+data Color {n : Level } : Set n where
+  Red   : Color
+  Black : Color
+
+data CompareResult {n : Level } : Set n where
+  LT : CompareResult
+  GT : CompareResult
+  EQ : CompareResult
+
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
+  field
+    key   : k
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
+
+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
+    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 (
+      \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 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 } ) } )   
+        replaceNode1 s (Just grandParent) result with result
+        ... | LT =  replaceNode tree s grandParent ( record parent { left = Just n0 } ) next
+        ... | 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 = {!!}
+
+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 = {!!}
+
+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 = {!!}
+
+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 = {!!}
+
+{-# 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 )
+   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
+          -- 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 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
+    ... | Just uncle | _  with compare tree ( key uncle ) ( key parent )
+    ...                   | EQ =  insertCase4 tree s n0 parent grandParent next
+    ...                   | _ with color uncle
+    ...                           | 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 s n0 parent grandParent with color parent
+    ... | Black = replaceNode tree s grandParent n0 next
+    ... | Red = insertCase3 s n0 parent grandParent
+    insertCase1 s n0 Nothing Nothing = next tree
+    insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
+    insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
+    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)
+  where
+    findNode2 : Stack (Node a k) si -> (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 s n1 with (compare tree (key n0) (key n1))
+    ...                                | EQ = next tree s n0 
+    ...                                | GT = findNode2 s (right n1)
+    ...                                | LT = findNode2 s (left n1)
+
+
+leafNode : {n : Level } {a k : Set n}  -> k -> a -> Node a k
+leafNode k1 value = record {
+    key   = k1 ;
+    value = value ;
+    right = Nothing ;
+    left  = Nothing ;
+    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)
+...                                | 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)
+  where
+    checkNode : Maybe (Node a k) -> t
+    checkNode Nothing = cs tree Nothing
+    checkNode (Just n) = search n
+      where
+        search : Node a k -> t
+        search n with compare tree k1 (key n)
+        search n | LT = checkNode (left n)
+        search n | GT = checkNode (right n)
+        search n | EQ = cs tree (Just n)