# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1637576600 -32400
# Node ID 077e2f3e417fc14294f0759f1e1161611b0d4b4d
# Parent  d009198364dc6c6a255bcd40c203a1da366c9648
...

diff -r d009198364dc -r 077e2f3e417f hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Mon Nov 22 16:04:06 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 22 19:23:20 2021 +0900
@@ -64,17 +64,17 @@
 replaceNode k v1 (node key value t t₁) next = next (node k v1 t t₁)
 
 replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t
-replace key value tree [] next exit = exit tree
-replace key value tree (leaf ∷ []) next exit = exit  (node key value leaf leaf)
-replace key value tree (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = exit (node key₁ value₁ tree right ) 
+replace key value repl [] next exit = exit repl    -- can't happen
+replace key value repl (leaf ∷ []) next exit = exit repl    -- can't happen
+replace key value repl (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) 
 ... | tri≈ ¬a b ¬c = exit (node key₁ value  left right ) 
-... | tri> ¬a ¬b c = exit (node key₁ value₁ left tree ) 
-replace key value tree (leaf ∷ st) next exit = next key value (node key value leaf leaf) st
-replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st
+... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) 
+replace key value repl (leaf ∷ st) next exit = next key value repl st    -- can't happen
+replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st
-... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st
 
 {-# TERMINATING #-}
 replace-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A)  → (exit : bt A → t) → t
@@ -87,6 +87,8 @@
 
 insertTest1 = insertTree leaf 1 1 (λ x → x )
 insertTest2 = insertTree insertTest1 2 1 (λ x → x )
+insertTest3 = insertTree insertTest2 3 2 (λ x → x )
+insertTest4 = insertTree insertTest3 2 2 (λ x → x )
 
 open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
 
@@ -266,28 +268,18 @@
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {tree0 tree : bt A} ( repl : bt A)
-     → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree tree0 (tree ∷ stack) ∧ replacedTree key value tree repl
+     → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree tree0 stack ∧ replacedTree key value tree repl
      → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
          → treeInvariant tree0 ∧ stackInvariant key tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
-replaceP key value {tree0} {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (proj1 (proj2 Pre)) {!!} ) -- can't happen
+replaceP key value {tree0} {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (proj1 (proj2 Pre)) refl ) -- can't happen
 replaceP key value {tree0} {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (proj1 (proj2 Pre)) -- tree0 ≡ leaf
 ... | refl =  exit tree0 (node key value leaf leaf) ⟪ proj1 Pre ,  r-leaf ⟫
 replaceP key value {tree0} {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ repl right )
-    ⟪ proj1 Pre , subst (λ k → replacedTree key value k (node key₁ value₁ repl right)) {!!} (r-left a (proj2 (proj2 Pre)) ) ⟫ where
-      repl03 : node key₁ value₁ left right ≡ tree0
-      repl03 with si-property-last  _ _ _ _ (proj1 (proj2 Pre))
-      ... | refl = refl
-... | tri≈ ¬a refl ¬c = exit tree0 (node key₁ value  left right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} r-node ⟫
-... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫
-replaceP {n} {_} {A} key value {tree0} {tree}  repl (leaf ∷ st@(_ ∷ _)) Pre next exit =
-     next key value {tree0} (node key value leaf leaf) st
-         ⟪ proj1 Pre ,  ⟪ repl01 (sym (si-property1 (proj1 (proj2 Pre)))) {!!}
-             , subst (λ k → replacedTree key value k  (node key value leaf leaf) ) {!!} r-leaf ⟫  ⟫  ≤-refl where
-      repl01 : {x : bt A} → { xs : List (bt A)} → {!!} → stackInvariant key tree tree0 (leaf ∷ x ∷ xs) → stackInvariant key x tree0 (x ∷ xs)
-      repl01 {x} {xs} refl (s-right lt si) = subst (λ k → stackInvariant key k tree0 (x ∷ xs) ) (sym (si-property1 si)) si
-      repl01 {x} {xs} refl (s-left lt si) = subst (λ k → stackInvariant key k tree0 (x ∷ xs) ) (sym (si-property1 si)) si
+... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) ⟪ proj1 Pre , {!!} ⟫
+... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value  left right )  ⟪ proj1 Pre , {!!} ⟫
+... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree )  ⟪ proj1 Pre , {!!} ⟫
+replaceP {n} {_} {A} key value {tree0} {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
 replaceP key value {tree0} {tree}  repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit  with <-cmp key key₁
 ... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫  ⟫ ≤-refl
 ... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value  left right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫ ⟫ ≤-refl