Mercurial > hg > Gears > GearsAgda

comparison src/parallel_execution/RedBlackTree.agda @ 522:f63a9a081b61

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove implementation from RedBlackTree.aga
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Jan 2018 09:41:27 +0900
parents e3cd5e3a01b8
children
comparison
equal deleted inserted replaced
521:e3cd5e3a01b8 522:f63a9a081b61
37 right : Maybe (Node a k) 37 right : Maybe (Node a k)
38 left : Maybe (Node a k) 38 left : Maybe (Node a k)
39 color : Color {n} 39 color : Color {n}
40 open Node 40 open Node
41 41
42 Stak : {n m : Level } (a k : Set n) (t : Set m ) -> Set (m ⊔ n) 42 record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
43 Stak {n} {m} a k t = Stack {n} {m} (Node a k) {t} (SingleLinkedStack (Node a k))
44 open Stack
45
46 record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where
47 field 43 field
48 root : Maybe (Node a k) 44 root : Maybe (Node a k)
49 nodeStack : Stak a k t 45 nodeStack : Stack {n} {m} (Node a k) {t} si
50 compare : k -> k -> CompareResult {n} 46 compare : k -> k -> CompareResult {n}
51 47
52 open RedBlackTree 48 open RedBlackTree
53 49
54 50 open Stack
55 51
56 -- 52 --
57 -- put new node at parent node, and rebuild tree to the top 53 -- put new node at parent node, and rebuild tree to the top
58 -- 54 --
59 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html 55 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
60 replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t 56 replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
61 replaceNode {n} {m} {t} {a} {k} tree s parent n0 next = popStack s ( 57 replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s (
62 \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) ) 58 \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
63 where 59 where
64 replaceNode1 : Stak a k t -> Maybe ( Node a k ) -> CompareResult -> t 60 replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t
65 replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } ) 61 replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } )
66 replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } ) 62 replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )
67 replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } ) 63 replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )
68 replaceNode1 s (Just grandParent) result with result 64 replaceNode1 s (Just grandParent) result with result
69 ... | LT = replaceNode tree s grandParent ( record parent { left = Just n0 } ) next 65 ... | LT = replaceNode tree s grandParent ( record parent { left = Just n0 } ) next
70 ... | GT = replaceNode tree s grandParent ( record parent { right = Just n0 } ) next 66 ... | GT = replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
71 ... | EQ = next tree 67 ... | EQ = next tree
72 68
73 rotateRight : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t 69 rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
74 rotateRight {n} {m} {t} {a} {k} tree s n0 parent grandParent next = {!!} 70 rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
75 71
76 rotateLeft : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t 72 rotateLeft : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
77 rotateLeft {n} {m} {t} {a} {k} tree s n0 parent grandParent next = {!!} 73 rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
78 74
79 insertCase5 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t 75 insertCase5 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
80 insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = {!!} 76 insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
81 77
82 insertCase4 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t 78 insertCase4 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
83 insertCase4 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = {!!} 79 insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
84 80
85 {-# TERMINATING #-} 81 {-# TERMINATING #-}
86 insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t 82 insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
87 insertNode {n} {m} {t} {a} {k} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 ) 83 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
88 where 84 where
89 insertCase1 : Stack (Node a k) (SingleLinkedStack (Node a k)) -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion 85 insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion
90 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html 86 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
91 insertCase3 : Stak a k t -> Node a k -> Node a k -> Node a k -> t 87 insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
92 insertCase3 s n0 parent grandParent with left grandParent | right grandParent 88 insertCase3 s n0 parent grandParent with left grandParent | right grandParent
93 ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next 89 ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
94 ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next 90 ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next
95 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent ) 91 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent )
96 ... | EQ = insertCase4 tree s n0 parent grandParent next 92 ... | EQ = insertCase4 tree s n0 parent grandParent next
97 ... | _ with color uncle 93 ... | _ with color uncle
98 ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( 94 ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s (
99 record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 ) 95 record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
100 ... | Black = insertCase4 tree s n0 parent grandParent next 96 ... | Black = insertCase4 tree s n0 parent grandParent next
101 insertCase2 : Stak a k t -> Node a k -> Node a k -> Node a k -> t 97 insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
102 insertCase2 s n0 parent grandParent with color parent 98 insertCase2 s n0 parent grandParent with color parent
103 ... | Black = replaceNode tree s grandParent n0 next 99 ... | Black = replaceNode tree s grandParent n0 next
104 ... | Red = insertCase3 s n0 parent grandParent 100 ... | Red = insertCase3 s n0 parent grandParent
105 insertCase1 s n0 Nothing Nothing = next tree 101 insertCase1 s n0 Nothing Nothing = next tree
106 insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next 102 insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
107 insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next 103 insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
108 insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent 104 insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
109 where 105 where
110 106
111 findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> t) -> t 107 findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
112 findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1) 108 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
113 where 109 where
114 findNode2 : Stak a k t -> (Maybe (Node a k)) -> t 110 findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
115 findNode2 s Nothing = next tree s n0 111 findNode2 s Nothing = next tree s n0
116 findNode2 s (Just n) = findNode tree s n0 n next 112 findNode2 s (Just n) = findNode tree s n0 n next
117 findNode1 : Stak a k t -> (Node a k) -> t 113 findNode1 : Stack (Node a k) si -> (Node a k) -> t
118 findNode1 s n1 with (compare tree (key n0) (key n1)) 114 findNode1 s n1 with (compare tree (key n0) (key n1))
119 ... | EQ = next tree s n0 115 ... | EQ = next tree s n0
120 ... | GT = findNode2 s (right n1) 116 ... | GT = findNode2 s (right n1)
121 ... | LT = findNode2 s (left n1) 117 ... | LT = findNode2 s (left n1)
122 118
128 right = Nothing ; 124 right = Nothing ;
129 left = Nothing ; 125 left = Nothing ;
130 color = Black 126 color = Black
131 } 127 }
132 128
133 putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree a k -> k -> a -> (RedBlackTree a k -> t) -> t 129 putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
134 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) 130 putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
135 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) 131 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
136 ... | Just n2 = findNode tree (nodeStack tree) (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next) 132 ... | Just n2 = findNode tree (nodeStack tree) (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)
137 133
138 getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> (RedBlackTree a k -> (Maybe (Node a k)) -> t) -> t 134 getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t
139 getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree) 135 getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
140 where 136 where
141 checkNode : Maybe (Node a k) -> t 137 checkNode : Maybe (Node a k) -> t
142 checkNode Nothing = cs tree Nothing 138 checkNode Nothing = cs tree Nothing
143 checkNode (Just n) = search n 139 checkNode (Just n) = search n
144 where 140 where