Mercurial > hg > Members > Moririn

comparison RedBlackTree.agda @ 586:0ddfa505d612

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isolate search function problem, and add hoareBinaryTree.agda.
author ryokka
date Wed, 04 Dec 2019 15:42:47 +0900
parents 73fc32092b64
children 8df36383ced0
comparison
equal deleted inserted replaced
585:42e8cf963c5c 586:0ddfa505d612
214 214
215 215
216 leafNode : {n : Level } { a : Set n } → a → (k : ℕ) → (Node a k) 216 leafNode : {n : Level } { a : Set n } → a → (k : ℕ) → (Node a k)
217 leafNode v k1 = record { key = k1 ; value = v ; right = nothing ; left = nothing ; color = Red } 217 leafNode v k1 = record { key = k1 ; value = v ; right = nothing ; left = nothing ; color = Red }
218 218
219 putRedBlackTree : {n m : Level} {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → {!!} → {!!} → (RedBlackTree {n} {m} {t} a k → t) → t 219 putRedBlackTree : {n m : Level} {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → ℕ → ℕ → (RedBlackTree {n} {m} {t} a k → t) → t
220 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next with (root tree) 220 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next with (root tree)
221 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | nothing = next (record tree {root = just (leafNode {!!} {!!}) }) 221 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | nothing = next (record tree {root = just (leafNode val k1) })
222 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode {!!} {!!}) n2 (λ tree1 s n1 → insertNode tree1 s n1 next)) 222 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode {!!} {!!}) n2 (λ tree1 s n1 → insertNode tree1 s n1 next))
223 -- putRedBlackTree {n} {m} {t} {a} {k} tree value k1 next with (root tree) 223 -- putRedBlackTree {n} {m} {t} {a} {k} tree value k1 next with (root tree)
224 -- ... | nothing = next (record tree {root = just (leafNode k1 value) }) 224 -- ... | nothing = next (record tree {root = just (leafNode k1 value) })
225 -- ... | just n2 = clearSingleLinkedStack (nodeStack tree) (\ s → findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 → insertNode tree1 s n1 next)) 225 -- ... | just n2 = clearSingleLinkedStack (nodeStack tree) (\ s → findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 → insertNode tree1 s n1 next))
226 226
283 283
284 -- ( x y : ℕ ) -> Tri ( x < y ) ( x ≡ y ) ( x > y ) 284 -- ( x y : ℕ ) -> Tri ( x < y ) ( x ≡ y ) ( x > y )
285 285
286 -- test = (λ x → (createEmptyRedBlackTreeℕ x x) 286 -- test = (λ x → (createEmptyRedBlackTreeℕ x x)
287 287
288 ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0 288 -- ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0
289 289
290 -- tes = putRedBlackTree {_} {_} {_} (createEmptyRedBlackTreeℕ {_} {_} {_} 3 3) 2 2 (λ t → t) 290 -- tes = putRedBlackTree {_} {_} {_} (createEmptyRedBlackTreeℕ {_} {_} {_} 3 3) 2 2 (λ t → t)