|
4
|
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
|
|
|
16 open Tree
|
|
|
17
|
|
|
18 data Color {n : Level } : Set n where
|
|
|
19 Red : Color
|
|
|
20 Black : Color
|
|
|
21
|
|
|
22 data CompareResult {n : Level } : Set n where
|
|
|
23 LT : CompareResult
|
|
|
24 GT : CompareResult
|
|
|
25 EQ : CompareResult
|
|
|
26
|
|
|
27 record Node {n : Level } (a k : Set n) : Set n where
|
|
|
28 inductive
|
|
|
29 field
|
|
|
30 key : k
|
|
|
31 value : a
|
|
|
32 right : Maybe (Node a k)
|
|
|
33 left : Maybe (Node a k)
|
|
|
34 color : Color {n}
|
|
|
35 open Node
|
|
|
36
|
|
|
37 record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where
|
|
|
38 field
|
|
|
39 root : Maybe (Node a k)
|
|
|
40 nodeStack : SingleLinkedStack (Node a k)
|
|
|
41 compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n}
|
|
|
42
|
|
|
43 open RedBlackTree
|
|
|
44
|
|
|
45
|
|
|
46 leafNode : {n : Level } {a k : Set n} @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k
|
|
|
47 leafNode k1 value = record {
|
|
|
48 key = k1 ;
|
|
|
49 value = value ;
|
|
|
50 right = Nothing ;
|
|
|
51 left = Nothing ;
|
|
|
52 color = Red
|
|
|
53 }
|
|
|
54
|
|
|
55 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
|
|
|
56 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree)
|
|
|
57 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
|
|
|
58 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next))
|
|
|
59
|
|
|
60 getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ (Maybe (Node a k)) @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
61 getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
|
|
|
62 module GetRedBlackTree where
|
|
|
63 search : Node a k @$\rightarrow$@ t
|
|
|
64 checkNode : Maybe (Node a k) @$\rightarrow$@ t
|
|
|
65 checkNode Nothing = cs tree Nothing
|
|
|
66 checkNode (Just n) = search n
|
|
|
67 search n with compare tree k1 (key n)
|
|
|
68 search n | LT = checkNode (left n)
|
|
|
69 search n | GT = checkNode (right n)
|
|
|
70 search n | EQ = cs tree (Just n)
|
