# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1636958070 -32400
# Node ID be6bd51c3f05ec8d85ddd971717ebfd3c19e24d8
# Parent  e30dcd03c07f285d5c6faa194a6e2b464991ea9a
replaceTree

diff -r e30dcd03c07f -r be6bd51c3f05 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Mon Nov 15 15:04:06 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 15 15:34:30 2021 +0900
@@ -161,20 +161,28 @@
 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
            →  treeInvariant tree ∧ stackInvariant tree tree0 stack  
            → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 tree0 stack → t ) → t
-findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre
+           → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 tree0 stack
+                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
+findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre (case1 refl)
 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
-findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st Pre
+findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl)
 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st) ⟪ treeLeftDown tree tree₁ (proj1 Pre)  , findP1 a (proj2 Pre) ⟫ depth-1< where
    findP1 : key < key₁ →  stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree tree0 (tree ∷ st)
    findP1 a si = s-left si
 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right (proj2 Pre) ⟫ depth-2<
 
 
-replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree )
-    → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value tree tree1 → t) → t
-replaceNodeP k v1 leaf P next = next (node k v1 leaf leaf) {!!} {!!} 
-replaceNodeP k v1 (node key value t t₁) P next = next (node k v1 t t₁) {!!} {!!}
+replaceTree1 : {n  : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) →  treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
+replaceTree1 k v1 value (t-single .k .v1) = t-single k value
+replaceTree1 k v1 value (t-right x t) = t-right x t
+replaceTree1 k v1 value (t-left x t) = t-left x t
+replaceTree1 k v1 value (t-node x x₁ t t₁) = t-node x x₁ t t₁
+
+replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
+    → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
+    → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value tree tree1 → t) → t
+replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf 
+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
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant repl tree stack ∧ replacedTree key value tree repl
@@ -224,7 +232,7 @@
 insertTreeP {n} {m} {A} {t} tree key value P exit =
    TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  ⟪ P , {!!}  ⟫
        $ λ p P loop → findP key (proj1 p)  tree (proj2 p) {!!} (λ t _ s P1 lt → loop ⟪ t ,  s  ⟫ {!!} lt )
-       $ λ t _ s P → replaceNodeP key value t (proj1 P)
+       $ λ t _ s P C → replaceNodeP key value t C (proj1 P)
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
             {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p)  ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
                (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ proj1 P , ⟪ {!!}  , R ⟫ ⟫
@@ -269,7 +277,7 @@
 insertTreePP {n} {m} {A} {t} tree key value  P exit =
    TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR key (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  {!!}
        $ λ p P loop → findPP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t ,  s  ⟫ P1 lt )
-       $ λ t s _ P → replaceNodeP key value t {!!}
+       $ λ t s _ P → replaceNodeP key value t {!!} {!!}
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
             {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p)  ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
                (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!}  , R ⟫ ⟫