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