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