|
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
|
|
511
|
15 treeMethods : TreeMethods {a} {t}
|
|
|
16 putTree : a -> (Tree -> t) -> t
|
|
|
17 putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
|
|
|
18 getTree : (Tree -> Maybe a -> t) -> t
|
|
|
19 getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
|
|
427
|
20
|
|
478
|
21 open Tree
|
|
|
22
|
|
425
|
23 data Color : Set where
|
|
|
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
|
|
|
32 record Node (a k : Set) : Set where
|
|
425
|
33 field
|
|
512
|
34 key : k
|
|
|
35 value : a
|
|
425
|
36 right : Maybe (Node a)
|
|
|
37 left : Maybe (Node a)
|
|
|
38 color : Color
|
|
512
|
39 open Node
|
|
425
|
40
|
|
512
|
41 record RedBlackTree (a k si : Set) : Set where
|
|
417
|
42 field
|
|
512
|
43 root : Maybe (Node a k )
|
|
511
|
44 stack : Stack si
|
|
512
|
45 compare : k -> k -> CompareResult
|
|
425
|
46
|
|
417
|
47 open RedBlackTree
|
|
|
48
|
|
512
|
49 open Stack
|
|
|
50
|
|
|
51 insertCase3 : ?
|
|
|
52 insertCase3 = ? -- tree datum parent grandparent next
|
|
478
|
53
|
|
512
|
54 insertCase2 : {n m : Level } {t : Set m } {a : Set n} -> RedBlackTree ? ? -> a (Node a) (Node a) ? -> t
|
|
|
55 insertCase2 tree datum parent grandparent next with (color parent)
|
|
|
56 ... | Red = insertCase3 tree datum parent grandparent next
|
|
|
57 ... | Black = next (record { root = ?; stack = createSingleLinkedStack })
|
|
425
|
58
|
|
512
|
59 insertCase1 : {n m : Level } {t : Set m } {a : Set n} -> RedBlackTree ? ? -> a (Maybe (Node a) ) (Node a) ? -> t
|
|
|
60 insertCase1 tree datum Nothing grandparent next = next (record { root = ?; stack = createSingleLinkedStack })
|
|
|
61 insertCase1 tree datum (Just parent) grandparent next = insertCase2 tree datum parent grandparent next
|
|
|
62
|
|
|
63 insertNode : ?
|
|
|
64 insertNode tree datum next = get2Stack (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next)
|
|
425
|
65
|
|
|
66 findNode1 : {Data t : Set} -> RedBlackTree Data -> Data -> Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
|
|
|
67 findNode1 tree datum n next with (compare datum n)
|
|
428
|
68 ... | EQ = popStack (tree stack) (\s d -> findNode3 d (record tree { root = just (record n {node = datum}); stack = s }) next)
|
|
425
|
69 ... | GT = findNode2 tree datum (right n) next
|
|
|
70 ... | LT = findNode2 tree datum (left n) next
|
|
417
|
71 where
|
|
425
|
72 findNode2 tree datum nothing next = insertNode tree datum next
|
|
427
|
73 findNode2 tree datum (just n) next = findNode (record tree {root = just n}) datum n next
|
|
512
|
74 findNode3 : ?
|
|
428
|
75 findNode3 nothing tree next = next tree
|
|
|
76 findNode3 (just n) tree next =
|
|
478
|
77 popStack (tree stack) (\s d -> findNode3 d (record { root = record n {right = ? } }))
|
|
425
|
78
|
|
512
|
79 findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
|
|
|
80 findNode tree datum n next = pushStack (stack tree) n (\ s -> findNode1 (record tree {stack = s }) datum n next)
|
|
425
|
81
|
|
512
|
82 putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
|
|
|
83 putRedBlackTree tree datum next with (root tree)
|
|
|
84 ... | Nothing = insertNode tree datum next
|
|
|
85 ... | Just n = findNode tree datum n (\ tree1 -> insertNode tree1 datum next)
|
|
417
|
86
|
|
|
87 getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
|
|
425
|
88 getRedBlackTree tree cs with (root tree)
|
|
417
|
89 ... | Nothing = cs tree Nothing
|
|
|
90 ... | Just d = cs stack1 (Just data1)
|
|
|
91 where
|
|
|
92 data1 = datum d
|
|
425
|
93 stack1 = record { root = (next d) }
|
