|
417
|
1 module RedBlackTree where
|
|
|
2
|
|
|
3 open import stack
|
|
|
4
|
|
|
5 record Tree {a t : Set} (treeImpl : Set) : Set where
|
|
|
6 field
|
|
|
7 tree : treeImpl
|
|
427
|
8 putImpl : treeImpl -> a -> (treeImpl -> t) -> t
|
|
|
9 getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t
|
|
|
10
|
|
478
|
11 open Tree
|
|
|
12
|
|
|
13
|
|
427
|
14 putTree : {a t : Set} -> Tree -> a -> (Tree -> t) -> t
|
|
478
|
15 putTree {a} {t} t0 d next = (putImpl t0) (tree t0) d (\t1 -> next (record t0 {tree = t1} ))
|
|
427
|
16
|
|
|
17 getTree : {a t : Set} -> Tree -> (Tree -> t) -> t
|
|
|
18 getTree {a} {t} t0 next = (getImpl t0) (tree t0) (\t1 -> next t0)
|
|
|
19
|
|
417
|
20
|
|
425
|
21 data Color : Set where
|
|
|
22 Red : Color
|
|
|
23 Black : Color
|
|
|
24
|
|
|
25 record Node (a : Set) : Set where
|
|
|
26 field
|
|
|
27 node : Element a
|
|
|
28 right : Maybe (Node a)
|
|
|
29 left : Maybe (Node a)
|
|
|
30 color : Color
|
|
|
31
|
|
417
|
32 record RedBlackTree (a : Set) : Set where
|
|
|
33 field
|
|
425
|
34 root : Maybe (Node a)
|
|
417
|
35 stack : Stack
|
|
425
|
36
|
|
417
|
37 open RedBlackTree
|
|
|
38
|
|
478
|
39 insertNode : ?
|
|
|
40 insertNode tree datum next = get2 (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next)
|
|
|
41
|
|
417
|
42 putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
|
|
425
|
43 putRedBlackTree tree datum next with (root tree)
|
|
|
44 ... | Nothing = insertNode tree datum next
|
|
|
45 ... | Just n = findNode tree datum n (\ tree1 -> insertNode tree1 datum next)
|
|
|
46
|
|
|
47 findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
|
|
478
|
48 findNode tree datum n next = pushStack (stack tree) n (\ s -> findNode1 (record tree {stack = s }) datum n next)
|
|
425
|
49
|
|
|
50 findNode1 : {Data t : Set} -> RedBlackTree Data -> Data -> Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
|
|
|
51 findNode1 tree datum n next with (compare datum n)
|
|
428
|
52 ... | EQ = popStack (tree stack) (\s d -> findNode3 d (record tree { root = just (record n {node = datum}); stack = s }) next)
|
|
425
|
53 ... | GT = findNode2 tree datum (right n) next
|
|
|
54 ... | LT = findNode2 tree datum (left n) next
|
|
417
|
55 where
|
|
425
|
56 findNode2 tree datum nothing next = insertNode tree datum next
|
|
427
|
57 findNode2 tree datum (just n) next = findNode (record tree {root = just n}) datum n next
|
|
428
|
58 findNode3 nothing tree next = next tree
|
|
|
59 findNode3 (just n) tree next =
|
|
478
|
60 popStack (tree stack) (\s d -> findNode3 d (record { root = record n {right = ? } }))
|
|
425
|
61
|
|
|
62
|
|
|
63 insertCase1 tree datum nothing grandparent next = next (record { root = ?; stack = createSingleLinkedStack })
|
|
|
64 insertCase1 tree datum (just parent) grandparent next = insertCase2 tree datum parent grandparent next
|
|
|
65
|
|
|
66 insertCase2 tree datum parent grandparent next with (color parent)
|
|
|
67 ... | Red = insertCase3 tree datum parent grandparent next
|
|
|
68 ... | Black = next (record { root = ?; stack = createSingleLinkedStack })
|
|
|
69
|
|
|
70 insertCase3 tree datum parent grandparent next
|
|
417
|
71
|
|
|
72 getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
|
|
425
|
73 getRedBlackTree tree cs with (root tree)
|
|
417
|
74 ... | Nothing = cs tree Nothing
|
|
|
75 ... | Just d = cs stack1 (Just data1)
|
|
|
76 where
|
|
|
77 data1 = datum d
|
|
425
|
78 stack1 = record { root = (next d) }
|
