|
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
|
|
|
8 put : treeImpl -> a -> (treeImpl -> t) -> t
|
|
|
9 get : treeImpl -> (treeImpl -> Maybe a -> t) -> t
|
|
|
10
|
|
|
11 record RedBlackTree (a : Set) : Set where
|
|
|
12 field
|
|
|
13 top : Maybe (Element a)
|
|
|
14 stack : Stack
|
|
|
15 open RedBlackTree
|
|
|
16
|
|
|
17 putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
|
|
|
18 putRedBlackTree stack datum next = next newtree
|
|
|
19 where
|
|
|
20 element = cons datum (top stack)
|
|
|
21 newtree = record {top = Just element}
|
|
|
22
|
|
|
23 getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
|
|
|
24 getRedBlackTree tree cs with (top tree)
|
|
|
25 ... | Nothing = cs tree Nothing
|
|
|
26 ... | Just d = cs stack1 (Just data1)
|
|
|
27 where
|
|
|
28 data1 = datum d
|
|
|
29 stack1 = record { top = (next d) }
|
|
|
30
|
