Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 622:a1849f24fa66

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Nov 2021 20:54:09 +0900
parents 6861bcb9c54d
children 753353a41da5
comparison
equal deleted inserted replaced
621:6861bcb9c54d 622:a1849f24fa66
192 insertTreeSpec0 _ _ _ = tt 192 insertTreeSpec0 _ _ _ = tt
193 193
194 record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where 194 record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
195 field 195 field
196 tree0 : bt A 196 tree0 : bt A
197 ti : treeInvariant tree 197 ti : treeInvariant tree0
198 si : stackInvariant tree tree0 stack 198 si : stackInvariant tree tree0 stack
199 199
200 findPP : {n m : Level} {A : Set n} {t : Set m} 200 findPP : {n m : Level} {A : Set n} {t : Set m}
201 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) 201 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
202 → (Pre : findPR tree stack ) 202 → (Pre : findPR tree stack )
204 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 → t) → t 204 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 → t) → t
205 findPP key leaf st Pre next exit = exit leaf st Pre 205 findPP key leaf st Pre next exit = exit leaf st Pre
206 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁ 206 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
207 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st P 207 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st P
208 findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c = 208 findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c =
209 next tree (n ∷ st) (record {ti = findPP0 tree tree₁ (findPR.ti Pre ) ; si = findPP2 st (findPR.si Pre)} ) findPP1 where 209 next tree (n ∷ st) (record {ti = findPR.ti Pre ; si = findPP2 st (findPR.si Pre)} ) findPP1 where
210 tree0 = findPR.tree0 Pre 210 tree0 = findPR.tree0 Pre
211 findPP0 : (tree tree₁ : bt A) → treeInvariant ( node key₁ v tree tree₁ ) → treeInvariant tree
212 findPP0 leaf t x = {!!}
213 findPP0 (node key value tree tree₁) leaf x = proj1 {!!}
214 findPP0 (node key value tree tree₁) (node key₁ value₁ t t₁) x = proj1 {!!}
215 findPP2 : (st : List (bt A)) → stackInvariant {!!} tree0 st → stackInvariant {!!} tree0 (node key₁ v tree tree₁ ∷ st) 211 findPP2 : (st : List (bt A)) → stackInvariant {!!} tree0 st → stackInvariant {!!} tree0 (node key₁ v tree tree₁ ∷ st)
216 findPP2 [] = {!!} 212 findPP2 = ?
217 findPP2 (leaf ∷ st) x = {!!}
218 findPP2 (node key value leaf leaf ∷ st) x = {!!}
219 findPP2 (node key value leaf (node key₁ value₁ x₂ x₃) ∷ st) x = {!!}
220 findPP2 (node key value (node key₁ value₁ x₁ x₃) leaf ∷ st) x = {!!}
221 findPP2 (node key value (node key₁ value₁ x₁ x₃) (node key₂ value₂ x₂ x₄) ∷ st) x = {!!}
222 findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) 213 findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
223 findPP1 = {!!} 214 findPP1 = {!!}
224 findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st) 215 findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st)
225 findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) 216 findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
226 findPP2 = {!!} 217 findPP2 = {!!}
249 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ 240 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
250 containsTree {n} {m} {A} {t} tree tree1 key value P RT = 241 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
251 TerminatingLoopS (bt A ∧ List (bt A) ) 242 TerminatingLoopS (bt A ∧ List (bt A) )
252 {λ p → findPR (proj1 p) (proj2 p) ∧ findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p)) 243 {λ p → findPR (proj1 p) (proj2 p) ∧ findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p))
253 ⟪ tree1 , [] ⟫ ⟪ {!!} , record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { tree0 = {!!} ; ti = P ; si = lift tt } } ⟫ 244 ⟪ tree1 , [] ⟫ ⟪ {!!} , record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { tree0 = {!!} ; ti = P ; si = lift tt } } ⟫
254 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt ) 245 $ λ p P loop → findPP key (proj1 p) (proj2 p) (proj1 P) (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt )
255 $ λ t s P → insertTreeSpec0 t value {!!} 246 $ λ t1 s1 P2 → insertTreeSpec0 t1 value {!!}
256 247
257 insertTreeSpec1 : {n : Level} {A : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
258 insertTreeSpec1 {n} {A} tree key value P =
259 insertTreeP tree key value P (λ (tree₁ repl : bt A)
260 (P1 : treeInvariant tree₁ ∧ replacedTree key value tree₁ repl ) → insertTreeSpec0 tree₁ value (lemma1 {!!} ) ) where
261 lemma1 : (tree₁ : bt A) → top-value tree₁ ≡ just value
262 lemma1 = {!!}