Mercurial > hg > Gears > GearsAgda
changeset 597:89fd7cf09b2a
fix
| author | ryokka |
|---|---|
| date | Mon, 20 Jan 2020 18:12:31 +0900 |
| parents | 4be84ddbf593 |
| children | 40ffa0833d03 |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 273 insertions(+), 192 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Thu Jan 16 17:53:47 2020 +0900 +++ b/hoareBinaryTree.agda Mon Jan 20 18:12:31 2020 +0900 @@ -52,31 +52,134 @@ iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ } -{-- - data A B : C → D → Set where の A B と C → D の差は？ - - --} - -data bt {n : Level} {a : Set n} : Set n where -- (a : Setn) - bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt - bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) → - bt {n} {a} → bt {n} {a} → l ≤ l' → u' ≤ u → bt - -- -- -- no children , having left node , having right node , having both -- -data bt' {n : Level} { l r : ℕ } (A : Set n) : (key : ℕ) → Set n where -- (a : Setn) - bt'-leaf : (key : ℕ) → bt' A key - bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) → - bt' {n} {{!!}} {{!!}} A l → bt' {n} {{!!}} {{!!}} A r → l ≤ key → key ≤ r → bt' A key +data bt {n : Level} (A : Set n) : Set n where + bt-leaf : (key : ℕ) → bt A + bt-node : (key : ℕ) → + (ltree : bt A) → (rtree : bt A) → bt A + + +data bt-path {n : Level} (A : Set n) : Set n where + bt-left : (key : ℕ) → (bt A ) → bt-path A + bt-right : (key : ℕ) → (bt A ) → bt-path A + + +bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path A) + → ( bt A → List (bt-path A) → t ) → t +bt-find {n} {m} {A} {t} key leaf@(bt-leaf key₁) stack exit = exit leaf stack +bt-find {n} {m} {A} {t} key (bt-node key₁ tree tree₁) stack next with <-cmp key key₁ +bt-find {n} {m} {A} {t} key node@(bt-node key₁ tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack +bt-find {n} {m} {A} {t} key node@(bt-node key₁ ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (bt-left key node ∷ stack) next +bt-find {n} {m} {A} {t} key node@(bt-node key₁ ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (bt-right key node ∷ stack) next + -data bt'-path {n : Level} (A : Set n) : ℕ → Set n where -- (a : Setn) - bt'-left : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A left-key - bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A right-key +bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt-path A) → (bt A → t ) → t +bt-replace {n} {m} {A} {t} ikey otree stack next = bt-replace0 otree where + bt-replace1 : bt A → List (bt-path A) → t + bt-replace1 tree [] = next tree + bt-replace1 node (bt-left key (bt-leaf key₁) ∷ stack) = bt-replace1 node stack + bt-replace1 node (bt-right key (bt-leaf key₁) ∷ stack) = bt-replace1 node stack + bt-replace1 node (bt-left key (bt-node key₁ x x₁) ∷ stack) = bt-replace1 (bt-node key₁ node x₁) stack + bt-replace1 node (bt-right key (bt-node key₁ x x₁) ∷ stack) = bt-replace1 (bt-node key₁ x node) stack + bt-replace0 : (tree : bt A) → t + bt-replace0 tree@(bt-node key ltr rtr) = bt-replace1 tree stack -- find case + bt-replace0 (bt-leaf key) with <-cmp key ikey -- not-find case + bt-replace0 (bt-leaf key) | tri< a ¬b ¬c = bt-replace1 (bt-node ikey (bt-leaf key) (bt-leaf (suc ikey))) stack + bt-replace0 (bt-leaf key) | tri≈ ¬a b ¬c = bt-replace1 (bt-node ikey (bt-leaf (pred ikey)) (bt-leaf (suc ikey))) stack + bt-replace0 (bt-leaf key) | tri> ¬a ¬b c = bt-replace1 (bt-node ikey (bt-leaf (suc ikey)) (bt-leaf (key))) stack + +-- bt-replace1 (bt-node ikey (bt-leaf {!!}) (bt-leaf {!!})) stack -- not-find case + + +bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → (bt A → t ) → t +bt-insert {n} {m} {A} {t} key tree next = bt-find key tree [] (λ tr st → bt-replace key tr st (λ new → next new)) + + +tree->key : {n : Level} {A : Set n} → (tree : bt A ) → ℕ +tree->key {n} (bt-leaf key) = key +tree->key {n} (bt-node key tree tree₁) = key + +{-- +find でステップ毎にみている node と stack の top を一致させる +find 中はnode と stack の top が一致する(root に来た時 stack top がなくなる) +-- どうやって経路の入ったstackを手に入れるか?(find 実行後でよい?) +tree+stack≡tree は find 後の tree と stack をもって +reverse した stack を使って find をチェックするかんじ? +--} -test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n))) +tree+stack : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A ) + → (stack : List (bt-path A)) → Set n +tree+stack tree mtree [] = tree ≡ mtree -- fin case +tree+stack {n} {m} {A} {t} tree mtree@(bt-leaf key1) (bt-left key x ∷ stack) = (mtree ≡ x) -- unknow case +tree+stack {n} {m} {A} {t} tree mtree@(bt-leaf key₁) (bt-right key x ∷ stack) = (mtree ≡ x) -- we nofound leaf's left, right node +tree+stack {n} {m} {A} {t} tree mtree@(bt-node key1 ltree rtree) (bt-left key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree ltree stack) -- correct case +tree+stack {n} {m} {A} {t} tree mtree@(bt-node key₁ ltree rtree) (bt-right key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree rtree stack) + + +tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A ) + → (stack : List (bt-path A )) → tree+stack {_} {m} {_} {t} tree mtree (reverse stack) +tree+stack≡tree tree (bt-leaf key) stack = {!!} +tree+stack≡tree tree (bt-node key rtree ltree) stack = {!!} + + +-- loop はきっと start, running, stop の3つに分けて考えるといいよね +{-- find status + 1. find start → stack empty + 2. find loop → stack Not empty ∧ node Not empty + or "in reverse stack" ≡ "find route orig tree" + 3. find fin → "stack Not empty ∧ current node is leaf" + or "stack Not empty ∧ current node key ≡ find-key" +--} + +find-step : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt-path A)) + → (next : bt A → List (bt-path A) → (¬ (stack ≡ [])) ∧ (tree ≡ bt-leaf key) → t) + → (next : bt A → List (bt-path A) + → ((¬ (stack ≡ [])) ∧ (tree ≡ bt-leaf key) + ∨ (¬ (stack ≡ [])) ∧ (key ≡ (tree->key tree)) )→ t) → t +find-step {n} {m} {A} {t} key node stack next exit = {!!} + + +find-check : {n m : Level} {A : Set n} {t : Set m} → (k : ℕ) → (tree : bt A ) + → (stack : List (bt-path A )) → bt-find k tree [] (λ mtree mstack → tree+stack {_} {m} {_} {t} tree mtree (reverse mstack)) +find-check {n} {m} {A} {t} key (bt-leaf key₁) [] = refl +find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] with <-cmp key key₁ +find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl +find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!} +find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!} +find-check {n} {m} {A} {t} key tree (x ∷ stack) = {!!} + + +module ts where + tbt : {n : Level} {A : Set n} → bt A + tbt {n} {A} = bt-node {n} {A} 8 (bt-node 6 (bt-node 2 (bt-leaf 1) (bt-leaf 3)) (bt-leaf 7)) (bt-leaf 9) + + find : {n : Level} {A : Set n} → ℕ → List (bt-path A) + find {n} {A} key = bt-find key tbt [] (λ x y → y ) + + rep : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A + rep {n} {m} {A} {t} key = bt-find {n} {_} {A} key tbt [] (λ tr st → bt-replace key tr st (λ mtr → mtr)) + + ins : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A + ins {n} {m} {A} {t} key = bt-insert key tbt (λ tr → tr) +-- +-- +-- no children , having left node , having right node , having both +-- +-- data bt' {n : Level} { l r : ℕ } (A : Set n) : (key : ℕ) → Set n where -- (a : Setn) +-- bt'-leaf : (key : ℕ) → bt' A key +-- bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) → +-- bt' {n} {{!!}} {{!!}} A l → bt' {n} {{!!}} {{!!}} A r → l ≤ key → key ≤ r → bt' A key + +-- data bt'-path {n : Level} (A : Set n) : ℕ → Set n where -- (a : Setn) +-- bt'-left : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A left-key +-- bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A right-key + + +-- test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n))) @@ -85,83 +188,61 @@ -- reverse1 (x ∷ s0) s1 with reverse1 s0 (x ∷ s1) -- ... | as = {!!} -{-- -find でステップ毎にみている node と stack の top を一致させる -find 中はnode と stack の top が一致する(root に来た時 stack top がなくなる) --- どうやって経路の入ったstackを手に入れるか?(find 実行後でよい?) - - -tree+stack≡tree は find 後の tree と stack をもって -reverse した stack を使って find をチェックするかんじ? ---} -tree+stack : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn ) - → (stack : List (bt'-path A tn)) → Set n -tree+stack tree mtree [] = tree ≡ mtree -- fin case -tree+stack {n} {m} {A} {t} {.key₁} tree mtree@(bt'-leaf key₁) (bt'-left key x x₁ ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree {!!} stack) -tree+stack {n} {m} {A} {t} {.key₁} tree mtree@(bt'-node {l} {r} key₁ value lmtree rmtree x₂ x₃) (bt'-left key x x₁ ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} {{!!}} tree {!!} stack) -tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-right key x x₁ ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} {tn} tree {!!} stack) --- tree+stack tree mtree (bt'-right key {rkey} x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack tree {!!} stack) -- tn ≡ rkey がひつよう - -tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn ) - → (stack : List (bt'-path A tn)) → (reverse stack) ≡ {!!} -tree+stack≡tree tree (bt'-leaf key) stack = {!!} -tree+stack≡tree tree (bt'-node key value mtree mtree₁ x x₁) stack = {!!} - -bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn) - → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t -bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack -- no key found -bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁ -bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c = - bt-find' key tree ( (bt'-left key {!!} ({!!}) ) ∷ {!!}) next -bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack -bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = - bt-find' key tree ( (bt'-right key {!!} {!!} ) ∷ {!!}) next +-- bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn) +-- → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t +-- bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack -- no key found +-- bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁ +-- bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c = +-- bt-find' key tree ( (bt'-left key {!!} ({!!}) ) ∷ {!!}) next +-- bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack +-- bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = +-- bt-find' key tree ( (bt'-right key {!!} {!!} ) ∷ {!!}) next -bt-find-step : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn) - → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t -bt-find-step key tr@(bt'-leaf key₁) stack exit = exit tr stack -- no key found -bt-find-step key (bt'-node key₁ value tree tree₁ x x₁) stack next = {!!} +-- bt-find-step : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn) +-- → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t +-- bt-find-step key tr@(bt'-leaf key₁) stack exit = exit tr stack -- no key found +-- bt-find-step key (bt'-node key₁ value tree tree₁ x x₁) stack next = {!!} -a<sa : { a : ℕ } → a < suc a -a<sa {zero} = s≤s z≤n -a<sa {suc a} = s≤s a<sa +-- a<sa : { a : ℕ } → a < suc a +-- a<sa {zero} = s≤s z≤n +-- a<sa {suc a} = s≤s a<sa -a≤sa : { a : ℕ } → a ≤ suc a -a≤sa {zero} = z≤n -a≤sa {suc a} = s≤s a≤sa +-- a≤sa : { a : ℕ } → a ≤ suc a +-- a≤sa {zero} = z≤n +-- a≤sa {suc a} = s≤s a≤sa -pa<a : { a : ℕ } → pred (suc a) < suc a -pa<a {zero} = s≤s z≤n -pa<a {suc a} = s≤s pa<a +-- pa<a : { a : ℕ } → pred (suc a) < suc a +-- pa<a {zero} = s≤s z≤n +-- pa<a {suc a} = s≤s pa<a -bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A {!!}) - → ({key1 : ℕ } → bt' A key1 → t ) → t -bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where - bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A {!!}) → t - bt-replace0 node [] = next node - bt-replace0 node (bt'-left key (bt'-leaf key₁) x₁ ∷ stack) = {!!} - bt-replace0 {tn} node (bt'-left key (bt'-node key₁ value x x₂ x₃ x₄) x₁ ∷ stack) = bt-replace0 {key₁} (bt'-node key₁ value node x₂ {!!} x₄ ) stack - bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!} - bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t - bt-replace1 tn (bt'-leaf key0) = bt-replace0 (bt'-node tn value - (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ) (≤⇒pred≤ ≤-refl) a≤sa) stack - bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack +-- bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A {!!}) +-- → ({key1 : ℕ } → bt' A key1 → t ) → t +-- bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where +-- bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A {!!}) → t +-- bt-replace0 node [] = next node +-- bt-replace0 node (bt'-left key (bt'-leaf key₁) x₁ ∷ stack) = {!!} +-- bt-replace0 {tn} node (bt'-left key (bt'-node key₁ value x x₂ x₃ x₄) x₁ ∷ stack) = bt-replace0 {key₁} (bt'-node key₁ value node x₂ {!!} x₄ ) stack +-- bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!} +-- bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t +-- bt-replace1 tn (bt'-leaf key0) = bt-replace0 (bt'-node tn value +-- (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ) (≤⇒pred≤ ≤-refl) a≤sa) stack +-- bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack -tree->key : {n : Level} {tn : ℕ} → (A : Set n) → (tree : bt' A tn ) → ℕ -tree->key {n} {.key} (A) (bt'-leaf key) = key -tree->key {n} {.key} (A) (bt'-node key value tree tree₁ x x₁) = key +-- tree->key : {n : Level} {tn : ℕ} → (A : Set n) → (tree : bt' A tn ) → ℕ +-- tree->key {n} {.key} (A) (bt'-leaf key) = key +-- tree->key {n} {.key} (A) (bt'-node key value tree tree₁ x x₁) = key -bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree : bt' A tn ) → Set n -bt-find'-assert1 {n} {m} {A} {t} {tn} tree = (key : ℕ) → (val : A) → bt-find' key tree [] (λ tree1 stack → key ≡ (tree->key A tree1)) +-- bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree : bt' A tn ) → Set n +-- bt-find'-assert1 {n} {m} {A} {t} {tn} tree = (key : ℕ) → (val : A) → bt-find' key tree [] (λ tree1 stack → key ≡ (tree->key A tree1)) -bt-replace-hoare : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) - → (pre : bt-find'-assert1 {n} {m} {A} {t} tree → bt-replace' {!!} {!!} {!!} {!!} {!!}) → t -bt-replace-hoare key value tree stack = {!!} +-- bt-replace-hoare : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) +-- → (pre : bt-find'-assert1 {n} {m} {A} {t} tree → bt-replace' {!!} {!!} {!!} {!!} {!!}) → t +-- bt-replace-hoare key value tree stack = {!!} @@ -180,162 +261,162 @@ -lleaf : {n : Level} {a : Set n} → bt {n} {a} -lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n) +-- lleaf : {n : Level} {a : Set n} → bt {n} {a} +-- lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n) -lleaf1 : {n : Level} {A : Set n} → (0 < 3) → (a : A) → (d : ℕ ) → bt' {n} A d -lleaf1 0<3 a d = bt'-leaf d +-- lleaf1 : {n : Level} {A : Set n} → (0 < 3) → (a : A) → (d : ℕ ) → bt' {n} A d +-- lleaf1 0<3 a d = bt'-leaf d -test-node1 : bt' ℕ 3 -test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!}))) +-- test-node1 : bt' ℕ 3 +-- test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!}))) -rleaf : {n : Level} {a : Set n} → bt {n} {a} -rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n)))) +-- rleaf : {n : Level} {a : Set n} → bt {n} {a} +-- rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n)))) -test-node : {n : Level} {a : Set n} → bt {n} {a} -test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl ) +-- test-node : {n : Level} {a : Set n} → bt {n} {a} +-- test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl ) --- stt : {n m : Level} {a : Set n} {t : Set m} → {!!} --- stt {n} {m} {a} {t} = pushSingleLinkedStack [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) ) +-- -- stt : {n m : Level} {a : Set n} {t : Set m} → {!!} +-- -- stt {n} {m} {a} {t} = pushSingleLinkedStack [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) ) --- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい --- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる -bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t -bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing -bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d -bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg -bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) -bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg +-- -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい +-- -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる +-- bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t +-- bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing +-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d +-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg +-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) +-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg --- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg --- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) --- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg +-- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg +-- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) +-- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg --- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう -bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t -bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node +-- -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう +-- bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t +-- bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node -bt-search-test-bad : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 8 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 7) → ⊥)))) → t) → t -bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node +-- bt-search-test-bad : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 8 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 7) → ⊥)))) → t) → t +-- bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node --- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ) --- up-some (just (fst , snd)) = just fst --- up-some nothing = nothing +-- -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ) +-- -- up-some (just (fst , snd)) = just fst +-- -- up-some nothing = nothing -search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} ) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata) -search-lem {n} {m} {a} {t} key (bt-leaf x) = refl -search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d -search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄ key tree₁ -search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl -search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄ key tree₂ +-- search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} ) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata) +-- search-lem {n} {m} {a} {t} key (bt-leaf x) = refl +-- search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d +-- search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄ key tree₁ +-- search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl +-- search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄ key tree₂ --- bt-find -find-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t +-- -- bt-find +-- find-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t -find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing -find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d -find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c)) +-- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing +-- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d +-- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c)) -find-support {n} {m} {a} {t} key node@(bt-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c = - pushSingleLinkedStack st node - (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg) +-- find-support {n} {m} {a} {t} key node@(bt-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c = +-- pushSingleLinkedStack st node +-- (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg) -find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node - (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg) +-- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node +-- (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg) -bt-find : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t -bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st - (λ cst → find-support ⦃ l ⦄ ⦃ u ⦄ key tr cst cg) +-- bt-find : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t +-- bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st +-- (λ cst → find-support ⦃ l ⦄ ⦃ u ⦄ key tr cst cg) -find-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → List bt -- ? -find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st) -{-- result - λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ → - bt-node 3 (bt-leaf z≤n) (bt-leaf (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ [] ---} +-- find-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → List bt -- ? +-- find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st) +-- {-- result +-- λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ → +-- bt-node 3 (bt-leaf z≤n) (bt-leaf (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ [] +-- --} -find-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) → (st : List (bt {n} {a})) → find-support {{l}} {{u}} d tree st (λ ta st ad → ta ≡ ta) -find-lem d (bt-leaf x) st = refl -find-lem d (bt-node d₁ tree tree₁ x x₁) st with <-cmp d d₁ -find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl +-- find-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) → (st : List (bt {n} {a})) → find-support {{l}} {{u}} d tree st (λ ta st ad → ta ≡ ta) +-- find-lem d (bt-leaf x) st = refl +-- find-lem d (bt-node d₁ tree tree₁ x x₁) st with <-cmp d d₁ +-- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl -find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with tri< a ¬b ¬c -find-lem {n} {m} {a} {t} {{l}} {{u}} d (bt-node d₁ tree tree₁ x x₁) st | tri< lt ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!} -find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!} -find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!} +-- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with tri< a ¬b ¬c +-- find-lem {n} {m} {a} {t} {{l}} {{u}} d (bt-node d₁ tree tree₁ x x₁) st | tri< lt ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!} +-- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!} +-- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!} -find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!} +-- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!} -bt-singleton :{n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t -bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl) +-- bt-singleton :{n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t +-- bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl) -singleton-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? -singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x +-- singleton-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? +-- singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x -replace-helper : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → t ) → t -replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree -replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(bt-node d L R x₁ x₂) (bt-leaf x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case -replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁ -replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg -replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg -replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ x₃ subt x₄ x₅) st cg -replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case +-- replace-helper : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → t ) → t +-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree +-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(bt-node d L R x₁ x₂) (bt-leaf x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case +-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁ +-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg +-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg +-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ x₃ subt x₄ x₅) st cg +-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case -bt-replace : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ - → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) - → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t -bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg +-- bt-replace : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ +-- → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) +-- → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t +-- bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg --- 証明に insert がはいっててほしい -bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) - → ((bt {n} {a}) → t) → t +-- -- 証明に insert がはいっててほしい +-- bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) +-- → ((bt {n} {a}) → t) → t -bt-insert {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree cg = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree [] (λ tt st ad → bt-replace ⦃ l ⦄ ⦃ u ⦄ d tt st ad cg ) +-- bt-insert {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree cg = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree [] (λ tt st ad → bt-replace ⦃ l ⦄ ⦃ u ⦄ d tt st ad cg ) -pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ -pickKey (bt-leaf x) = nothing -pickKey (bt-node d tree tree₁ x x₁) = just d +-- pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ +-- pickKey (bt-leaf x) = nothing +-- pickKey (bt-node d tree tree₁ x x₁) = just d -insert-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? -insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x +-- insert-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? +-- insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x -insert-test-l : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? -insert-test-l {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 (lleaf) λ x → x +-- insert-test-l : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? +-- insert-test-l {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 (lleaf) λ x → x -insert-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) - → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 [] - (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt) ≡ just d ) ) +-- insert-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) +-- → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 [] +-- (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt) ≡ just d ) ) -insert-lem d (bt-leaf x) with <-cmp d d -- bt-insert d (bt-leaf x) (λ tree1 → {!!}) -insert-lem d (bt-leaf x) | tri< a ¬b ¬c = ⊥-elim (¬b refl) -insert-lem d (bt-leaf x) | tri≈ ¬a b ¬c = refl -insert-lem d (bt-leaf x) | tri> ¬a ¬b c = ⊥-elim (¬b refl) -insert-lem d (bt-node d₁ tree tree₁ x x₁) with <-cmp d d₁ - -- bt-insert d (bt-node d₁ tree tree₁ x x₁) (λ tree1 → {!!}) -insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d -insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) -insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl -insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) +-- insert-lem d (bt-leaf x) with <-cmp d d -- bt-insert d (bt-leaf x) (λ tree1 → {!!}) +-- insert-lem d (bt-leaf x) | tri< a ¬b ¬c = ⊥-elim (¬b refl) +-- insert-lem d (bt-leaf x) | tri≈ ¬a b ¬c = refl +-- insert-lem d (bt-leaf x) | tri> ¬a ¬b c = ⊥-elim (¬b refl) +-- insert-lem d (bt-node d₁ tree tree₁ x x₁) with <-cmp d d₁ +-- -- bt-insert d (bt-node d₁ tree tree₁ x x₁) (λ tree1 → {!!}) +-- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d +-- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) +-- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl +-- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) -insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!} - where - lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (bt-node d₁ tree tree₁ x x₁ ∷ []) (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄ (bt-node ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (bt-leaf ⦃ {!!} ⦄ ⦃ {!!} ⦄ (≤-reflexive refl)) z≤n (≤-reflexive refl)) st (λ tree1 → find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄ tt₂ ≡ just d))) - lem-helper = {!!} +-- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!} +-- where +-- lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (bt-node d₁ tree tree₁ x x₁ ∷ []) (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄ (bt-node ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (bt-leaf ⦃ {!!} ⦄ ⦃ {!!} ⦄ (≤-reflexive refl)) z≤n (≤-reflexive refl)) st (λ tree1 → find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄ tt₂ ≡ just d))) +-- lem-helper = {!!} -insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!} +-- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!}