|
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
|
|
514
|
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)
|
|
515
|
45 nodeStack : Stack {n} {m} (Node a k) {t} si
|
|
514
|
46 compare : k -> k -> CompareResult {n}
|
|
425
|
47
|
|
417
|
48 open RedBlackTree
|
|
|
49
|
|
512
|
50 open Stack
|
|
|
51
|
|
478
|
52
|
|
515
|
53 insertNode : {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 -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
|
|
|
54 insertNode tree s datum next = get2Stack s (\ s d1 d2 -> {!!} tree s datum d1 d2 next)
|
|
425
|
55
|
|
515
|
56 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
|
|
|
57 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
|
|
417
|
58 where
|
|
515
|
59 findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
|
|
|
60 findNode2 s Nothing = next tree s n0
|
|
|
61 findNode2 s (Just n) = findNode tree s n0 n next
|
|
|
62 findNode1 : Stack (Node a k) si -> (Node a k) -> t
|
|
|
63 findNode1 s n1 with (compare tree (key n0) (key n1))
|
|
|
64 ... | EQ = next tree s n0
|
|
|
65 ... | GT = findNode2 s (right n1)
|
|
|
66 ... | LT = findNode2 s (left n1)
|
|
513
|
67 where
|
|
515
|
68 -- findNode3 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
|
|
|
69 -- findNode3 s nothing = next tree s n0
|
|
|
70 -- findNode3 s (Just n) =
|
|
|
71 -- popStack (nodeStack tree) (\s d -> findNode3 s d)
|
|
425
|
72
|
|
|
73
|
|
515
|
74 leafNode : {n m : Level } {a k si : Set n} {t : Set m} -> k -> a -> Node a k
|
|
|
75 leafNode k1 value = record {
|
|
|
76 key = k1 ;
|
|
|
77 value = value ;
|
|
|
78 right = Nothing ;
|
|
|
79 left = Nothing ;
|
|
|
80 color = Black
|
|
|
81 }
|
|
417
|
82
|
|
515
|
83 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
|
|
|
84 putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
|
|
|
85 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
|
|
|
86 ... | Just n2 = findNode tree (nodeStack tree) (leafNode {n} {m} {a} {k} {si} {t} k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)
|
|
|
87
|
|
|
88 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
|
|
|
89 getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
|
|
417
|
90 where
|
|
515
|
91 checkNode : Maybe (Node a k) -> t
|
|
|
92 checkNode Nothing = cs tree Nothing
|
|
|
93 checkNode (Just n) = search n
|
|
|
94 where
|
|
|
95 search : Node a k -> t
|
|
|
96 search n with compare tree k1 (key n)
|
|
|
97 search n | LT = checkNode (left n)
|
|
|
98 search n | GT = checkNode (right n)
|
|
|
99 search n | EQ = cs tree (Just n)
|
