Mercurial > hg > Gears > GearsAgda
annotate RedBlackTree.agda @ 532:ccf98ed4a4f7
fix red black tree
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 09 Jan 2018 23:56:42 +0900 |
parents | f6060e1bf900 |
children | 2d6ccbf429ad |
rev | line source |
---|---|
417 | 1 module RedBlackTree where |
2 | |
3 open import stack | |
511 | 4 open import Level |
417 | 5 |
511 | 6 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where |
7 field | |
8 putImpl : treeImpl -> a -> (treeImpl -> t) -> t | |
9 getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t | |
10 open TreeMethods | |
11 | |
12 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where | |
417 | 13 field |
14 tree : treeImpl | |
513 | 15 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl |
16 putTree : a -> (Tree treeImpl -> t) -> t | |
511 | 17 putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) |
513 | 18 getTree : (Tree treeImpl -> Maybe a -> t) -> t |
511 | 19 getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) |
427 | 20 |
478 | 21 open Tree |
22 | |
513 | 23 data Color {n : Level } : Set n where |
425 | 24 Red : Color |
25 Black : Color | |
26 | |
512 | 27 data CompareResult {n : Level } : Set n where |
28 LT : CompareResult | |
29 GT : CompareResult | |
30 EQ : CompareResult | |
31 | |
513 | 32 record Node {n : Level } (a k : Set n) : Set n where |
33 inductive | |
425 | 34 field |
512 | 35 key : k |
36 value : a | |
513 | 37 right : Maybe (Node a k) |
38 left : Maybe (Node a k) | |
514 | 39 color : Color {n} |
512 | 40 open Node |
425 | 41 |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
42 record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where |
417 | 43 field |
514 | 44 root : Maybe (Node a k) |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
45 nodeStack : Stack {n} {m} (Node a k) {t} si |
514 | 46 compare : k -> k -> CompareResult {n} |
425 | 47 |
417 | 48 open RedBlackTree |
49 | |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
50 open Stack |
512 | 51 |
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
52 -- |
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
53 -- 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
|
54 -- |
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
55 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
56 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 |
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
57 replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s ( |
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
58 \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) ) |
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
59 where |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
60 replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t |
529 | 61 replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } ) |
62 replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } ) | |
63 replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } ) | |
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
64 replaceNode1 s (Just grandParent) result with result |
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
65 ... | LT = replaceNode tree s grandParent ( record parent { left = Just n0 } ) next |
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
66 ... | GT = replaceNode tree s grandParent ( record parent { right = Just n0 } ) next |
529 | 67 ... | EQ = next tree |
478 | 68 |
525 | 69 |
532 | 70 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) -> |
71 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t | |
72 rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext = getStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext) | |
530 | 73 where |
532 | 74 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) -> |
75 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t | |
76 rotateRight1 {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext with n0 | |
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 |
532 | 87 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) -> |
88 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t | |
89 rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext = getStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext) | |
530 | 90 where |
532 | 91 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) -> |
92 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t | |
93 rotateLeft1 {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext with n0 | |
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 #-} |
532 | 104 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 |
530 | 105 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) |
106 where | |
532 | 107 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 |
108 insertCase51 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with n0 | |
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 |
528 | 123 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 |
527 | 124 insertCase4 {n} {m} {t} {a} {k} {si} 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) |
532 | 129 ... | EQ | EQ = popStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent) |
130 (\ tree s n0 parent -> insertCase5 tree s n0 rightParent grandParent next)) | |
530 | 131 ... | _ | _ = insertCase41 tree s n0 parent grandParent next |
132 where | |
133 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 | |
134 insertCase41 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next | |
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) |
532 | 139 ... | EQ | EQ = popStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent) |
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 #-} |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
147 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 |
532 | 148 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack 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 |
532 | 150 insertCase1 : Node a k -> Stack (Node a k) si -> 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 |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
152 insertCase3 : Stack (Node a k) si -> 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 |
532 | 159 ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 ( |
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 |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
162 insertCase2 : Stack (Node a k) si -> 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 |
532 | 164 ... | Black = replaceNode tree s parent n0 next |
165 ... | Red = insertCase3 s n0 parent grandParent | |
166 insertCase1 n0 s Nothing Nothing = next tree | |
167 insertCase1 n0 s Nothing (Just grandParent) = next tree | |
168 insertCase1 n0 s (Just parent) Nothing = replaceNode tree s parent (colorNode n0 Black) next | |
169 insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent | |
528 | 170 |
531 | 171 ---- |
172 -- find node potition to insert or to delete, the pass will be in the stack | |
173 -- | |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
174 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 |
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
175 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1) |
417 | 176 where |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
177 findNode2 : Stack (Node a k) si -> (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 | |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
180 findNode1 : Stack (Node a k) si -> (Node a k) -> t |
515 | 181 findNode1 s n1 with (compare tree (key n0) (key n1)) |
529 | 182 ... | EQ = next tree s 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 |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
196 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 |
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
197 putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree) |
515 | 198 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) |
531 | 199 ... | Just n2 = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)) |
515 | 200 |
522
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
201 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 |
f63a9a081b61
remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
202 getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree) |
417 | 203 where |
515 | 204 checkNode : Maybe (Node a k) -> t |
205 checkNode Nothing = cs tree Nothing | |
206 checkNode (Just n) = search n | |
207 where | |
208 search : Node a k -> t | |
209 search n with compare tree k1 (key n) | |
210 search n | LT = checkNode (left n) | |
211 search n | GT = checkNode (right n) | |
212 search n | EQ = cs tree (Just n) |