Mercurial > hg > Gears > GearsAgda

comparison src/parallel_execution/RedBlackTree.agda @ 417:24c98ca207f4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add RedBlackTree.agda
author mir3636
date Thu, 05 Oct 2017 17:52:06 +0900
parents
children ea6353b6c4ef
comparison
equal deleted inserted replaced
416:6f873aad1b06 417:24c98ca207f4
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