Mercurial > hg > Members > Moririn

comparison redBlackTreeTest.agda @ 578:7bacba816277

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use list base simple stack
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 Nov 2019 16:37:27 +0900
parents 73fc32092b64
children
comparison
equal deleted inserted replaced
577:ac2293378d7a 578:7bacba816277
156 156
157 157
158 open stack.SingleLinkedStack 158 open stack.SingleLinkedStack
159 open stack.Element 159 open stack.Element
160 160
161
162 insertP : { a : Set } { t : Set } {P : Set } → ( f : ( a → t ) → t ) ( g : a → t ) ( g' : P → a → t )
163 → ( p : P )
164 → ( g ≡ g' p )
165 → f ( λ x → g' p x ) ≡ f ( λ x → g x )
166 insertP f g g' p refl = refl
167
168
161 {-# TERMINATING #-} 169 {-# TERMINATING #-}
162 inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool 170 inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool
163 inStack {l} n s with ( top s ) 171 inStack {l} n s with ( top s )
164 ... | nothing = true 172 ... | nothing = true
165 ... | just n1 with compTri (key n) (key (datum n1)) 173 ... | just n1 with compTri (key n) (key (datum n1))
166 ... | tri> _ neq _ = inStack {l} n ( record { top = next n1 } ) 174 ... | tri> _ neq _ = inStack {l} n ( record { top = next n1 } )
167 ... | tri< _ neq _ = inStack {l} n ( record { top = next n1 } ) 175 ... | tri< _ neq _ = inStack {l} n ( record { top = next n1 } )
168 ... | tri≈ _ refl _ = false 176 ... | tri≈ _ refl _ = false
169 177
170 record StackTreeInvariant ( n : Node ℕ ℕ ) 178 record StackTreeInvariant ( n : Node ℕ ℕ )
179 <<<<<<< working copy
180 ( s : SingleLinkedStack (Node ℕ ℕ) ) : Set where
181 ||||||| base
182 ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
183 =======
171 ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where 184 ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
185 >>>>>>> destination
172 field 186 field
187 <<<<<<< working copy
188 -- sti : replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT x1 (value n) ≡ True)
189 notInStack : inStack n s ≡ True → ⊥
190 ||||||| base
191 sti : replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT x1 (value n) ≡ True)
192 notInStack : inStack n s ≡ True → ⊥
193 =======
173 sti : {m : Level} → replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT {m} x1 (value n) ≡ true) 194 sti : {m : Level} → replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT {m} x1 (value n) ≡ true)
174 notInStack : {m : Level} → inStack {m} n s ≡ true → ⊥ 195 notInStack : {m : Level} → inStack {m} n s ≡ true → ⊥
196 >>>>>>> destination
175 197
176 open StackTreeInvariant 198 open StackTreeInvariant
177 199
200 <<<<<<< working copy
201 putTest1 : (n : Maybe (Node ℕ ℕ))
202 → (k : ℕ) (x : ℕ)
203 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
204 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))
205 putTest1 n k x with n
206 ... | Just n1 = lemma0
207 where
208 tree0 : (n1 : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
209 tree0 n1 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
210 lemma2 : (n1 : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s
211 → findNode (tree0 n1 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
212 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))
213 lemma2 n1 s STI with compTri k (key n1)
214 ... | tri> le eq gt with (right n1)
215 ... | Just rightNode = {!!} -- ( lemma2 rightNode ( record { top = Just ( cons n1 (top s) ) } ) (record {notInStack = {!!} } ) )
216 ... | Nothing with compTri k k
217 ... | tri≈ _ refl _ = {!!}
218 ... | tri< _ neq _ = ⊥-elim (neq refl)
219 ... | tri> _ neq _ = ⊥-elim (neq refl)
220 lemma2 n1 s STI | tri< le eq gt = {!!}
221 lemma2 n1 s STI | tri≈ le refl gt = lemma5 s ( tree0 n1 s ) n1
222 where
223 lemma5 : (s : SingleLinkedStack (Node ℕ ℕ) ) → ( t : RedBlackTree ℕ ℕ ) → ( n : Node ℕ ℕ ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) } )
224 ( \ s1 _ -> (replaceNode (tree0 n1 s1) s1 (record n1 { key = k ; value = x } ) (λ t →
225 GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
226 lemma5 s t n with (top s)
227 ... | Just n2 with compTri k k
228 ... | tri< _ neq _ = ⊥-elim (neq refl)
229 ... | tri> _ neq _ = ⊥-elim (neq refl)
230 ... | tri≈ _ refl _ = ⊥-elim ( (notInStack STI) {!!} )
231 lemma5 s t n | Nothing with compTri k k
232 ... | tri≈ _ refl _ = checkEQ x _ refl
233 ... | tri< _ neq _ = ⊥-elim (neq refl)
234 ... | tri> _ neq _ = ⊥-elim (neq refl)
235 lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 n1 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
236 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))))
237 lemma0 = lemma2 n1 (record {top = Nothing}) ( record { notInStack = {!!} } )
238 ... | Nothing = lemma1
239 where
240 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
241 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k
242 ( λ t x1 → checkT x1 x ≡ True)
243 lemma1 with compTri k k
244 ... | tri≈ _ refl _ = checkEQ x _ refl
245 ... | tri< _ neq _ = ⊥-elim (neq refl)
246 ... | tri> _ neq _ = ⊥-elim (neq refl)
247 ||||||| base
248 putTest1 : (n : Maybe (Node ℕ ℕ))
249 → (k : ℕ) (x : ℕ)
250 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
251 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))
252 putTest1 n k x with n
253 ... | Just n1 = lemma0
254 where
255 tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
256 tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
257 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s (tree0 s)
258 → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
259 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))
260 lemma2 s STI with compTri k (key n1)
261 ... | tri≈ le refl gt = lemma5 s ( tree0 s ) n1
262 where
263 lemma5 : (s : SingleLinkedStack (Node ℕ ℕ) ) → ( t : RedBlackTree ℕ ℕ ) → ( n : Node ℕ ℕ ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) } )
264 ( \ s1 _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t →
265 GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
266 lemma5 s t n with (top s)
267 ... | Just n2 with compTri k k
268 ... | tri< _ neq _ = ⊥-elim (neq refl)
269 ... | tri> _ neq _ = ⊥-elim (neq refl)
270 ... | tri≈ _ refl _ = ⊥-elim ( (notInStack STI) {!!} )
271 lemma5 s t n | Nothing with compTri k k
272 ... | tri≈ _ refl _ = checkEQ x _ refl
273 ... | tri< _ neq _ = ⊥-elim (neq refl)
274 ... | tri> _ neq _ = ⊥-elim (neq refl)
275 ... | tri> le eq gt = sti ( record { sti = {!!} ; notInStack = {!!} } )
276 ... | tri< le eq gt = {!!}
277 lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
278 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))))
279 lemma0 = lemma2 (record {top = Nothing}) ( record { sti = {!!} ; notInStack = {!!} } )
280 ... | Nothing = lemma1
281 where
282 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
283 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k
284 ( λ t x1 → checkT x1 x ≡ True)
285 lemma1 with compTri k k
286 ... | tri≈ _ refl _ = checkEQ x _ refl
287 ... | tri< _ neq _ = ⊥-elim (neq refl)
288 ... | tri> _ neq _ = ⊥-elim (neq refl)
289 =======
178 290
179 -- testn : {!!} 291 -- testn : {!!}
180 -- testn = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 292 -- testn = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2
181 -- $ λ t → putTree1 t 1 1 293 -- $ λ t → putTree1 t 1 1
182 -- $ λ t → putTree1 t 3 3 (λ ta → record {root = root ta ; nodeStack = nodeStack ta }) 294 -- $ λ t → putTree1 t 3 3 (λ ta → record {root = root ta ; nodeStack = nodeStack ta })
369 -- findNodePush 481 -- findNodePush
370 482
371 -- stack+tree が just だって言えたらよい 483 -- stack+tree が just だって言えたらよい
372 -- {}2 は orig の どっちかのNode 484 -- {}2 は orig の どっちかのNode
373 485
486 >>>>>>> destination