|
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
|
|
|
27 record Node (a : Set) : Set where
|
|
|
28 field
|
|
|
29 node : Element a
|
|
|
30 right : Maybe (Node a)
|
|
|
31 left : Maybe (Node a)
|
|
|
32 color : Color
|
|
|
33
|
|
511
|
34 record RedBlackTree (a si : Set) : Set where
|
|
417
|
35 field
|
|
425
|
36 root : Maybe (Node a)
|
|
511
|
37 stack : Stack si
|
|
425
|
38
|
|
417
|
39 open RedBlackTree
|
|
|
40
|
|
478
|
41 insertNode : ?
|
|
|
42 insertNode tree datum next = get2 (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next)
|
|
|
43
|
|
417
|
44 putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
|
|
425
|
45 putRedBlackTree tree datum next with (root tree)
|
|
|
46 ... | Nothing = insertNode tree datum next
|
|
|
47 ... | Just n = findNode tree datum n (\ tree1 -> insertNode tree1 datum next)
|
|
|
48
|
|
|
49 findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
|
|
478
|
50 findNode tree datum n next = pushStack (stack tree) n (\ s -> findNode1 (record tree {stack = s }) datum n next)
|
|
425
|
51
|
|
|
52 findNode1 : {Data t : Set} -> RedBlackTree Data -> Data -> Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
|
|
|
53 findNode1 tree datum n next with (compare datum n)
|
|
428
|
54 ... | EQ = popStack (tree stack) (\s d -> findNode3 d (record tree { root = just (record n {node = datum}); stack = s }) next)
|
|
425
|
55 ... | GT = findNode2 tree datum (right n) next
|
|
|
56 ... | LT = findNode2 tree datum (left n) next
|
|
417
|
57 where
|
|
425
|
58 findNode2 tree datum nothing next = insertNode tree datum next
|
|
427
|
59 findNode2 tree datum (just n) next = findNode (record tree {root = just n}) datum n next
|
|
428
|
60 findNode3 nothing tree next = next tree
|
|
|
61 findNode3 (just n) tree next =
|
|
478
|
62 popStack (tree stack) (\s d -> findNode3 d (record { root = record n {right = ? } }))
|
|
425
|
63
|
|
|
64
|
|
|
65 insertCase1 tree datum nothing grandparent next = next (record { root = ?; stack = createSingleLinkedStack })
|
|
|
66 insertCase1 tree datum (just parent) grandparent next = insertCase2 tree datum parent grandparent next
|
|
|
67
|
|
|
68 insertCase2 tree datum parent grandparent next with (color parent)
|
|
|
69 ... | Red = insertCase3 tree datum parent grandparent next
|
|
|
70 ... | Black = next (record { root = ?; stack = createSingleLinkedStack })
|
|
|
71
|
|
|
72 insertCase3 tree datum parent grandparent next
|
|
417
|
73
|
|
|
74 getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
|
|
425
|
75 getRedBlackTree tree cs with (root tree)
|
|
417
|
76 ... | Nothing = cs tree Nothing
|
|
|
77 ... | Just d = cs stack1 (Just data1)
|
|
|
78 where
|
|
|
79 data1 = datum d
|
|
425
|
80 stack1 = record { root = (next d) }
|
