Mercurial > hg > Papers > 2021 > soto-prosym
comparison Paper/src/RedBlackTree.agda.replaced @ 0:c59202657321
init
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 02 Nov 2021 06:55:58 +0900 |
| parents | |
| children | 339fb67b4375 |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:c59202657321 |
|---|---|
| 1 module RedBlackTree where | |
| 2 | |
| 3 open import stack | |
| 4 open import Level hiding (zero) | |
| 5 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where | |
| 6 field | |
| 7 putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 8 getImpl : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 9 open TreeMethods | |
| 10 | |
| 11 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where | |
| 12 field | |
| 13 tree : treeImpl | |
| 14 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl | |
| 15 putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 16 putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} )) | |
| 17 getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 18 getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d ) | |
| 19 | |
| 20 open Tree | |
| 21 | |
| 22 data Color {n : Level } : Set n where | |
| 23 Red : Color | |
| 24 Black : Color | |
| 25 | |
| 26 data CompareResult {n : Level } : Set n where | |
| 27 LT : CompareResult | |
| 28 GT : CompareResult | |
| 29 EQ : CompareResult | |
| 30 | |
| 31 record Node {n : Level } (a k : Set n) : Set n where | |
| 32 inductive | |
| 33 field | |
| 34 key : k | |
| 35 value : a | |
| 36 right : Maybe (Node a k) | |
| 37 left : Maybe (Node a k) | |
| 38 color : Color {n} | |
| 39 open Node | |
| 40 | |
| 41 record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where | |
| 42 field | |
| 43 root : Maybe (Node a k) | |
| 44 nodeStack : SingleLinkedStack (Node a k) | |
| 45 compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n} | |
| 46 | |
| 47 open RedBlackTree | |
| 48 | |
| 49 open SingleLinkedStack | |
| 50 | |
| 51 -- | |
| 52 -- put new node at parent node, and rebuild tree to the top | |
| 53 -- | |
| 54 {-@$\#$@ TERMINATING @$\#$@-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html | |
| 55 replaceNode : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 56 replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s ( | |
| 57 \s parent @$\rightarrow$@ replaceNode1 s parent) | |
| 58 where | |
| 59 replaceNode1 : SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe ( Node a k ) @$\rightarrow$@ t | |
| 60 replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } ) | |
| 61 replaceNode1 s (Just n1) with compare tree (key n1) (key n0) | |
| 62 ... | EQ = replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next | |
| 63 ... | GT = replaceNode tree s ( record n1 { left = Just n0 } ) next | |
| 64 ... | LT = replaceNode tree s ( record n1 { right = Just n0 } ) next | |
| 65 | |
| 66 | |
| 67 rotateRight : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ | |
| 68 (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 69 rotateRight {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 @$\rightarrow$@ rotateRight1 tree s n0 parent rotateNext) | |
| 70 where | |
| 71 rotateRight1 : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ | |
| 72 (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 73 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0 | |
| 74 ... | Nothing = rotateNext tree s Nothing n0 | |
| 75 ... | Just n1 with parent | |
| 76 ... | Nothing = rotateNext tree s (Just n1 ) n0 | |
| 77 ... | Just parent1 with left parent1 | |
| 78 ... | Nothing = rotateNext tree s (Just n1) Nothing | |
| 79 ... | Just leftParent with compare tree (key n1) (key leftParent) | |
| 80 ... | EQ = rotateNext tree s (Just n1) parent | |
| 81 ... | _ = rotateNext tree s (Just n1) parent | |
| 82 | |
| 83 | |
| 84 rotateLeft : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ | |
| 85 (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 86 rotateLeft {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 @$\rightarrow$@ rotateLeft1 tree s n0 parent rotateNext) | |
| 87 where | |
| 88 rotateLeft1 : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ | |
| 89 (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 90 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0 | |
| 91 ... | Nothing = rotateNext tree s Nothing n0 | |
| 92 ... | Just n1 with parent | |
| 93 ... | Nothing = rotateNext tree s (Just n1) Nothing | |
| 94 ... | Just parent1 with right parent1 | |
| 95 ... | Nothing = rotateNext tree s (Just n1) Nothing | |
| 96 ... | Just rightParent with compare tree (key n1) (key rightParent) | |
| 97 ... | EQ = rotateNext tree s (Just n1) parent | |
| 98 ... | _ = rotateNext tree s (Just n1) parent | |
| 99 | |
| 100 {-@$\#$@ TERMINATING @$\#$@-} | |
| 101 insertCase5 : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 102 insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent @$\rightarrow$@ insertCase51 tree s n0 parent grandParent next) | |
| 103 where | |
| 104 insertCase51 : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 105 insertCase51 {n} {m} {t} {a} {k} tree s n0 parent grandParent next with n0 | |
| 106 ... | Nothing = next tree | |
| 107 ... | Just n1 with parent | grandParent | |
| 108 ... | Nothing | _ = next tree | |
| 109 ... | _ | Nothing = next tree | |
| 110 ... | Just parent1 | Just grandParent1 with left parent1 | left grandParent1 | |
| 111 ... | Nothing | _ = next tree | |
| 112 ... | _ | Nothing = next tree | |
| 113 ... | Just leftParent1 | Just leftGrandParent1 | |
| 114 with compare tree (key n1) (key leftParent1) | compare tree (key leftParent1) (key leftGrandParent1) | |
| 115 ... | EQ | EQ = rotateRight tree s n0 parent | |
| 116 (\ tree s n0 parent @$\rightarrow$@ insertCase5 tree s n0 parent1 grandParent1 next) | |
| 117 ... | _ | _ = rotateLeft tree s n0 parent | |
| 118 (\ tree s n0 parent @$\rightarrow$@ insertCase5 tree s n0 parent1 grandParent1 next) | |
| 119 | |
| 120 insertCase4 : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 121 insertCase4 {n} {m} {t} {a} {k} tree s n0 parent grandParent next | |
| 122 with (right parent) | (left grandParent) | |
| 123 ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next | |
| 124 ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next | |
| 125 ... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent) | |
| 126 ... | EQ | EQ = popSingleLinkedStack s (\ s n1 @$\rightarrow$@ rotateLeft tree s (left n0) (Just grandParent) | |
| 127 (\ tree s n0 parent @$\rightarrow$@ insertCase5 tree s n0 rightParent grandParent next)) | |
| 128 ... | _ | _ = insertCase41 tree s n0 parent grandParent next | |
| 129 where | |
| 130 insertCase41 : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 131 insertCase41 {n} {m} {t} {a} {k} tree s n0 parent grandParent next | |
| 132 with (left parent) | (right grandParent) | |
| 133 ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next | |
| 134 ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next | |
| 135 ... | Just leftParent | Just rightGrandParent with compare tree (key n0) (key leftParent) | compare tree (key parent) (key rightGrandParent) | |
| 136 ... | EQ | EQ = popSingleLinkedStack s (\ s n1 @$\rightarrow$@ rotateRight tree s (right n0) (Just grandParent) | |
| 137 (\ tree s n0 parent @$\rightarrow$@ insertCase5 tree s n0 leftParent grandParent next)) | |
| 138 ... | _ | _ = insertCase5 tree s (Just n0) parent grandParent next | |
| 139 | |
| 140 colorNode : {n : Level } {a k : Set n} @$\rightarrow$@ Node a k @$\rightarrow$@ Color @$\rightarrow$@ Node a k | |
| 141 colorNode old c = record old { color = c } | |
| 142 | |
| 143 {-@$\#$@ TERMINATING @$\#$@-} | |
| 144 insertNode : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 145 insertNode {n} {m} {t} {a} {k} tree s n0 next = get2SingleLinkedStack s (insertCase1 n0) | |
| 146 where | |
| 147 insertCase1 : Node a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ t -- placed here to allow mutual recursion | |
| 148 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html | |
| 149 insertCase3 : SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ t | |
| 150 insertCase3 s n0 parent grandParent with left grandParent | right grandParent | |
| 151 ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next | |
| 152 ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next | |
| 153 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent ) | |
| 154 ... | EQ = insertCase4 tree s n0 parent grandParent next | |
| 155 ... | _ with color uncle | |
| 156 ... | Red = pop2SingleLinkedStack s ( \s p0 p1 @$\rightarrow$@ insertCase1 ( | |
| 157 record grandParent { color = Red ; left = Just ( record parent { color = Black } ) ; right = Just ( record uncle { color = Black } ) }) s p0 p1 ) | |
| 158 ... | Black = insertCase4 tree s n0 parent grandParent next | |
| 159 insertCase2 : SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ t | |
| 160 insertCase2 s n0 parent grandParent with color parent | |
| 161 ... | Black = replaceNode tree s n0 next | |
| 162 ... | Red = insertCase3 s n0 parent grandParent | |
| 163 insertCase1 n0 s Nothing Nothing = next tree | |
| 164 insertCase1 n0 s Nothing (Just grandParent) = next tree | |
| 165 insertCase1 n0 s (Just parent) Nothing = replaceNode tree s (colorNode n0 Black) next | |
| 166 insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent | |
| 167 | |
| 168 ---- | |
| 169 -- find node potition to insert or to delete, the path will be in the stack | |
| 170 -- | |
| 171 findNode : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ (Node a k) @$\rightarrow$@ (Node a k) @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 172 findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s @$\rightarrow$@ findNode1 s n1) | |
| 173 where | |
| 174 findNode2 : SingleLinkedStack (Node a k) @$\rightarrow$@ (Maybe (Node a k)) @$\rightarrow$@ t | |
| 175 findNode2 s Nothing = next tree s n0 | |
| 176 findNode2 s (Just n) = findNode tree s n0 n next | |
| 177 findNode1 : SingleLinkedStack (Node a k) @$\rightarrow$@ (Node a k) @$\rightarrow$@ t | |
| 178 findNode1 s n1 with (compare tree (key n0) (key n1)) | |
| 179 ... | EQ = popSingleLinkedStack s ( \s _ @$\rightarrow$@ next tree s (record n1 { key = key n1 ; value = value n0 } ) ) | |
| 180 ... | GT = findNode2 s (right n1) | |
| 181 ... | LT = findNode2 s (left n1) | |
| 182 | |
| 183 | |
| 184 leafNode : {n : Level } {a k : Set n} @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k | |
| 185 leafNode k1 value = record { | |
| 186 key = k1 ; | |
| 187 value = value ; | |
| 188 right = Nothing ; | |
| 189 left = Nothing ; | |
| 190 color = Red | |
| 191 } | |
| 192 | |
| 193 putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 194 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) | |
| 195 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) | |
| 196 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next)) | |
| 197 | |
| 198 getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ (Maybe (Node a k)) @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 199 getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree) | |
| 200 module GetRedBlackTree where -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html | |
| 201 search : Node a k @$\rightarrow$@ t | |
| 202 checkNode : Maybe (Node a k) @$\rightarrow$@ t | |
| 203 checkNode Nothing = cs tree Nothing | |
| 204 checkNode (Just n) = search n | |
| 205 search n with compare tree k1 (key n) | |
| 206 search n | LT = checkNode (left n) | |
| 207 search n | GT = checkNode (right n) | |
| 208 search n | EQ = cs tree (Just n) | |
| 209 | |
| 210 open import Data.Nat hiding (compare) | |
| 211 | |
| 212 compare@$\mathbb{N}$@ : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ CompareResult {Level.zero} | |
| 213 compare@$\mathbb{N}$@ x y with Data.Nat.compare x y | |
| 214 ... | less _ _ = LT | |
| 215 ... | equal _ = EQ | |
| 216 ... | greater _ _ = GT | |
| 217 | |
| 218 compare2 : (x y : @$\mathbb{N}$@ ) @$\rightarrow$@ CompareResult {Level.zero} | |
| 219 compare2 zero zero = EQ | |
| 220 compare2 (suc _) zero = GT | |
| 221 compare2 zero (suc _) = LT | |
| 222 compare2 (suc x) (suc y) = compare2 x y | |
| 223 | |
| 224 | |
| 225 createEmptyRedBlackTree@$\mathbb{N}$@ : { m : Level } (a : Set Level.zero) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@ | |
| 226 createEmptyRedBlackTree@$\mathbb{N}$@ {m} a {t} = record { | |
| 227 root = Nothing | |
| 228 ; nodeStack = emptySingleLinkedStack | |
| 229 ; compare = compare2 | |
| 230 } | |
| 231 |