# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1637634755 -32400
# Node ID 3676e845d46f4236ff3b8e7d5174e2fce8158636
# Parent  b5fde972783094cb94fa3adb7604e35945595166
...

diff -r b5fde9727830 -r 3676e845d46f hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Mon Nov 22 22:59:08 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 23 11:32:35 2021 +0900
@@ -265,7 +265,7 @@
      tree0 : bt A
      ti : treeInvariant tree0
      si : stackInvariant key tree tree0 stack
-     ri : replacedTree key value (replFromStack si) repl
+     ri : replacedTree key value tree repl
      ci : C tree repl stack     -- data continuation
    
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
@@ -280,19 +280,34 @@
      → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
          → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
-replaceP key value {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 {!!} refl ) -- can't happen
-replaceP key value {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  {!!} -- tree0 ≡ leaf
-... | eq =  exit {!!} (node key value leaf leaf) ⟪ {!!} ,  r-leaf ⟫
-replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = exit {!!} (node key₁ value₁ repl right ) {!!} where
-    repl01 : node key₁ value₁ tree right ≡ {!!}
-    repl01 with si-property-last _ _ _ _ {!!}
-    ... | eq = {!!}
-... | 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 [] 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 = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre  , repl02 ⟫ where
+    repl01 : tree ≡ replacePR.tree0 Pre
+    repl01 with replacePR.si Pre
+    ... | s-single x = refl
+    repl05 : just (node key₁ value₁ left right) ≡ just (replacePR.tree0 Pre) 
+    repl05 =  si-property-last _ _ _ _ (replacePR.si Pre) 
+    repl02 : replacedTree key value (replacePR.tree0 Pre) repl
+    repl02 = subst (λ k → replacedTree key value k repl ) repl01 (replacePR.ri Pre)
 replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
-replaceP key value {tree}  repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value {{!!}} (node key₁ value₁ tree right ) st {!!} ≤-refl
+replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁
+... | tri< a ¬b ¬c = next key value {tree1} (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 lt si1 with  si-property1 si1   -- lt : suc key₂ ≤ key  -- not allowed
+    ... | refl = record { tree0 = replacePR.tree0 Pre; ti =  replacePR.ti  Pre ; si = si1; ri = repl04 } where
+       repl03 : replacedTree key value tree1 {!!}
+       repl03 =  r-right lt ( replacePR.ri  Pre)
+       repl04 :  replacedTree key value tree1 (node key₁ value₁ repl right)
+       repl04 = subst (λ k →  replacedTree key value tree1 k ) {!!} (r-right lt ( replacePR.ri  Pre))
+    Post | s-left lt si1 with  si-property1 si1
+    ... | refl = record { tree0 = replacePR.tree0 Pre; ti =  replacePR.ti  Pre ; si = si1; ri = repl06 } where
+       repl05 : replacedTree key value tree1 {!!}
+       repl05 =  r-left lt ( replacePR.ri  Pre)
+       repl06 :  replacedTree key value tree1 (node key₁ value₁ repl right)
+       repl06 = subst (λ k →  replacedTree key value tree1 k ) {!!} (r-left lt ( replacePR.ri  Pre))
 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl
 ... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl