Mercurial > hg > Papers > 2018 > ryokka-sigos

comparison Paper/src/AgdaTreeImpl.agda @ 6:4312a27022d1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Mon, 23 Apr 2018 18:11:46 +0900
parents 576637483425
children
comparison
equal deleted inserted replaced
5:341b4c04597f 6:4312a27022d1
1 record Node {n : Level } (a k : Set n) : Set n where 1 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
2 inductive
3 field 2 field
4 key : k 3 putImpl : treeImpl -> a -> (treeImpl -> t) -> t
5 value : a 4 getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t
6 right : Maybe (Node a k)
7 left : Maybe (Node a k)
8 color : Color {n}
9 open Node
10 5
11 leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k 6 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
12 leafNode k1 value = record { 7 field
13 key = k1 ; 8 tree : treeImpl
14 value = value ; 9 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
15 right = Nothing ; 10 putTree : a -> (Tree treeImpl -> t) -> t
16 left = Nothing ; 11 putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
17 color = Red 12 getTree : (Tree treeImpl -> Maybe a -> t) -> t
18 } 13 getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
19 open leafNode
20 14
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