Mercurial > hg > Gears > GearsAgda
diff hoareBinaryTree.agda @ 589:37f5826ca7d2
minor fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 06 Dec 2019 13:01:53 +0900 |
| parents | 8627d35d4bff |
| children | 7c424dd0945d |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Thu Dec 05 20:38:54 2019 +0900 +++ b/hoareBinaryTree.agda Fri Dec 06 13:01:53 2019 +0900 @@ -75,13 +75,15 @@ test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s (s≤s z≤n)))) -bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' ℕ tn ) → List (bt'-path A ) → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A ) → t ) → t -bt-find' key (bt'-leaf key₁) stack next = {!!} +bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A ) + → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A ) → 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' {n} {m} {A} {t} key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c = - bt-find' {n} {m} {A} {t} key tree ( (bt'-left {n} {A} key {key₁} {!!} {!!} ) ∷ stack) next -bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next {!!} stack -bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = {!!} +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 {key₁} tr a ) ∷ stack) 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 {key₁} tr c ) ∷ stack) next bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' ℕ tn ) → List (bt'-path A ) → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A ) → t ) → t