Mercurial > hg > Gears > GearsAgda
annotate src/parallel_execution/RedBlackTree.agda @ 521:e3cd5e3a01b8
add stack implement
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 Jan 2018 09:31:04 +0900 |
| parents | b118ed3ba583 |
| children | f63a9a081b61 |
| 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 |
| 521 | 42 Stak : {n m : Level } (a k : Set n) (t : Set m ) -> Set (m ⊔ n) |
| 43 Stak {n} {m} a k t = Stack {n} {m} (Node a k) {t} (SingleLinkedStack (Node a k)) | |
| 44 open Stack | |
| 45 | |
| 46 record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where | |
| 417 | 47 field |
| 514 | 48 root : Maybe (Node a k) |
| 521 | 49 nodeStack : Stak a k t |
| 514 | 50 compare : k -> k -> CompareResult {n} |
| 425 | 51 |
| 417 | 52 open RedBlackTree |
| 53 | |
| 521 | 54 |
| 512 | 55 |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
56 -- |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
57 -- 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
|
58 -- |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
59 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html |
| 521 | 60 replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t |
| 61 replaceNode {n} {m} {t} {a} {k} 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
|
62 \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
|
63 where |
| 521 | 64 replaceNode1 : Stak a k t -> Maybe ( Node a k ) -> CompareResult -> t |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
65 replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } ) |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
66 replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } ) |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
67 replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } ) |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
68 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
|
69 ... | 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
|
70 ... | GT = replaceNode tree s grandParent ( record parent { right = Just n0 } ) next |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
71 ... | EQ = next tree |
| 478 | 72 |
| 521 | 73 rotateRight : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t |
| 74 rotateRight {n} {m} {t} {a} {k} tree s n0 parent grandParent next = {!!} | |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
75 |
| 521 | 76 rotateLeft : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t |
| 77 rotateLeft {n} {m} {t} {a} {k} tree s n0 parent grandParent next = {!!} | |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
78 |
| 521 | 79 insertCase5 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t |
| 80 insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = {!!} | |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
81 |
| 521 | 82 insertCase4 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t |
| 83 insertCase4 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = {!!} | |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
84 |
|
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
85 {-# TERMINATING #-} |
| 521 | 86 insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t |
| 87 insertNode {n} {m} {t} {a} {k} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 ) | |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
88 where |
| 521 | 89 insertCase1 : Stack (Node a k) (SingleLinkedStack (Node a k)) -> 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
|
90 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html |
| 521 | 91 insertCase3 : Stak a k t -> 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
|
92 insertCase3 s n0 parent grandParent with left grandParent | right grandParent |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
93 ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next |
|
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
94 ... | 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
|
95 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent ) |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
96 ... | 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
|
97 ... | _ with color uncle |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
98 ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
99 record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 ) |
|
519
0a723e418b2a
add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
518
diff
changeset
|
100 ... | Black = insertCase4 tree s n0 parent grandParent next |
| 521 | 101 insertCase2 : Stak a k t -> 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
|
102 insertCase2 s n0 parent grandParent with color parent |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
103 ... | Black = replaceNode tree s grandParent n0 next |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
104 ... | Red = insertCase3 s n0 parent grandParent |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
105 insertCase1 s n0 Nothing Nothing = next tree |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
106 insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
107 insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
108 insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent |
|
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
109 where |
| 425 | 110 |
| 521 | 111 findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> t) -> t |
| 112 findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1) | |
| 417 | 113 where |
| 521 | 114 findNode2 : Stak a k t -> (Maybe (Node a k)) -> t |
| 515 | 115 findNode2 s Nothing = next tree s n0 |
| 116 findNode2 s (Just n) = findNode tree s n0 n next | |
| 521 | 117 findNode1 : Stak a k t -> (Node a k) -> t |
| 515 | 118 findNode1 s n1 with (compare tree (key n0) (key n1)) |
| 119 ... | EQ = next tree s n0 | |
| 120 ... | GT = findNode2 s (right n1) | |
| 121 ... | LT = findNode2 s (left n1) | |
| 425 | 122 |
| 123 | |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
124 leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k |
| 515 | 125 leafNode k1 value = record { |
| 126 key = k1 ; | |
| 127 value = value ; | |
| 128 right = Nothing ; | |
| 129 left = Nothing ; | |
| 130 color = Black | |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
131 } |
| 417 | 132 |
| 521 | 133 putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree a k -> k -> a -> (RedBlackTree a k -> t) -> t |
| 520 | 134 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) |
| 515 | 135 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) |
|
518
c9f90f573efe
add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
515
diff
changeset
|
136 ... | Just n2 = findNode tree (nodeStack tree) (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next) |
| 515 | 137 |
| 521 | 138 getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> (RedBlackTree a k -> (Maybe (Node a k)) -> t) -> t |
| 520 | 139 getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree) |
| 417 | 140 where |
| 515 | 141 checkNode : Maybe (Node a k) -> t |
| 142 checkNode Nothing = cs tree Nothing | |
| 143 checkNode (Just n) = search n | |
| 144 where | |
| 145 search : Node a k -> t | |
| 146 search n with compare tree k1 (key n) | |
| 147 search n | LT = checkNode (left n) | |
| 148 search n | GT = checkNode (right n) | |
| 149 search n | EQ = cs tree (Just n) |