|
7
|
1 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
|
|
|
2 field
|
|
|
3 putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
4 getImpl : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
5 open TreeMethods
|
|
|
6
|
|
|
7 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
|
|
|
8 field
|
|
|
9 tree : treeImpl
|
|
|
10 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
|
|
|
11 putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
12 putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
|
|
|
13 getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
14 getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
|
|
|
15 open Tree
|
|
|
16
|
|
|
17 record Node {n : Level } (a k : Set n) : Set n where
|
|
|
18 inductive
|
|
|
19 field
|
|
|
20 key : k
|
|
|
21 value : a
|
|
|
22 right : Maybe (Node a k)
|
|
|
23 left : Maybe (Node a k)
|
|
|
24 color : Color {n}
|
|
|
25 open Node
|
|
|
26
|
|
|
27 leafNode : {n : Level } {a k : Set n} @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k
|
|
|
28 leafNode k1 value = record {
|
|
|
29 key = k1 ;
|
|
|
30 value = value ;
|
|
|
31 right = Nothing ;
|
|
|
32 left = Nothing ;
|
|
|
33 color = Red
|
|
|
34 }
|
|
|
35 record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where
|
|
|
36 field
|
|
|
37 root : Maybe (Node a k)
|
|
|
38 nodeStack : SingleLinkedStack (Node a k)
|
|
|
39 compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n}
|
|
|
40 open RedBlackTree
|
|
|
41
|
|
|
42 putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
43 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree)
|
|
|
44 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
|
|
|
45 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next))
|
|
|
46
|
|
|
47 -- 以下省略
|
