Mercurial > hg > Members > Moririn

comparison RedBlackTree.agda @ 523:8fbc3ef749b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate Agda
author ryokka
date Fri, 05 Jan 2018 16:39:43 +0900
parents src/parallel_execution/RedBlackTree.agda@f63a9a081b61
children 0696b9846415
comparison
equal deleted inserted replaced
522:f63a9a081b61 523:8fbc3ef749b6
1 module RedBlackTree where
2
3 open import stack
4 open import Level
5
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
13 field
14 tree : treeImpl
15 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
16 putTree : a -> (Tree treeImpl -> t) -> t
17 putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
18 getTree : (Tree treeImpl -> Maybe a -> t) -> t
19 getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
20
21 open Tree
22
23 data Color {n : Level } : Set n where
24 Red : Color
25 Black : Color
26
27 data CompareResult {n : Level } : Set n where
28 LT : CompareResult
29 GT : CompareResult
30 EQ : CompareResult
31
32 record Node {n : Level } (a k : Set n) : Set n where
33 inductive
34 field
35 key : k
36 value : a
37 right : Maybe (Node a k)
38 left : Maybe (Node a k)
39 color : Color {n}
40 open Node
41
42 record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
43 field
44 root : Maybe (Node a k)
45 nodeStack : Stack {n} {m} (Node a k) {t} si
46 compare : k -> k -> CompareResult {n}
47
48 open RedBlackTree
49
50 open Stack
51
52 --
53 -- put new node at parent node, and rebuild tree to the top
54 --
55 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
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
57 replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s (
58 \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
59 where
60 replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t
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 } ) } )
64 replaceNode1 s (Just grandParent) result with result
65 ... | LT = replaceNode tree s grandParent ( record parent { left = Just n0 } ) next
66 ... | GT = replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
67 ... | EQ = next tree
68
69 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 -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
70 rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
71
72 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 -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
73 rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
74
75 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 -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
76 insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
77
78 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
79 insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
80
81 {-# TERMINATING #-}
82 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
83 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
84 where
85 insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion
86 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
87 insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
88 insertCase3 s n0 parent grandParent with left grandParent | right grandParent
89 ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
90 ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next
91 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent )
92 ... | EQ = insertCase4 tree s n0 parent grandParent next
93 ... | _ with color uncle
94 ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s (
95 record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
96 ... | Black = insertCase4 tree s n0 parent grandParent next
97 insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
98 insertCase2 s n0 parent grandParent with color parent
99 ... | Black = replaceNode tree s grandParent n0 next
100 ... | Red = insertCase3 s n0 parent grandParent
101 insertCase1 s n0 Nothing Nothing = next tree
102 insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
103 insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
104 insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
105 where
106
107 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
108 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
109 where
110 findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
111 findNode2 s Nothing = next tree s n0
112 findNode2 s (Just n) = findNode tree s n0 n next
113 findNode1 : Stack (Node a k) si -> (Node a k) -> t
114 findNode1 s n1 with (compare tree (key n0) (key n1))
115 ... | EQ = next tree s n0
116 ... | GT = findNode2 s (right n1)
117 ... | LT = findNode2 s (left n1)
118
119
120 leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k
121 leafNode k1 value = record {
122 key = k1 ;
123 value = value ;
124 right = Nothing ;
125 left = Nothing ;
126 color = Black
127 }
128
129 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
130 putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
131 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
132 ... | Just n2 = findNode tree (nodeStack tree) (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)
133
134 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
135 getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
136 where
137 checkNode : Maybe (Node a k) -> t
138 checkNode Nothing = cs tree Nothing
139 checkNode (Just n) = search n
140 where
141 search : Node a k -> t
142 search n with compare tree k1 (key n)
143 search n | LT = checkNode (left n)
144 search n | GT = checkNode (right n)
145 search n | EQ = cs tree (Just n)