Mercurial > hg > Papers > 2018 > ryokka-thesis

comparison final_main/src/AgdaTree.agda.replaced @ 5:eafc166804f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Capter4.2,5,1
author ryokka
date Mon, 19 Feb 2018 18:44:59 +0900
parents 12204a2c2eda
children
comparison
equal deleted inserted replaced
4:12204a2c2eda 5:eafc166804f3
13 getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t 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 ) 14 getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
15 15
16 open Tree 16 open Tree
17 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)