Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 672:3676e845d46f

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 Tue, 23 Nov 2021 11:32:35 +0900
parents b5fde9727830
children a8e2bb44b843
comparison
equal deleted inserted replaced
671:b5fde9727830 672:3676e845d46f
263 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where 263 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
264 field 264 field
265 tree0 : bt A 265 tree0 : bt A
266 ti : treeInvariant tree0 266 ti : treeInvariant tree0
267 si : stackInvariant key tree tree0 stack 267 si : stackInvariant key tree tree0 stack
268 ri : replacedTree key value (replFromStack si) repl 268 ri : replacedTree key value tree repl
269 ci : C tree repl stack -- data continuation 269 ci : C tree repl stack -- data continuation
270 270
271 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) 271 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
272 → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) 272 → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
273 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t 273 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t
278 → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A) 278 → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A)
279 → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤) 279 → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤)
280 → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) 280 → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
281 → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t) 281 → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
282 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 282 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
283 replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 {!!} refl ) -- can't happen 283 replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
284 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ {!!} -- tree0 ≡ leaf 284 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre) -- tree0 ≡ leaf
285 ... | eq = exit {!!} (node key value leaf leaf) ⟪ {!!} , r-leaf ⟫ 285 ... | refl = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre , r-leaf ⟫
286 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ 286 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl02 ⟫ where
287 ... | tri< a ¬b ¬c = exit {!!} (node key₁ value₁ repl right ) {!!} where 287 repl01 : tree ≡ replacePR.tree0 Pre
288 repl01 : node key₁ value₁ tree right ≡ {!!} 288 repl01 with replacePR.si Pre
289 repl01 with si-property-last _ _ _ _ {!!} 289 ... | s-single x = refl
290 ... | eq = {!!} 290 repl05 : just (node key₁ value₁ left right) ≡ just (replacePR.tree0 Pre)
291 ... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value left right ) ⟪ {!!} , {!!} ⟫ -- can't happen 291 repl05 = si-property-last _ _ _ _ (replacePR.si Pre)
292 ... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl ) ⟪ {!!} , {!!} ⟫ 292 repl02 : replacedTree key value (replacePR.tree0 Pre) repl
293 repl02 = subst (λ k → replacedTree key value k repl ) repl01 (replacePR.ri Pre)
293 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen 294 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
294 replaceP key value {tree} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit with <-cmp key key₁ 295 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁
295 ... | tri< a ¬b ¬c = next key value {{!!}} (node key₁ value₁ tree right ) st {!!} ≤-refl 296 ... | tri< a ¬b ¬c = next key value {tree1} (node key₁ value₁ repl right ) st Post ≤-refl where
297 Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤)
298 Post with replacePR.si Pre
299 ... | s-right lt si1 with si-property1 si1 -- lt : suc key₂ ≤ key -- not allowed
300 ... | refl = record { tree0 = replacePR.tree0 Pre; ti = replacePR.ti Pre ; si = si1; ri = repl04 } where
301 repl03 : replacedTree key value tree1 {!!}
302 repl03 = r-right lt ( replacePR.ri Pre)
303 repl04 : replacedTree key value tree1 (node key₁ value₁ repl right)
304 repl04 = subst (λ k → replacedTree key value tree1 k ) {!!} (r-right lt ( replacePR.ri Pre))
305 Post | s-left lt si1 with si-property1 si1
306 ... | refl = record { tree0 = replacePR.tree0 Pre; ti = replacePR.ti Pre ; si = si1; ri = repl06 } where
307 repl05 : replacedTree key value tree1 {!!}
308 repl05 = r-left lt ( replacePR.ri Pre)
309 repl06 : replacedTree key value tree1 (node key₁ value₁ repl right)
310 repl06 = subst (λ k → replacedTree key value tree1 k ) {!!} (r-left lt ( replacePR.ri Pre))
296 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl 311 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl
297 ... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl 312 ... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
298 313
299 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) 314 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
300 → (r : Index) → (p : Invraiant r) 315 → (r : Index) → (p : Invraiant r)