# HG changeset patch
# User ryokka
# Date 1515660783 -32400
# Node ID 1595dd84fc3ea0edec39c4e7a826f5a83a031f3c
# Parent  ee65e69c9b620fec35f481899693be44c274758f
fix use SingleLinkedStack

diff -r ee65e69c9b62 -r 1595dd84fc3e RedBlackTree.agda
--- a/RedBlackTree.agda	Thu Jan 11 17:38:13 2018 +0900
+++ b/RedBlackTree.agda	Thu Jan 11 17:53:03 2018 +0900
@@ -38,25 +38,25 @@
     color : Color {n}
 open Node
 
-record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
+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} si
+    nodeStack : SingleLinkedStack  (Node a k)
     compare : k -> k -> CompareResult {n}
 
 open RedBlackTree
 
-open Stack
+open SingleLinkedStack
 
 --
 -- 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 -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-replaceNode {n} {m} {t} {a} {k} {si} tree s n0 next = popStack s (
+replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) ->  Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s (
       \s parent -> replaceNode1 s parent)
         where
-          replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> t 
+          replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t 
           replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } )
           replaceNode1 s (Just n1) with compare tree (key n1) (key n0)
           ... | EQ =  next tree
@@ -64,13 +64,13 @@
           ... | LT =  replaceNode tree s ( record n1 { right = Just n0 } ) next
 
 
-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 -> Maybe (Node a k) -> Maybe (Node a k) ->
-  (RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
-rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext = getStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext)
+rotateRight : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) ->
+  (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
+rotateRight {n} {m} {t} {a} {k}  tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext)
   where
-        rotateRight1 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> 
-          (RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
-        rotateRight1 {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext with n0
+        rotateRight1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k)  -> Maybe (Node a k) -> Maybe (Node a k) -> 
+          (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k)  -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
+        rotateRight1 {n} {m} {t} {a} {k}  tree s n0 parent rotateNext with n0
         ... | Nothing  = rotateNext tree s Nothing n0 
         ... | Just n1 with parent
         ...           | Nothing = rotateNext tree s (Just n1 ) n0
@@ -81,13 +81,13 @@
         ...                                    | _ = rotateNext tree s (Just n1) parent 
 
 
-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 -> Maybe (Node a k) -> Maybe (Node a k) ->
-  (RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) ->  t) -> t
-rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext = getStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext)
+rotateLeft : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) ->
+  (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) ->  t) -> t
+rotateLeft {n} {m} {t} {a} {k}  tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext)
   where
-        rotateLeft1 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> 
-          (RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
-        rotateLeft1 {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext with n0
+        rotateLeft1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) -> 
+          (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
+        rotateLeft1 {n} {m} {t} {a} {k}  tree s n0 parent rotateNext with n0
         ... | Nothing  = rotateNext tree s Nothing n0 
         ... | Just n1 with parent
         ...           | Nothing = rotateNext tree s (Just n1) Nothing 
@@ -98,11 +98,11 @@
         ...                                    | _ = rotateNext tree s (Just n1) parent 
 
 {-# TERMINATING #-}
-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 -> Maybe (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 = pop2Stack s (\ s parent grandParent -> insertCase51 tree s n0 parent grandParent next)
+insertCase5 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (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 = pop2SingleLinkedStack s (\ s parent grandParent -> insertCase51 tree s n0 parent grandParent next)
   where
-    insertCase51 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-    insertCase51 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with n0
+    insertCase51 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+    insertCase51 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next with n0
     ...     | Nothing = next tree
     ...     | Just n1  with  parent | grandParent
     ...                 | Nothing | _  = next tree
@@ -117,23 +117,23 @@
     ...     | _ | _ = rotateLeft tree s n0 parent 
                  (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 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 -> SingleLinkedStack (Node a k) -> 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
        with  (right parent) | (left grandParent)
 ...    | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next
 ...    | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next       
 ...    | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent)
-...                                              | EQ | EQ = popStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent)
+...                                              | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent)
    (\ tree s n0 parent -> insertCase5 tree s n0 rightParent grandParent next))
 ...                                              | _ | _  = insertCase41 tree s n0 parent grandParent next
   where
-    insertCase41 : {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
-    insertCase41 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next
+    insertCase41 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+    insertCase41 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next
                  with  (left parent) | (right grandParent)       
     ...    | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next
     ...    | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next
     ...    | Just leftParent | Just rightGrandParent with compare tree (key n0) (key leftParent) | compare tree (key parent) (key rightGrandParent)
-    ...                                              | EQ | EQ = popStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent)
+    ...                                              | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent)
        (\ tree s n0 parent -> insertCase5 tree s n0 leftParent grandParent next))
     ...                                              | _ | _  = insertCase5 tree s (Just n0) parent grandParent next
 
