|
1
|
1 record Node {n : Level } (a k : Set n) : Set n where
|
|
|
2 inductive
|
|
|
3 field
|
|
|
4 key : k
|
|
|
5 value : a
|
|
|
6 right : Maybe (Node a k)
|
|
|
7 left : Maybe (Node a k)
|
|
|
8 color : Color {n}
|
|
|
9 open Node
|
|
|
10
|
|
|
11 leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k
|
|
|
12 leafNode k1 value = record {
|
|
|
13 key = k1 ;
|
|
|
14 value = value ;
|
|
|
15 right = Nothing ;
|
|
|
16 left = Nothing ;
|
|
|
17 color = Red
|
|
|
18 }
|
|
|
19 open leafNode
|
|
|
20
|
|
|
21 record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where
|
|
|
22 field
|
|
|
23 root : Maybe (Node a k)
|
|
|
24 nodeStack : SingleLinkedStack (Node a k)
|
|
|
25 compare : k -> k -> CompareResult {n}
|
|
|
26 open RedBlackTree
|
|
|
27
|
|
|
28 putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
|
|
|
29 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree)
|
|
|
30 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
|
|
|
31 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next))
|
|
|
32
|
|
|
33 -- 以下省略
|
