Mercurial > hg > Gears > GearsAgda

changeset 678:8dd9b11aa358

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, 29 Nov 2021 15:40:55 +0900
parents 681577b60c35
children ce79298f4c00
files hoareBinaryTree.agda
diffstat 1 files changed, 12 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 29 09:06:31 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 29 15:40:55 2021 +0900
@@ -285,22 +285,25 @@
 replaceP key value {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
 replaceP key value {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (replacePR.si Pre)-- tree0 ≡ leaf
 ... | refl  =  exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre ,  r-leaf ⟫
-replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where
-    repl01 : replacedTree key value (replacePR.tree0 Pre) repl
-    repl01 = subst (λ k → replacedTree key value k _) {!!} (  replacePR.ri Pre )
-... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value  left right )  ⟪ {!!} , {!!} ⟫ -- can't happen
-... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl )  ⟪ {!!} , {!!} ⟫
+replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where
+    repl06 : child-replaced key value  (node key₁ value₁ left right ∷ []) tree (replacePR.tree0 Pre) (replacePR.si Pre)  ≡ node key₁ value₁ left right
+    repl06 with replacePR.si Pre
+    ... | s-single = refl
+    repl01 : replacedTree key value (replacePR.tree0 Pre) repl  
+    repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)   
+    repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl06 (replacePR.ri Pre)
 replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
 replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ | si-property1 (replacePR.si Pre)
 ... | tri< a ¬b ¬c | refl = next key value {{!!}} (node key₁ value₁ repl right ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
     Post with replacePR.si Pre
     ... | s-right x t = {!!}
-    ... | s-left lt si with si-property1 si
-    ... | refl = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si  ; ri = {!!} ; ci = lift tt } where
+    ... | s-left lt si with si-property1 si | replacePR.ri Pre
+    ... | refl | ri = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si  ; ri = {!!} ; ci = lift tt } where
+        repl03 : replacedTree key value {!!} repl
+        repl03 = ri
         repl02 : replacedTree key value tree (node key₁ value₁ repl right)
-        repl02 = {!!}
+        repl02 = subst (λ k → replacedTree key value (node key₁ value₁ k right) _ ) {!!} ( r-left {!!} ri )
 ... | tri≈ ¬a b ¬c | refl = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl -- can't happen
 ... | tri> ¬a ¬b c | refl = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl