Mercurial > hg > Members > Moririn
annotate hoareBinaryTree.agda @ 600:016a8deed93d
fix old binary tree
| author | ryokka |
|---|---|
| date | Wed, 04 Mar 2020 17:51:05 +0900 |
| parents | 89fd7cf09b2a |
| children | 803c423c2855 |
| rev | line source |
|---|---|
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
1 module hoareBinaryTree where |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
2 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
3 open import Level renaming (zero to Z ; suc to succ) |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
4 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
5 open import Data.Nat hiding (compare) |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
6 open import Data.Nat.Properties as NatProp |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
7 open import Data.Maybe |
| 588 | 8 -- open import Data.Maybe.Properties |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
9 open import Data.Empty |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
10 open import Data.List |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
11 open import Data.Product |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
12 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
13 open import Function as F hiding (const) |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
14 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
15 open import Relation.Binary |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
16 open import Relation.Binary.PropositionalEquality |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
17 open import Relation.Nullary |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
18 open import logic |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
19 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
20 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
21 SingleLinkedStack = List |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
22 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
23 emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
24 emptySingleLinkedStack = [] |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
25 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
26 clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data → ( SingleLinkedStack Data → t) → t |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
27 clearSingleLinkedStack [] cg = cg [] |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
28 clearSingleLinkedStack (x ∷ as) cg = cg [] |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
29 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
30 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
31 pushSingleLinkedStack stack datum next = next ( datum ∷ stack ) |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
32 |
| 587 | 33 |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
34 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
35 popSingleLinkedStack [] cs = cs [] nothing |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
36 popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1) |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
37 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
38 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
39 |
| 587 | 40 emptySigmaStack : {n : Level } { Data : Set n} → List Data |
| 41 emptySigmaStack = [] | |
| 42 | |
| 43 pushSigmaStack : {n m : Level} {d d2 : Set n} {t : Set m} → d2 → List d → (List (d × d2) → t) → t | |
| 44 pushSigmaStack {n} {m} {d} d2 st next = next (Data.List.zip (st) (d2 ∷ []) ) | |
| 45 | |
| 46 tt = pushSigmaStack 3 (true ∷ []) (λ st → st) | |
| 47 | |
| 588 | 48 _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set |
| 49 d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d)) | |
| 50 | |
| 51 iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y | |
| 52 iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ } | |
| 53 | |
| 54 | |
| 590 | 55 -- |
| 56 -- | |
| 57 -- no children , having left node , having right node , having both | |
| 58 -- | |
| 597 | 59 data bt {n : Level} (A : Set n) : Set n where |
| 600 | 60 L : bt A |
| 61 N : (key : ℕ) → | |
| 62 (ltree : bt A ) → (rtree : bt A ) → bt A | |
| 63 | |
| 64 | |
| 65 -- data bt-path {n : Level} (A : Set n) : Set n where | |
| 66 -- bt-left : (key : ℕ) → (bt A ) → bt-path A | |
| 67 -- bt-right : (key : ℕ) → (bt A ) → bt-path A | |
| 68 | |
| 69 data bt-path' {n : Level} (A : Set n) : Set n where | |
| 70 left : (bt A) → bt-path' A | |
| 71 right : (bt A) → bt-path' A | |
| 72 | |
| 73 | |
| 74 | |
| 75 tree->key : {n : Level} {A : Set n} → (tree : bt A) → ℕ | |
| 76 tree->key {n} L = zero | |
| 77 tree->key {n} (N key tree tree₁) = key | |
| 78 | |
| 79 -- path2tree : {n : Level} {A : Set n} → (bt-path' {n} A) → bt A | |
| 80 -- path2tree {n} {A} (left x) = x | |
| 81 -- path2tree {n} {A} (right x) = x | |
| 82 | |
| 83 | |
| 84 -- bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path A) | |
| 85 -- → ( bt A → List (bt-path A) → t ) → t | |
| 86 -- bt-find {n} {m} {A} {t} key leaf@(L) stack exit = exit leaf stack | |
| 87 -- bt-find {n} {m} {A} {t} key (N key₁ tree tree₁) stack next with <-cmp key key₁ | |
| 88 -- bt-find {n} {m} {A} {t} key node@(N key₁ tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack | |
| 89 -- bt-find {n} {m} {A} {t} key node@(N key₁ ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (bt-left key node ∷ stack) next | |
| 90 -- bt-find {n} {m} {A} {t} key node@(N key₁ ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (bt-right key node ∷ stack) next | |
| 91 | |
| 92 | |
| 93 -- 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 | |
| 94 -- bt-find' key leaf@(L) stack exit = exit leaf stack | |
| 95 -- bt-find' key node@(N key1 lnode rnode) stack exit with <-cmp key key1 | |
| 96 -- bt-find' key node@(N key1 lnode rnode) stack exit | tri≈ ¬a b ¬c = exit node stack | |
| 97 -- bt-find' key node@(N key1 lnode rnode) stack next | tri< a ¬b ¬c = bt-find' key lnode ((left node) ∷ stack) next | |
| 98 -- bt-find' key node@(N key1 lnode rnode) stack next | tri> ¬a ¬b c = bt-find' key rnode ((right node) ∷ stack) next | |
| 597 | 99 |
| 100 | |
| 600 | 101 -- find-next : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path' A) |
| 102 -- → (next : bt A → List (bt-path' A) → t ) → (exit : bt A → List (bt-path' A) → t ) → t | |
| 103 -- find-next key leaf@(L) st _ exit = exit leaf st | |
| 104 -- find-next key (N key₁ tree tree₁) st next exit with <-cmp key key₁ | |
| 105 -- find-next key node@(N key₁ tree tree₁) st _ exit | tri≈ ¬a b ¬c = exit node st | |
| 106 -- find-next key node@(N key₁ tree tree₁) st next _ | tri< a ¬b ¬c = next tree ((left node) ∷ st) | |
| 107 -- find-next key node@(N key₁ tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ ((right node) ∷ st) | |
| 108 | |
| 109 -- find-loop は bt-find' とだいたい一緒(induction してるくらい) | |
| 110 -- これも多分 Zコンビネータの一種? | |
| 111 -- loop で induction してる hight は現在の木の最大長より大きければよい(find-next が抜けきるため) | |
| 112 -- 逆に木の最大長より小さい(たどるルートより小さい)場合は途中経過の値が返る | |
| 113 | |
| 114 -- find-loop : {n m : Level} {A : Set n} {t : Set m} → (hight key : ℕ) → (tree : bt A ) → List (bt-path' A) → (exit : bt A → List (bt-path' A) → t) → t | |
| 115 -- find-loop zero key tree st exit = exit tree st | |
| 116 -- find-loop (suc h) key lf@(L) st exit = exit lf st | |
| 117 -- find-loop (suc h) key tr@(N key₁ tree tree₁) st exit = find-next key tr st ((λ tr1 st1 → find-loop h key tr1 st1 exit)) exit | |
| 118 | |
| 597 | 119 |
| 120 | |
| 600 | 121 node-ex : {n : Level} {A : Set n} → bt A |
| 122 node-ex {n} {A} = (N zero (L) (L)) | |
| 123 | |
| 124 ex : {n : Level} {A : Set n} → bt A | |
| 125 ex {n} {A} = (N {n} {A} 8 (N 6 (N 2 (N 1 L L) (N 3 L L)) (N 7 L L)) (N 9 L L)) | |
| 126 | |
| 127 exLR : {n : Level} {A : Set n} → bt A | |
| 128 exLR {n} {A} = (N {n} {A} 4 (N 2 L (N 3 L L)) (N 5 L L)) | |
| 129 | |
| 130 exRL : {n : Level} {A : Set n} → bt A | |
| 131 exRL {n} {A} = (N {n} {A} 3 L (N 5 (N 4 L L) L)) | |
| 132 | |
| 133 | |
| 134 | |
| 135 | |
| 136 leaf-ex : {n : Level} {A : Set n} → bt A | |
| 137 leaf-ex {n} {A} = L | |
| 138 | |
| 139 | |
| 140 | |
| 141 | |
| 142 | |
| 143 | |
| 144 findLoopInv : {n m : Level} {A : Set n} {t : Set m} → (orig : bt A) → (modify : bt A ) | |
| 145 → (stack : List (bt-path' A)) → Set n | |
| 146 -- findLoopInv {n} {m} {A} {t} tree mtree [] = tree ≡ mtree | |
| 147 -- findLoopInv {n} {m} {A} {t} tree mtree (left (L) ∷ st) = mtree ≡ (L) | |
| 148 -- findLoopInv {n} {m} {A} {t} tree mtree (right (L) ∷ st) = mtree ≡ (L) | |
| 149 findLoopInv {n} {m} {A} {t} tree mtree [] = tree ≡ mtree | |
| 150 findLoopInv {n} {m} {A} {t} tree mtree (left L ∷ st) = mtree ≡ (L) | |
| 151 findLoopInv {n} {m} {A} {t} tree mtree (right L ∷ st) = mtree ≡ (L) | |
| 152 findLoopInv {n} {m} {A} {t} tree mtree (left (N key x x₁) ∷ st) = mtree ≡ x | |
| 153 findLoopInv {n} {m} {A} {t} tree mtree (right (N key x x₁) ∷ st) = mtree ≡ x₁ | |
| 154 | |
| 155 | |
| 156 | |
| 157 | |
| 158 | |
| 597 | 159 |
| 588 | 160 |
| 600 | 161 |
| 162 | |
| 163 hightMerge : {n m : Level} {A : Set n} {t : Set m} → (l r : ℕ) → (ℕ → t) → t | |
| 164 hightMerge lh rh next with <-cmp lh rh | |
| 165 hightMerge lh rh next | tri< a ¬b ¬c = next rh | |
| 166 hightMerge lh rh next | tri≈ ¬a b ¬c = next lh | |
| 167 hightMerge lh rh next | tri> ¬a ¬b c = next lh | |
| 168 | |
| 169 isHightL : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t | |
| 170 isHightL L next = next zero | |
| 171 isHightL {n} {_} {A} (N key tree tree₁) next = isHightL tree λ x → next (suc x) | |
| 172 | |
| 173 isHightR : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t | |
| 174 isHightR L next = next zero | |
| 175 isHightR {n} {_} {A} (N key tree tree₁) next = isHightR tree₁ λ x → next (suc x) | |
| 176 | |
| 177 isHight : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t | |
| 178 isHight L next = next zero | |
| 179 isHight {n} {_} {A} tr@(N key tree tree₁) next = isHightL tr (λ lh → isHightR tr λ rh → hightMerge {n} {_} {A} (suc lh) (suc rh) next) | |
| 180 | |
| 597 | 181 |
| 600 | 182 treeHight : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t |
| 183 treeHight L next = next zero | |
| 184 treeHight {n} {_} {A} (N key tree tree₁) next = isHight tree (λ lh → isHight tree₁ (λ rh → hightMerge {n} {_} {A} (lh) (rh) next)) | |
| 185 | |
| 186 rhight : {n : Level} {A : Set n} → bt A → ℕ | |
| 187 rhight L = zero | |
| 188 rhight (N key tree tree₁) with <-cmp (rhight tree) (rhight tree₁) | |
| 189 rhight (N key tree tree₁) | tri< a ¬b ¬c = suc (rhight tree₁) | |
| 190 rhight (N key tree tree₁) | tri≈ ¬a b ¬c = suc (rhight tree₁) | |
| 191 rhight (N key tree tree₁) | tri> ¬a ¬b c = suc (rhight tree) | |
| 192 | |
| 193 leaf≠node : {n : Level} {A : Set n} {a : ℕ} {l r : bt A} → ((N {n} {A} a l r) ≡ L) → ⊥ | |
| 194 leaf≠node () | |
| 195 | |
| 196 leafIsNoHight : {n : Level} {A : Set n} (tree : bt A) → tree ≡ L → (treeHight tree (λ x → x) ≡ 0) | |
| 197 leafIsNoHight L refl = refl | |
| 198 | |
| 199 | |
| 200 | |
| 201 hight-tree : {n : Level} {A : Set n} {k : ℕ} {l r : bt A} → ℕ → (tree : bt A) → Set n | |
| 202 hight-tree zero tree = tree ≡ L | |
| 203 hight-tree {n} {A} {k} {l} {r} (suc h) tree = tree ≡ (N k l r) | |
| 597 | 204 |
| 205 | |
| 600 | 206 hightIsNotLeaf : {n : Level} {A : Set n} (h : ℕ) → (tree : bt A) → (h ≡ 0 ) ∧ (h ≡ treeHight tree (λ x → x)) → (tree ≡ L) |
| 207 hightIsNotLeaf .0 tree record { proj1 = refl ; proj2 = p2 } = {!!} | |
| 208 | |
| 209 -- leaf≡0 : {n : Level} {A : Set n} (tree : bt A) → (rhight tree ≡ 0) → tree ≡ L | |
| 210 -- leaf≡0 L _ = refl | |
| 211 | |
| 212 | |
| 213 | |
| 214 | |
| 215 | |
| 216 | |
| 217 | |
| 597 | 218 |
| 219 | |
| 600 | 220 find-hoare-next : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mt : bt A ) → (st : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree mt st) |
| 221 → (next : (nt : bt A) → (ns : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree nt ns) → t ) | |
| 222 → (exit : (nt : bt A) → (ns : List (bt-path' A)) → (nt ≡ L) ∨ (key ≡ tree->key nt) → t ) → t | |
| 223 find-hoare-next key leaf@(L) mt st eq _ exit = exit leaf st (case1 refl) | |
| 224 find-hoare-next key (N key₁ tree tree₁) mt st eq next exit with <-cmp key key₁ | |
| 225 find-hoare-next key node@(N key₁ tree tree₁) mt st eq _ exit | tri≈ ¬a b ¬c = exit node st (case2 b) | |
| 226 find-hoare-next key node@(N key₁ tree tree₁) mt st eq next _ | tri< a ¬b ¬c = next tree ((left node) ∷ st) refl | |
| 227 find-hoare-next key node@(N key₁ tree tree₁) mt st eq next _ | tri> ¬a ¬b c = next tree₁ ((right node) ∷ st) refl | |
| 228 | |
| 229 find-hoare-loop : {n m : Level} {A : Set n} {t : Set m} → (hight key : ℕ) → (tree mt : bt A ) → (st : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree mt st) | |
| 230 → (exit : (nt : bt A) → (ns : List (bt-path' A)) → (nt ≡ L) ∨ (key ≡ tree->key nt) → t) → t | |
| 231 find-hoare-loop zero key tree mt st eq exit with key ≟ (tree->key tree) | |
| 232 find-hoare-loop zero key tree mt st eq exit | yes p = exit tree st (case2 p) | |
| 233 find-hoare-loop zero key tree mt st eq exit | no ¬p = exit tree st (case1 {!!}) | |
| 234 | |
| 235 find-hoare-loop (suc h) key otr lf@(L) st eq exit = exit lf st (case1 refl) | |
| 236 find-hoare-loop (suc h) key otr tr@(N key₁ tree tree₁) st eq exit = find-hoare-next key otr tr st {!!} ((λ tr1 st1 eq → find-hoare-loop h key otr tr1 st1 {!!} exit)) exit | |
| 237 | |
| 238 | |
| 239 -- bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt-path A) → (bt A → t ) → t | |
| 240 -- bt-replace {n} {m} {A} {t} ikey otree stack next = bt-replace0 otree where | |
| 241 -- bt-replace1 : bt A → List (bt-path A) → t | |
| 242 -- bt-replace1 tree [] = next tree | |
| 243 -- bt-replace1 node (bt-left key (L) ∷ stack) = bt-replace1 node stack | |
| 244 -- bt-replace1 node (bt-right key (L) ∷ stack) = bt-replace1 node stack | |
| 245 -- bt-replace1 node (bt-left key (N key₁ x x₁) ∷ stack) = bt-replace1 (N key₁ node x₁) stack | |
| 246 -- bt-replace1 node (bt-right key (N key₁ x x₁) ∷ stack) = bt-replace1 (N key₁ x node) stack | |
| 247 -- bt-replace0 : (tree : bt A) → t | |
| 248 -- bt-replace0 tree@(N key ltr rtr) = bt-replace1 tree stack -- find case | |
| 249 -- bt-replace0 (L) = {!!} | |
| 250 | |
| 251 | |
| 252 | |
| 253 -- bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → (bt A → t ) → t | |
| 254 -- bt-insert {n} {m} {A} {t} key tree next = bt-find key tree [] (λ tr st → bt-replace key tr st (λ new → next new)) | |
| 255 | |
| 597 | 256 |
| 257 {-- | |
| 600 | 258 [ok] find でステップ毎にみている node と stack の top を一致させる |
| 259 [ok] find 中はnode と stack の top が一致する(pre は stack の中身がなく, post は stack の top とずれる) | |
| 260 | |
| 597 | 261 tree+stack≡tree は find 後の tree と stack をもって |
| 262 reverse した stack を使って find をチェックするかんじ? | |
| 263 --} | |
| 588 | 264 |
| 600 | 265 {-- |
| 266 tree+stack は tree と stack を受け取ってひとしさ(関係)を返すやつ | |
| 588 | 267 |
| 600 | 268 --} |
| 269 | |
| 270 -- tree+stack : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A ) | |
| 271 -- → (stack : List (bt-path A)) → Set n | |
| 272 -- tree+stack tree mtree [] = tree ≡ mtree -- fin case | |
| 273 -- tree+stack {n} {m} {A} {t} tree mtree@(L) (bt-left key x ∷ stack) = (mtree ≡ x) -- unknow case | |
| 274 -- tree+stack {n} {m} {A} {t} tree mtree@(L) (bt-right key x ∷ stack) = (mtree ≡ x) -- we nofound leaf's left, right node | |
| 275 -- tree+stack {n} {m} {A} {t} tree mtree@(N key1 ltree rtree) (bt-left key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree ltree stack) -- correct case | |
| 276 -- tree+stack {n} {m} {A} {t} tree mtree@(N key₁ ltree rtree) (bt-right key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree rtree stack) | |
| 277 | |
| 278 {-- | |
| 279 tree+stack | |
| 280 2. find loop → "top of reverse stack" ≡ "find route orig tree" | |
| 281 --} | |
| 282 | |
| 283 -- s+t≡t : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt-path' {n} A)) → bt-find' key tree stack (λ mt st → s+t {n} {A} tree mt st) | |
| 284 -- s+t≡t {n} {m} {A} {t} key (L) [] = refl | |
| 285 -- s+t≡t {n} {m} {A} {t} key (L) (left x ∷ []) = refl | |
| 286 -- s+t≡t {n} {m} {A} {t} key (L) (left x ∷ x₁ ∷ stack) = refl | |
| 287 -- s+t≡t {n} {m} {A} {t} key (L) (right x ∷ []) = refl | |
| 288 -- s+t≡t {n} {m} {A} {t} key (L) (right x ∷ x₁ ∷ stack) = refl | |
| 289 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] with <-cmp key key₁ | |
| 290 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl | |
| 291 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!} | |
| 292 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!} | |
| 293 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) (x ∷ stack) = {!!} | |
| 294 | |
| 597 | 295 |
| 296 | |
| 600 | 297 -- s+t : {n : Level} {A : Set n} → (tree mtree : bt A ) → (stack : List (bt-path' {n} A)) → Set n |
| 298 -- s+t tree mtree [] = tree ≡ mtree | |
| 299 -- s+t tree mtree (x ∷ []) = tree ≡ mtree | |
| 300 -- s+t tr@(L) mt (left x ∷ x₁ ∷ stack) = tr ≡ mt | |
| 301 -- s+t {n} {A} tr@(N key tree tree₁) mt (left x ∷ x₁ ∷ stack) = (mt ≡ x) ∧ (s+t {n} {A} tree (path2tree x₁) stack) | |
| 302 -- s+t tr@(L) mt (right x ∷ x₁ ∷ stack) = tr ≡ mt | |
| 303 -- s+t {n} {A} tr@(N key tree tree₁) mt (right x ∷ x₁ ∷ stack) = (mt ≡ x) ∧ (s+t {n} {A} tree₁ (path2tree x₁) stack) | |
| 304 | |
| 305 -- data treeType {n : Level} (A : Set n) : Set n where | |
| 306 -- leaf-t : treeType A | |
| 307 -- node-t : treeType A | |
| 308 | |
| 309 -- isType : {n : Level} {A : Set n} → bt A → treeType A | |
| 310 -- isType (L) = leaf-t | |
| 311 -- isType (N key tree tree₁) = node-t | |
| 312 | |
| 313 -- data findState : Set where | |
| 314 -- s1 : findState | |
| 315 -- s2 : findState | |
| 316 -- sf : findState | |
| 317 | |
| 318 -- findStateP : {n : Level} {A : Set n} → findState → ℕ → bt A → (mnode : bt A) → List (bt-path' A) → Set n | |
| 319 -- findStateP s1 key node mnode stack = stack ≡ [] | |
| 320 -- findStateP s2 key node mnode stack = (s+t node mnode (reverse stack)) | |
| 321 -- findStateP sf key node mnode stack = (key ≡ (tree->key mnode)) ∨ ((isType mnode) ≡ leaf-t) | |
| 322 | |
| 323 -- findStartPwP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (findStateP s1 key tree mtree [] → t) → t | |
| 324 -- findStartPwP key tree mtree next = next refl | |
| 325 | |
| 326 | |
| 327 | |
| 328 -- findLoopPwP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (st : List (bt-path' A)) | |
| 329 -- → (findStateP s2 key tree mtree st) | |
| 330 -- → (next : (tr : bt A) → (st : List (bt-path' A)) → (findStateP s2 key tree mtree st) → t) | |
| 331 -- → (exit : (tr : bt A) → (st : List (bt-path' A)) → (findStateP sf key tree mtree st) → t ) → t | |
| 332 -- findLoopPwP key tree (L) [] state next exit = exit tree [] (case2 refl) | |
| 333 -- findLoopPwP key tree (N key₁ mtree mtree₁) [] state next exit = next tree [] {!!} | |
| 334 -- findLoopPwP key tree mtree (x ∷ []) state next exit = {!!} | |
| 335 -- findLoopPwP key tree (L) (x ∷ x₁ ∷ stack) state next exit = {!!} | |
| 336 -- findLoopPwP key tree (N key₁ mtree mtree₁) (left x ∷ x₁ ∷ stack) state next exit = | |
| 337 -- next {!!} {!!} {!!} | |
| 338 -- findLoopPwP key tree (N key₁ mtree mtree₁) (right x ∷ x₁ ∷ stack) state next exit = {!!} | |
| 339 | |
| 340 | |
| 341 -- -- tree+stack' {n} {m} {A} {t} (N key ltree rtree) mtree@(N key₁ lmtree rmtree) (x ∷ stack) with <-cmp key key₁ | |
| 342 -- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) (x ∷ stack) | tri≈ ¬a b ¬c = tt ≡ mt | |
| 343 -- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) st@(x ∷ stack) | tri< a ¬b ¬c = (mt ≡ x) ∧ tree+stack' {n} {m} {A} {t} tt lmtree (mt ∷ st) | |
| 344 -- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) st@(x ∷ stack) | tri> ¬a ¬b c = (mt ≡ x) ∧ tree+stack' {n} {m} {A} {t} tt rmtree (mt ∷ st) | |
| 345 | |
| 346 | |
| 347 | |
| 348 -- tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A ) | |
| 349 -- → (stack : List (bt-path A )) → tree+stack {_} {m} {_} {t} tree mtree (reverse stack) | |
| 350 -- tree+stack≡tree tree (L key) stack = {!!} | |
| 351 -- tree+stack≡tree tree (N key rtree ltree) stack = {!!} | |
| 352 | |
| 597 | 353 |
| 354 | |
| 355 -- loop はきっと start, running, stop の3つに分けて考えるといいよね | |
| 356 {-- find status | |
| 357 1. find start → stack empty | |
| 358 2. find loop → stack Not empty ∧ node Not empty | |
| 359 or "in reverse stack" ≡ "find route orig tree" | |
| 360 3. find fin → "stack Not empty ∧ current node is leaf" | |
| 361 or "stack Not empty ∧ current node key ≡ find-key" | |
| 362 --} | |
| 363 | |
| 600 | 364 -- find-step : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A) → (stack : List (bt A)) |
| 365 -- → (next : (mtree : bt A) → (stack1 : List (bt A)) → (tree+stack' {n} {m} {A} {t} tree mtree stack1 ) → t) | |
| 366 -- → (exit : (mtree : bt A) → List (bt A) → (tree ≡ L (tree->key mtree )) ∨ (key ≡ (tree->key mtree)) → t) → t | |
| 367 -- find-step {n} {m} {A} {t} key (L) stack next exit = exit (L) stack (case1 refl) | |
| 368 -- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit with <-cmp key key₁ | |
| 369 -- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri≈ ¬a b ¬c = exit (N key₁ node node₁) stack (case2 b) | |
| 370 -- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri< a ¬b ¬c = next node stack {!!} | |
| 371 -- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri> ¬a ¬b c = next node₁ stack {!!} | |
| 372 | |
| 373 | |
| 374 -- find-check : {n m : Level} {A : Set n} {t : Set m} → (k : ℕ) → (tree : bt A ) | |
| 375 -- → (stack : List (bt-path A )) → bt-find k tree [] (λ mtree mstack → tree+stack {_} {m} {_} {t} tree mtree (reverse mstack)) | |
| 376 -- find-check {n} {m} {A} {t} key (L) [] = refl | |
| 377 -- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] with <-cmp key key₁ | |
| 378 -- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl | |
| 379 -- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!} | |
| 380 -- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!} | |
| 381 -- find-check {n} {m} {A} {t} key tree (x ∷ stack) = {!!} | |
| 597 | 382 |
| 383 | |
| 600 | 384 -- module ts where |
| 385 -- tbt : {n : Level} {A : Set n} → bt A | |
| 386 -- tbt {n} {A} = N {n} {A} 8 (N 6 (N 2 (L) (L)) (L)) (L) | |
| 597 | 387 |
| 600 | 388 -- find : {n : Level} {A : Set n} → ℕ → List (bt-path A) |
| 389 -- find {n} {A} key = bt-find key tbt [] (λ x y → y ) | |
| 390 | |
| 391 -- find' : {n : Level} {A : Set n} → ℕ → bt A | |
| 392 -- find' {n} {A} key = bt-find' key tbt [] (λ x y → x ) | |
| 597 | 393 |
| 600 | 394 -- rep : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A |
| 395 -- rep {n} {m} {A} {t} key = bt-find {n} {_} {A} key tbt [] (λ tr st → bt-replace key tr st (λ mtr → mtr)) | |
| 597 | 396 |
| 600 | 397 -- ins : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A |
| 398 -- ins {n} {m} {A} {t} key = bt-insert key tbt (λ tr → tr) | |
| 597 | 399 |
| 600 | 400 -- test : {n m : Level} {A : Set n} {t : Set m} (key : ℕ) |
| 401 -- → bt-find {n} {_} {A} {_} key tbt [] (λ x y → tree+stack {n} {m} {A} {t} tbt x y) | |
| 402 -- test key = {!!} | |
| 403 -- -- | |
| 597 | 404 -- |
| 405 -- no children , having left node , having right node , having both | |
| 406 -- | |
| 600 | 407 data bt' {n : Level} (A : Set n) : (key : ℕ) → Set n where -- (a : Setn) |
| 408 bt'-leaf : (key : ℕ) → bt' A key | |
| 409 bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) → | |
| 410 bt' A l → bt' A r → l ≤ key → key ≤ r → bt' A key | |
| 597 | 411 |
| 412 -- data bt'-path {n : Level} (A : Set n) : ℕ → Set n where -- (a : Setn) | |
| 413 -- bt'-left : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A left-key | |
| 414 -- bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A right-key | |
| 415 | |
| 416 | |
| 417 -- test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n))) | |
| 588 | 418 |
| 594 | 419 |
| 420 | |
| 421 -- reverse1 : List (bt' A tn) → List (bt' A tn) → List (bt' A tn) | |
| 600 | 422 -- reverse1 [] s1 = s1+ |
| 594 | 423 -- reverse1 (x ∷ s0) s1 with reverse1 s0 (x ∷ s1) |
| 424 -- ... | as = {!!} | |
| 425 | |
| 426 | |
| 596 | 427 |
| 597 | 428 -- bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn) |
| 429 -- → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t | |
| 430 -- bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack -- no key found | |
| 431 -- bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁ | |
| 432 -- bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c = | |
| 433 -- bt-find' key tree ( (bt'-left key {!!} ({!!}) ) ∷ {!!}) next | |
| 434 -- bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack | |
| 435 -- bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = | |
| 436 -- bt-find' key tree ( (bt'-right key {!!} {!!} ) ∷ {!!}) next | |
| 588 | 437 |
| 594 | 438 |
| 597 | 439 -- bt-find-step : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn) |
| 440 -- → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t | |
| 441 -- bt-find-step key tr@(bt'-leaf key₁) stack exit = exit tr stack -- no key found | |
| 442 -- bt-find-step key (bt'-node key₁ value tree tree₁ x x₁) stack next = {!!} | |
| 594 | 443 |
| 597 | 444 -- a<sa : { a : ℕ } → a < suc a |
| 445 -- a<sa {zero} = s≤s z≤n | |
| 446 -- a<sa {suc a} = s≤s a<sa | |
| 588 | 447 |
| 597 | 448 -- a≤sa : { a : ℕ } → a ≤ suc a |
| 449 -- a≤sa {zero} = z≤n | |
| 450 -- a≤sa {suc a} = s≤s a≤sa | |
| 592 | 451 |
| 597 | 452 -- pa<a : { a : ℕ } → pred (suc a) < suc a |
| 453 -- pa<a {zero} = s≤s z≤n | |
| 454 -- pa<a {suc a} = s≤s pa<a | |
| 590 | 455 |
| 597 | 456 -- bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A {!!}) |
| 457 -- → ({key1 : ℕ } → bt' A key1 → t ) → t | |
| 458 -- bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where | |
| 459 -- bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A {!!}) → t | |
| 460 -- bt-replace0 node [] = next node | |
| 461 -- bt-replace0 node (bt'-left key (bt'-leaf key₁) x₁ ∷ stack) = {!!} | |
| 462 -- 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 | |
| 463 -- bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!} | |
| 464 -- bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t | |
| 465 -- bt-replace1 tn (bt'-leaf key0) = bt-replace0 (bt'-node tn value | |
| 466 -- (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ) (≤⇒pred≤ ≤-refl) a≤sa) stack | |
| 467 -- bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack | |
| 588 | 468 |
| 597 | 469 -- tree->key : {n : Level} {tn : ℕ} → (A : Set n) → (tree : bt' A tn ) → ℕ |
| 470 -- tree->key {n} {.key} (A) (bt'-leaf key) = key | |
| 471 -- tree->key {n} {.key} (A) (bt'-node key value tree tree₁ x x₁) = key | |
| 593 | 472 |
| 473 | |
| 597 | 474 -- bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree : bt' A tn ) → Set n |
| 475 -- bt-find'-assert1 {n} {m} {A} {t} {tn} tree = (key : ℕ) → (val : A) → bt-find' key tree [] (λ tree1 stack → key ≡ (tree->key A tree1)) | |
| 593 | 476 |
| 477 | |
| 597 | 478 -- bt-replace-hoare : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) |
| 479 -- → (pre : bt-find'-assert1 {n} {m} {A} {t} tree → bt-replace' {!!} {!!} {!!} {!!} {!!}) → t | |
| 480 -- bt-replace-hoare key value tree stack = {!!} | |
| 593 | 481 |
| 588 | 482 |
| 483 | |
| 484 -- 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 | |
| 485 | |
| 486 -- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt'-leaf x) st cg = cg leaf st nothing | |
| 487 -- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt'-node d tree₁ tree₂ x x₁) st cg with <-cmp key d | |
| 488 -- 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)) | |
| 489 | |
| 490 -- 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 = | |
| 491 -- pushSingleLinkedStack st node | |
| 492 -- (λ st2 → find'-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg) | |
| 493 | |
| 494 -- 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 | |
| 495 -- (λ st2 → find'-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg) | |
| 496 | |
| 497 | |
| 498 | |
| 597 | 499 -- lleaf : {n : Level} {a : Set n} → bt {n} {a} |
| 600 | 500 -- lleaf = (L ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n) |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
501 |
| 597 | 502 -- lleaf1 : {n : Level} {A : Set n} → (0 < 3) → (a : A) → (d : ℕ ) → bt' {n} A d |
| 503 -- lleaf1 0<3 a d = bt'-leaf d | |
| 588 | 504 |
| 597 | 505 -- test-node1 : bt' ℕ 3 |
| 506 -- test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!}))) | |
| 588 | 507 |
| 508 | |
| 597 | 509 -- rleaf : {n : Level} {a : Set n} → bt {n} {a} |
| 600 | 510 -- rleaf = (L ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n)))) |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
511 |
| 597 | 512 -- test-node : {n : Level} {a : Set n} → bt {n} {a} |
| 600 | 513 -- test-node {n} {a} = (N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl ) |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
514 |
| 597 | 515 -- -- stt : {n m : Level} {a : Set n} {t : Set m} → {!!} |
| 516 -- -- stt {n} {m} {a} {t} = pushSingleLinkedStack [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) ) | |
| 587 | 517 |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
518 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
519 |
| 597 | 520 -- -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい |
| 521 -- -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる | |
| 522 -- 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 | |
| 600 | 523 -- bt-search {n} {m} {a} {t} key (L x) cg = cg nothing |
| 524 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d | |
| 525 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg | |
| 526 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) | |
| 527 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg | |
| 587 | 528 |
| 600 | 529 -- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg |
| 530 -- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) | |
| 531 -- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
532 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
533 |
| 597 | 534 -- -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう |
| 535 -- 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 | |
| 536 -- bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
537 |
| 597 | 538 -- 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 |
| 539 -- bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
540 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
541 |
| 597 | 542 -- -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ) |
| 543 -- -- up-some (just (fst , snd)) = just fst | |
| 544 -- -- up-some nothing = nothing | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
545 |
| 597 | 546 -- 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) |
| 600 | 547 -- search-lem {n} {m} {a} {t} key (L x) = refl |
| 548 -- search-lem {n} {m} {a} {t} key (N d tree₁ tree₂ x x₁) with <-cmp key d | |
| 549 -- search-lem {n} {m} {a} {t} key (N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄ key tree₁ | |
| 550 -- search-lem {n} {m} {a} {t} key (N d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl | |
| 551 -- search-lem {n} {m} {a} {t} key (N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄ key tree₂ | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
552 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
553 |
| 597 | 554 -- -- bt-find |
| 555 -- 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 | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
556 |
| 600 | 557 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(L x) st cg = cg leaf st nothing |
| 558 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N d tree₁ tree₂ x x₁) st cg with <-cmp key d | |
| 559 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(N d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c)) | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
560 |
| 600 | 561 -- find-support {n} {m} {a} {t} key node@(N ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c = |
| 597 | 562 -- pushSingleLinkedStack st node |
| 563 -- (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg) | |
| 587 | 564 |
| 600 | 565 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node |
| 597 | 566 -- (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg) |
| 587 | 567 |
| 597 | 568 -- 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 |
| 569 -- bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st | |
| 570 -- (λ cst → find-support ⦃ l ⦄ ⦃ u ⦄ key tr cst cg) | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
571 |
| 597 | 572 -- find-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → List bt -- ? |
| 573 -- find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st) | |
| 574 -- {-- result | |
| 575 -- λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ → | |
| 600 | 576 -- N 3 (L z≤n) (L (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ [] |
| 597 | 577 -- --} |
| 587 | 578 |
| 597 | 579 -- 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) |
| 600 | 580 -- find-lem d (L x) st = refl |
| 581 -- find-lem d (N d₁ tree tree₁ x x₁) st with <-cmp d d₁ | |
| 582 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
583 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
584 |
| 600 | 585 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with tri< a ¬b ¬c |
| 586 -- find-lem {n} {m} {a} {t} {{l}} {{u}} d (N d₁ tree tree₁ x x₁) st | tri< lt ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!} | |
| 587 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!} | |
| 588 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!} | |
| 587 | 589 |
| 600 | 590 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!} |
| 587 | 591 |
| 597 | 592 -- bt-singleton :{n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t |
| 600 | 593 -- bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (L ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl) |
| 587 | 594 |
| 595 | |
| 597 | 596 -- singleton-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? |
| 597 -- singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
598 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
599 |
| 597 | 600 -- 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 |
| 601 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree | |
| 600 | 602 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(N d L R x₁ x₂) (L x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case |
| 603 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁ | |
| 604 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ subt x₃ x₄ x₅) st cg | |
| 605 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ subt x₃ x₄ x₅) st cg | |
| 606 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ x₃ subt x₄ x₅) st cg | |
| 597 | 607 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case |
| 587 | 608 |
| 609 | |
| 610 | |
| 597 | 611 -- bt-replace : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ |
| 612 -- → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) | |
| 613 -- → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t | |
| 600 | 614 -- bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (L ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
615 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
616 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
617 |
| 597 | 618 -- -- 証明に insert がはいっててほしい |
| 619 -- bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) | |
| 620 -- → ((bt {n} {a}) → t) → t | |
| 587 | 621 |
| 597 | 622 -- 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 ) |
| 587 | 623 |
| 597 | 624 -- pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ |
| 600 | 625 -- pickKey (L x) = nothing |
| 626 -- pickKey (N d tree tree₁ x x₁) = just d | |
| 587 | 627 |
| 597 | 628 -- insert-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? |
| 629 -- insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x | |
| 587 | 630 |
| 597 | 631 -- insert-test-l : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? |
| 632 -- insert-test-l {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 (lleaf) λ x → x | |
| 587 | 633 |
| 634 | |
| 597 | 635 -- insert-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) |
| 636 -- → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 [] | |
| 637 -- (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt) ≡ just d ) ) | |
| 587 | 638 |
| 639 | |
| 600 | 640 -- insert-lem d (L x) with <-cmp d d -- bt-insert d (L x) (λ tree1 → {!!}) |
| 641 -- insert-lem d (L x) | tri< a ¬b ¬c = ⊥-elim (¬b refl) | |
| 642 -- insert-lem d (L x) | tri≈ ¬a b ¬c = refl | |
| 643 -- insert-lem d (L x) | tri> ¬a ¬b c = ⊥-elim (¬b refl) | |
| 644 -- insert-lem d (N d₁ tree tree₁ x x₁) with <-cmp d d₁ | |
| 645 -- -- bt-insert d (N d₁ tree tree₁ x x₁) (λ tree1 → {!!}) | |
| 646 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d | |
| 647 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) | |
| 648 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl | |
| 649 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) | |
| 587 | 650 |
| 600 | 651 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!} |
| 597 | 652 -- where |
| 600 | 653 -- lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (N d₁ tree tree₁ x x₁ ∷ []) (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄ (N ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (L ⦃ {!!} ⦄ ⦃ {!!} ⦄ (≤-reflexive refl)) z≤n (≤-reflexive refl)) st (λ tree1 → find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄ tt₂ ≡ just d))) |
| 597 | 654 -- lem-helper = {!!} |
| 587 | 655 |
| 600 | 656 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!} |
| 587 | 657 |