Mercurial > hg > Gears > GearsAgda
annotate RedBlackTree.agda @ 570:a6aa2ff5fea4
separate clearStack
| author | ryokka |
|---|---|
| date | Thu, 26 Apr 2018 20:09:55 +0900 |
| parents | 40ab3d39e49d |
| children | 73fc32092b64 |
| rev | line source |
|---|---|
| 417 | 1 module RedBlackTree where |
| 2 | |
| 3 open import stack | |
| 533 | 4 open import Level hiding (zero) |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
5 open import Relation.Binary |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
6 open import Data.Nat.Properties as NatProp |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
7 |
| 511 | 8 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where |
| 9 field | |
| 10 putImpl : treeImpl -> a -> (treeImpl -> t) -> t | |
| 11 getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t | |
| 12 open TreeMethods | |
| 13 | |
| 14 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where | |
| 417 | 15 field |
| 16 tree : treeImpl | |
| 513 | 17 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl |
| 18 putTree : a -> (Tree treeImpl -> t) -> t | |
| 511 | 19 putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) |
| 513 | 20 getTree : (Tree treeImpl -> Maybe a -> t) -> t |
| 511 | 21 getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) |
| 427 | 22 |
| 478 | 23 open Tree |
| 24 | |
| 513 | 25 data Color {n : Level } : Set n where |
| 425 | 26 Red : Color |
| 27 Black : Color | |
| 28 | |
| 512 | 29 data CompareResult {n : Level } : Set n where |
| 30 LT : CompareResult | |
| 31 GT : CompareResult | |
| 32 EQ : CompareResult | |
| 33 | |
| 513 | 34 record Node {n : Level } (a k : Set n) : Set n where |
| 35 inductive | |
| 425 | 36 field |
| 512 | 37 key : k |
| 38 value : a | |
| 513 | 39 right : Maybe (Node a k) |
| 40 left : Maybe (Node a k) | |
| 514 | 41 color : Color {n} |
| 512 | 42 open Node |
| 425 | 43 |
| 543 | 44 record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where |
| 417 | 45 field |
| 514 | 46 root : Maybe (Node a k) |
| 543 | 47 nodeStack : SingleLinkedStack (Node a k) |
| 514 | 48 compare : k -> k -> CompareResult {n} |
| 425 | 49 |
| 417 | 50 open RedBlackTree |
| 51 | |
| 543 | 52 open SingleLinkedStack |
| 512 | 53 |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
54 -- |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
55 -- put new node at parent node, and rebuild tree to the top |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
56 -- |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
57 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html |
| 543 | 58 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 |
| 59 replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s ( | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
60 \s parent -> replaceNode1 s parent) |
| 570 | 61 module ReplaceNode where |
| 543 | 62 replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
63 replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } ) |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
64 replaceNode1 s (Just n1) with compare tree (key n1) (key n0) |
| 551 | 65 ... | EQ = replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next |
| 541 | 66 ... | GT = replaceNode tree s ( record n1 { left = Just n0 } ) next |
| 67 ... | LT = replaceNode tree s ( record n1 { right = Just n0 } ) next | |
| 478 | 68 |
| 525 | 69 |
| 543 | 70 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) -> |
| 71 (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t | |
| 72 rotateRight {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext) | |
| 530 | 73 where |
| 543 | 74 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) -> |
| 75 (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t | |
| 76 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0 | |
| 532 | 77 ... | Nothing = rotateNext tree s Nothing n0 |
| 530 | 78 ... | Just n1 with parent |
| 532 | 79 ... | Nothing = rotateNext tree s (Just n1 ) n0 |
| 530 | 80 ... | Just parent1 with left parent1 |
| 532 | 81 ... | Nothing = rotateNext tree s (Just n1) Nothing |
| 530 | 82 ... | Just leftParent with compare tree (key n1) (key leftParent) |
| 532 | 83 ... | EQ = rotateNext tree s (Just n1) parent |
| 84 ... | _ = rotateNext tree s (Just n1) parent | |
| 530 | 85 |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
86 |
| 543 | 87 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) -> |
| 88 (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t | |
| 89 rotateLeft {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext) | |
| 530 | 90 where |
| 543 | 91 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) -> |
| 92 (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t | |
| 93 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0 | |
| 532 | 94 ... | Nothing = rotateNext tree s Nothing n0 |
| 530 | 95 ... | Just n1 with parent |
| 532 | 96 ... | Nothing = rotateNext tree s (Just n1) Nothing |
| 530 | 97 ... | Just parent1 with right parent1 |
| 532 | 98 ... | Nothing = rotateNext tree s (Just n1) Nothing |
| 530 | 99 ... | Just rightParent with compare tree (key n1) (key rightParent) |
| 532 | 100 ... | EQ = rotateNext tree s (Just n1) parent |
| 101 ... | _ = rotateNext tree s (Just n1) parent | |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
102 |
| 530 | 103 {-# TERMINATING #-} |
| 543 | 104 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 |
| 105 insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent -> insertCase51 tree s n0 parent grandParent next) | |
| 530 | 106 where |
| 543 | 107 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 |
| 108 insertCase51 {n} {m} {t} {a} {k} tree s n0 parent grandParent next with n0 | |
| 532 | 109 ... | Nothing = next tree |
| 110 ... | Just n1 with parent | grandParent | |
| 111 ... | Nothing | _ = next tree | |
| 112 ... | _ | Nothing = next tree | |
| 113 ... | Just parent1 | Just grandParent1 with left parent1 | left grandParent1 | |
| 114 ... | Nothing | _ = next tree | |
| 115 ... | _ | Nothing = next tree | |
| 116 ... | Just leftParent1 | Just leftGrandParent1 | |
| 117 with compare tree (key n1) (key leftParent1) | compare tree (key leftParent1) (key leftGrandParent1) | |
| 118 ... | EQ | EQ = rotateRight tree s n0 parent | |
| 119 (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next) | |
| 120 ... | _ | _ = rotateLeft tree s n0 parent | |
| 121 (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next) | |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
122 |
| 543 | 123 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 |
| 124 insertCase4 {n} {m} {t} {a} {k} tree s n0 parent grandParent next | |
| 528 | 125 with (right parent) | (left grandParent) |
| 532 | 126 ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next |
| 127 ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next | |
| 528 | 128 ... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent) |
| 543 | 129 ... | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent) |
| 532 | 130 (\ tree s n0 parent -> insertCase5 tree s n0 rightParent grandParent next)) |
| 530 | 131 ... | _ | _ = insertCase41 tree s n0 parent grandParent next |
| 132 where | |
| 543 | 133 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 |
| 134 insertCase41 {n} {m} {t} {a} {k} tree s n0 parent grandParent next | |
| 530 | 135 with (left parent) | (right grandParent) |
| 532 | 136 ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next |
| 137 ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next | |
| 530 | 138 ... | Just leftParent | Just rightGrandParent with compare tree (key n0) (key leftParent) | compare tree (key parent) (key rightGrandParent) |
| 543 | 139 ... | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent) |
| 532 | 140 (\ tree s n0 parent -> insertCase5 tree s n0 leftParent grandParent next)) |
| 141 ... | _ | _ = insertCase5 tree s (Just n0) parent grandParent next | |
| 527 | 142 |
| 532 | 143 colorNode : {n : Level } {a k : Set n} -> Node a k -> Color -> Node a k |
| 144 colorNode old c = record old { color = c } | |
| 527 | 145 |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
146 {-# TERMINATING #-} |
| 543 | 147 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 |
| 148 insertNode {n} {m} {t} {a} {k} tree s n0 next = get2SingleLinkedStack s (insertCase1 n0) | |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
149 where |
| 543 | 150 insertCase1 : Node a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
151 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html |
| 543 | 152 insertCase3 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
153 insertCase3 s n0 parent grandParent with left grandParent | right grandParent |
| 528 | 154 ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next |
| 155 ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next | |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
156 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent ) |
| 528 | 157 ... | EQ = insertCase4 tree s n0 parent grandParent next |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
158 ... | _ with color uncle |
| 543 | 159 ... | Red = pop2SingleLinkedStack s ( \s p0 p1 -> insertCase1 ( |
| 532 | 160 record grandParent { color = Red ; left = Just ( record parent { color = Black } ) ; right = Just ( record uncle { color = Black } ) }) s p0 p1 ) |
| 528 | 161 ... | Black = insertCase4 tree s n0 parent grandParent next |
| 543 | 162 insertCase2 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
163 insertCase2 s n0 parent grandParent with color parent |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
164 ... | Black = replaceNode tree s n0 next |
| 532 | 165 ... | Red = insertCase3 s n0 parent grandParent |
| 166 insertCase1 n0 s Nothing Nothing = next tree | |
| 167 insertCase1 n0 s Nothing (Just grandParent) = next tree | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
168 insertCase1 n0 s (Just parent) Nothing = replaceNode tree s (colorNode n0 Black) next |
| 532 | 169 insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent |
| 528 | 170 |
| 531 | 171 ---- |
| 549 | 172 -- find node potition to insert or to delete, the path will be in the stack |
| 531 | 173 -- |
| 543 | 174 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 |
| 175 findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1) | |
| 570 | 176 module FindNode where |
| 543 | 177 findNode2 : SingleLinkedStack (Node a k) -> (Maybe (Node a k)) -> t |
| 515 | 178 findNode2 s Nothing = next tree s n0 |
| 179 findNode2 s (Just n) = findNode tree s n0 n next | |
| 543 | 180 findNode1 : SingleLinkedStack (Node a k) -> (Node a k) -> t |
| 515 | 181 findNode1 s n1 with (compare tree (key n0) (key n1)) |
| 551 | 182 ... | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n0 } ) ) |
| 515 | 183 ... | GT = findNode2 s (right n1) |
| 184 ... | LT = findNode2 s (left n1) | |
| 425 | 185 |
| 186 | |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
187 leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k |
| 515 | 188 leafNode k1 value = record { |
| 189 key = k1 ; | |
| 190 value = value ; | |
| 191 right = Nothing ; | |
| 192 left = Nothing ; | |
| 532 | 193 color = Red |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
194 } |
| 417 | 195 |
| 543 | 196 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 |
| 197 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) | |
| 515 | 198 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) |
| 543 | 199 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)) |
| 515 | 200 |
| 543 | 201 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 |
| 202 getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree) | |
| 551 | 203 module GetRedBlackTree where -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html |
| 542 | 204 search : Node a k -> t |
| 515 | 205 checkNode : Maybe (Node a k) -> t |
| 206 checkNode Nothing = cs tree Nothing | |
| 207 checkNode (Just n) = search n | |
| 542 | 208 search n with compare tree k1 (key n) |
| 209 search n | LT = checkNode (left n) | |
| 210 search n | GT = checkNode (right n) | |
| 211 search n | EQ = cs tree (Just n) | |
| 533 | 212 |
| 213 open import Data.Nat hiding (compare) | |
| 214 | |
| 545 | 215 compareℕ : ℕ → ℕ → CompareResult {Level.zero} |
| 216 compareℕ x y with Data.Nat.compare x y | |
| 217 ... | less _ _ = LT | |
| 218 ... | equal _ = EQ | |
| 219 ... | greater _ _ = GT | |
| 220 | |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
221 compareT : ℕ → ℕ → CompareResult {Level.zero} |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
222 compareT x y with IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) x y |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
223 ... | tri≈ _ _ _ = EQ |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
224 ... | tri< _ _ _ = LT |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
225 ... | tri> _ _ _ = GT |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
226 |
| 549 | 227 compare2 : (x y : ℕ ) -> CompareResult {Level.zero} |
| 228 compare2 zero zero = EQ | |
| 229 compare2 (suc _) zero = GT | |
| 230 compare2 zero (suc _) = LT | |
| 231 compare2 (suc x) (suc y) = compare2 x y | |
| 232 | |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
233 putUnblanceTree : {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 |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
234 putUnblanceTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
235 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
236 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next)) |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
237 |
| 545 | 238 |
| 543 | 239 createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ |
| 533 | 240 createEmptyRedBlackTreeℕ {m} a {t} = record { |
| 241 root = Nothing | |
| 543 | 242 ; nodeStack = emptySingleLinkedStack |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
551
diff
changeset
|
243 ; compare = compareT |
| 545 | 244 } |
| 245 |