@@ -141,22 +141,22 @@
 colorNode old c = record old { color = c }
 
 {-# 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 (insertCase1 n0)
+insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+insertNode {n} {m} {t} {a} {k}  tree s n0 next = get2SingleLinkedStack s (insertCase1 n0)
    where
-    insertCase1 : Node a k -> Stack (Node a k) si -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allow mutual recursion
+    insertCase1 : Node a k -> SingleLinkedStack (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 : SingleLinkedStack (Node a k) -> 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  (
+    ...                           | Red = pop2SingleLinkedStack s ( \s p0 p1 -> insertCase1  (
            record grandParent { color = Red ; left = Just ( record parent { color = Black } )  ; right = Just ( record uncle { color = Black } ) }) s 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 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t
     insertCase2 s n0 parent grandParent with color parent
     ... | Black = replaceNode tree s n0 next
     ... | Red =   insertCase3 s n0 parent grandParent
@@ -168,15 +168,15 @@
 ----
 -- find node potition to insert or to delete, the pass will be in the stack
 -- 
-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 -> SingleLinkedStack (Node a k) -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t
+findNode {n} {m} {a} {k}  {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1)
   where
-    findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
+    findNode2 : SingleLinkedStack (Node a k) -> (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 : SingleLinkedStack (Node a k) -> (Node a k)  -> t
     findNode1 s n1 with (compare tree (key n0) (key n1))
-    ...                                | EQ = popStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n1 } ) )
+    ...                                | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n1 } ) )
     ...                                | GT = findNode2 s (right n1)
     ...                                | LT = findNode2 s (left n1)
 
@@ -190,13 +190,13 @@
     color = Red
   }
 
-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 {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} 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  = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next))
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (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 -> k -> (RedBlackTree {n} {m} {t} a k -> (Maybe (Node a k)) -> t) -> t
+getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
   where
     search : Node a k -> t
     checkNode : Maybe (Node a k) -> t
@@ -209,10 +209,10 @@
 
 open import Data.Nat hiding (compare)
 
-createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ ( SingleLinkedStack (Node a ℕ ) )
+createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
 createEmptyRedBlackTreeℕ  {m} a {t} = record {
         root = Nothing
-     ;  nodeStack = createSingleLinkedStack 
+     ;  nodeStack = emptySingleLinkedStack
      ;  compare = compare1
    } where
        compare1 :  ℕ → ℕ → CompareResult {Level.zero}
diff -r ee65e69c9b62 -r 1595dd84fc3e redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Thu Jan 11 17:38:13 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Jan 11 17:53:03 2018 +0900
@@ -13,10 +13,10 @@
 
 -- tests
 
-putTree1 : {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
-putTree1 {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
+putTree1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
 ...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
-...                                | Just n2  = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next))
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next))
 
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Core
@@ -41,7 +41,7 @@
 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 
     $ \t -> putTree1 t 2 2
     $ \t -> putTree1 t 3 3
-    $ \t -> putTree1 t 4 4
+    $ \t -> putTree1 t 4 4        
     $ \t -> getRedBlackTree t 4
     $ \t x -> check1 x 4 ≡ True  
 test3 = refl
@@ -60,7 +60,7 @@
 -- test5 : Maybe (Node ℕ ℕ)
 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 
     $ \t -> putTree1 t 6 6
-    $ \t0 ->  clearStack (nodeStack t0)
+    $ \t0 ->  clearSingleLinkedStack (nodeStack t0)
     $ \s -> findNode1 t0 s (leafNode 3 3) ( root t0 )
     $ \t1 s n1 -> replaceNode t1 s n1 
     $ \t -> getRedBlackTree t 3
@@ -68,7 +68,7 @@
     -- $ \t x -> n1
     $ \t x -> root t
   where
-     findNode1 : {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) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
+     findNode1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t
      findNode1 t s n1 Nothing next = next t s n1
      findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next
 
@@ -81,7 +81,7 @@
 
 
 test7 : Maybe (Node ℕ ℕ)
-test7 = clearStack (nodeStack tree2) (\ s -> replaceNode tree2 s n2 (\ t -> root t))
+test7 = clearSingleLinkedStack (nodeStack tree2) (\ s -> replaceNode tree2 s n2 (\ t -> root t))
   where
     tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}
     k1 = 1