Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 651:7b9d35f7c033

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix stack top and replaced tree
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 20 Nov 2021 14:24:22 +0900
parents 11388cab162f
children 8c7446829b99
comparison
equal deleted inserted replaced
650:11388cab162f 651:7b9d35f7c033
250 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t 250 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t
251 replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf 251 replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf
252 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) r-node 252 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) r-node
253 253
254 replaceP : {n m : Level} {A : Set n} {t : Set m} 254 replaceP : {n m : Level} {A : Set n} {t : Set m}
255 → (key : ℕ) → (value : A) → {tree0 tree : bt A} ( repl : bt A) 255 → (key : ℕ) → (value : A) → {tree0 tree tree-st : bt A} ( repl : bt A)
256 → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree tree0 stack ∧ replacedTree key value tree repl 256 → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack ∧ replacedTree key value tree repl
257 → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) 257 → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A))
258 → treeInvariant tree0 ∧ stackInvariant key tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) 258 → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
259 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 259 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
260 replaceP key value {tree0} {tree} repl [] Pre next exit with proj1 (proj2 Pre) 260 replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit with proj1 (proj2 Pre)
261 ... | () 261 ... | ()
262 replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ []) Pre next exit = 262 replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit =
263 exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (repl4 (proj1 (proj2 Pre))) (proj2 (proj2 Pre)) ⟫ where 263 exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (repl4 (proj1 (proj2 Pre))) {!!} ⟫ where
264 repl4 : stackInvariant key tree tree0 (leaf ∷ []) → tree ≡ tree0 264 repl41 : tree-st ≡ tree
265 repl41 = {!!}
266 repl4 : stackInvariant key tree-st tree0 (leaf ∷ []) → tree-st ≡ tree0
265 repl4 (s-single .leaf) = refl 267 repl4 (s-single .leaf) = refl
266 replaceP key value {tree0} {tree} repl (leaf ∷ leaf ∷ st) Pre next exit = ⊥-elim ( repl3 (proj1 (proj2 Pre))) where -- can't happen 268 replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ leaf ∷ st) Pre next exit = ⊥-elim ( repl3 (proj1 (proj2 Pre))) where -- can't happen
267 repl3 : stackInvariant key tree tree0 (leaf ∷ leaf ∷ st) → ⊥ 269 repl3 : stackInvariant key tree-st tree0 (leaf ∷ leaf ∷ st) → ⊥
268 repl3 (s-right x ()) 270 repl3 (s-right x ())
269 repl3 (s-left x ()) 271 repl3 (s-left x ())
270 replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ 272 replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
271 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) (node key₁ value₁ tree right ∷ st) 273 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) (node key₁ value₁ tree right ∷ st)
272 ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where 274 ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where
273 repl5 : stackInvariant key tree tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st ) 275 repl5 : stackInvariant key tree-st tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st )
274 repl5 (s-right x si) with si-property1 _ _ _ _ si 276 repl5 (s-right x si) with si-property1 _ _ _ _ si
275 ... | refl = ⊥-elim (nat-<> a x) 277 ... | refl = ⊥-elim (nat-<> a x)
276 repl5 (s-left x si) with si-property1 _ _ _ _ si 278 repl5 (s-left x si) with si-property1 _ _ _ _ si -- stackInvariant key (node key₁ value₁ leaf right) tree0 (node key₁ value₁ leaf right ∷ st)
277 ... | refl = si 279 -- stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st)
280 ... | refl = {!!} -- tree ≡ leaf
278 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3< 281 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3<
279 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3< 282 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3<
280 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ 283 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
281 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl 284 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl
282 ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen 285 ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen
283 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where 286 ... | tri< a ¬b ¬c with proj1 (proj2 Pre)
284 repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 st 287 ... | s-single .(node key₁ value₁ left right) = {!!}
285 repl2 (s-single .(node key₁ value₁ left right)) = {!!} 288 ... | s-right x si1 = {!!}
286 repl2 (s-right x si) with si-property1 _ _ _ _ si 289 ... | s-left x si1 = next key value (node key₁ value₁ repl right ) st ⟪ proj1 Pre , ⟪ si1 , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl
287 ... | eq = {!!}
288 repl2 (s-left x si) with si-property1 _ _ _ _ si
289 ... | eq = ?
290
291 290
292 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) 291 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
293 → (r : Index) → (p : Invraiant r) 292 → (r : Index) → (p : Invraiant r)
294 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t 293 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
295 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) 294 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)