Mercurial > hg > Members > soto > experimental
diff rbt_t.agda @ 9:a335a903f87d
add imple
author | soto |
---|---|
date | Tue, 12 Jan 2021 21:20:16 +0900 |
parents | 5b398e84eae3 |
children | 2521da2c3c9a |
line wrap: on
line diff
--- a/rbt_t.agda Tue Dec 01 19:04:17 2020 +0900 +++ b/rbt_t.agda Tue Jan 12 21:20:16 2021 +0900 @@ -18,12 +18,14 @@ field coler : A number : B +open node record tree (A B C : Set) : Set where field key : A ltree : B rtree : C +open tree data rbt : Set where bt-empty : rbt @@ -124,9 +126,12 @@ init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit = exit record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } +--修正前 merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit node merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty ∷ varl₁) } next exit = exit node + merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit with <-cmp varn number + merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri≈ ¬a b ¬c = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl₁ } @@ -136,6 +141,17 @@ merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri< a ¬b ¬c = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl₁ } +--修正後 +merge-tree1 : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +merge-tree1 env next exit with varl env +... | [] = exit env +... | bt-empty ∷ nl = exit env +... | bt-node node₁ ∷ nl with <-cmp (varn env) (number ( key node₁ )) +... | tri≈ ¬a b ¬c = next (record env { varn = number (key node₁) ; varl = nl }) +-- next (record{ vart = vart env ; varn = number (key node₁) ; varl = nl }) +... | tri> ¬a ¬b c = next (record env { vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl }) +-- next (record{ vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl }) +... | tri< a ¬b ¬c = next (record{ vart = (bt-node record { key = key node₁ ; ltree = vart env ; rtree = rtree node₁ }) ; varn = number (key node₁) ; varl = nl }) -- insert bt-insert : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t @@ -154,6 +170,8 @@ bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a ¬b ¬c = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ∷ varl }) + + -- normal loop without termination {-# TERMINATING #-} insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t @@ -216,6 +234,12 @@ mergeP env exit = merge-tree env (λ env → skew' env (λ env → split' env (λ env → mergeP env exit)) ) exit {- +mergeP1 : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +mergeP1 record { vart = vart ; varn = varn ; varl = [] } exit = {!!} +mergeP1 record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = {!!} +-} + +{- merge-tree env (λ env → skew-bt env (λ env → merge-rotate-left env