# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1636071698 -32400
# Node ID db42d1033857f08cdc429ab8cca07acf8f3f4a65
# Parent  8239583dac0b7837897c8abfb1c4d753a546d468
...

diff -r 8239583dac0b -r db42d1033857 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Thu Nov 04 23:52:05 2021 +0900
+++ b/hoareBinaryTree.agda	Fri Nov 05 09:21:38 2021 +0900
@@ -47,10 +47,14 @@
 
 {-# TERMINATING #-}
 find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A)  → (exit : bt A → List (bt A) → t) → t
-find-loop {_} {_} {A} {t} key tree st exit = find-loop1 tree st where
+find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where
     find-loop1 : bt A → List (bt A) → t
     find-loop1 tree st = find key tree st find-loop1  exit
 
+replaceNode : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → (bt A → t) → t
+replaceNode k v leaf next = next (node k v leaf leaf)
+replaceNode k v (node key value t t₁) next = next (node k v 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 ∷ st) next exit = next key value tree st 
@@ -66,9 +70,10 @@
     replace-loop1 key value tree st = replace key value tree st replace-loop1  exit
 
 insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t
-insertTree tree key value exit = find-loop key tree [] ( λ t st → replace-loop key value t st exit ) 
+insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st exit 
 
 insertTest1 = insertTree leaf 1 1 (λ x → x )
+insertTest2 = insertTree insertTest1 2 1 (λ x → x )
 
 open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
 
@@ -89,6 +94,14 @@
 stackInvariant {_} {A} tree (x ∷ tail @ (node key value left right ∷ _  )) = ( (left ≡ x) ∧ stackInvariant tree tail) ∨ ( (right ≡ x) ∧ stackInvariant tree tail)
 stackInvariant {_} {A} tree s = Lift _ ⊥
 
+rstackInvariant : {n : Level} {A : Set n} → (tree : bt A) → (stack  : List (bt A)) → Set n
+rstackInvariant {_} {A} _ [] = Lift _ ⊤
+rstackInvariant {_} {A} tree (tree1 ∷ [] ) = tree1 ≡ tree
+rstackInvariant {_} {A} tree (node key value leaf right ∷ x ∷ y )  = (right ≡ x) ∧ rstackInvariant tree (x ∷ y)
+rstackInvariant {_} {A} tree (node key value left leaf ∷ x ∷ y )  = (left ≡ x) ∧ rstackInvariant tree (x ∷ y)
+rstackInvariant {_} {A} tree (node key value left right ∷ x  ∷ y  ) = ( (left ≡ x) ∧ rstackInvariant tree (x ∷ y)) ∨ ( (right ≡ x) ∧ rstackInvariant tree (x ∷ y))
+rstackInvariant {_} {A} tree s = Lift _ ⊥
+
 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
            →  treeInvariant tree ∧ stackInvariant tree stack  
            → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack → bt-depth tree1 < bt-depth tree   → t )
@@ -99,17 +112,21 @@
 findP key n@(node key₁ v tree tree₁) st Pre next _ | tri< a ¬b ¬c = next tree (n ∷ st) {!!} {!!}
 findP key n@(node key₁ v tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} {!!}
 
+replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree )
+    → ((tree : bt A) → treeInvariant tree → (rstack : List (bt A))  → rstackInvariant tree rstack → t) → t
+replaceNodeP k v leaf P next = next (node k v leaf leaf) {!!} {!!} {!!}
+replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!} {!!}
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → (tree : bt A) → (stack rstack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack 
-     → (next : ℕ → A → (tree1 : bt A) → (stack rstack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree stack ∧ stackInvariant tree1 rstack → bt-depth tree1 < bt-depth tree   → t )
-     → (exit : (tree1 : bt A) → (stack : List (bt A))  → treeInvariant tree1 ∧ stackInvariant tree1 stack → t) → t
-replaceP key value tree [] rs Pre next exit = exit tree {!!} {!!} 
-replaceP key value tree (leaf ∷ st) rs Pre next exit = next key value tree st {!!} {!!} {!!}
-replaceP key value tree (node key₁ value₁ left right ∷ st) rs Pre next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree 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 {!!} {!!} {!!}
+     → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack ∧ rstackInvariant tree rstack
+     → (next : ℕ → A → (tree1 repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ rstackInvariant repl rstack → bt-depth tree1 < bt-depth tree   → t )
+     → (exit : (tree1 repl : bt A) → (rstack : List (bt A))  → treeInvariant tree1 ∧ rstackInvariant repl rstack → t) → t
+replaceP key value tree repl [] rs Pre next exit = exit tree repl {!!} {!!}  
+replaceP key value tree repl (leaf ∷ st) rs Pre next exit = next key value tree repl st {!!} {!!} {!!}
+replaceP key value tree repl (node key₁ value₁ left right ∷ st) rs Pre next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) repl st {!!} {!!} {!!} 
+... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) repl st {!!} {!!} {!!}
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) repl st {!!} {!!} {!!}
 
 open import Relation.Binary.Definitions
 
@@ -135,13 +152,16 @@
 
 open _∧_
 
-insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → (exit : (tree : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack  → t ) → t
+insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
+     → (exit : (tree repl : bt A) → (rstack : List (bt A)) → treeInvariant tree ∧ rstackInvariant repl rstack  → t ) → t
 insertTreeP {n} {m} {A} {t} tree key value P exit =
-   TerminatingLoopS (bt A ∧ List (bt A) ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p)) ∧ {!!} } (λ p → bt-depth (proj1 p)) ⟪ tree , ⟪ [] , {!!} ⟫ ⟫  ⟪ P , ⟪ lift tt , {!!} ⟫ ⟫
-       (λ p P loop → findP key (proj1 p)  (proj1 (proj2 p)) {!!} (λ t s P1 lt → loop ⟪ t , ⟪ s , {!!} ⟫ ⟫ {!!} lt )
-       (λ t s P → TerminatingLoopS (bt A ∧ List (bt A) ∧ bt A) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p))} (λ p → bt-depth (proj1 p)) ⟪ t , ⟪ s , {!!} ⟫ ⟫　P
-         (λ p P1 loop → replaceP key value (proj1 p) (proj1 (proj2 p)) {!!} P1 (λ k v t s s1 P2 lt → loop ⟪ t , ⟪  s , {!!} ⟫ ⟫ {!!} {!!} ) exit) 
-       ) )
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  ⟪ P , lift tt  ⟫
+       $ λ p P loop → findP key (proj1 p)  (proj2 p) P (λ t s P1 lt → loop ⟪ t ,  s  ⟫ P1 lt )
+       $ λ t s P → replaceNodeP key value t (proj1 P)
+       $ λ t1 P1 r R → TerminatingLoopS (bt A ∧ List (bt A) ∧ List (bt A))
+            {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p))  ∧ rstackInvariant t1 (proj2 (proj2 p))}
+               (λ p → bt-depth (proj1 p)) ⟪ t , ⟪ s , r ⟫ ⟫　⟪ proj1 P , ⟪ proj2 P , R ⟫ ⟫
+       $  λ p P1 loop → replaceP key value (proj1 p) {!!} (proj1 (proj2 p)) (proj2 (proj2 p)) {!!} (λ k v t repl s s1 P2 lt → loop ⟪ t , ⟪  {!!} , s1 ⟫ ⟫ {!!} {!!} ) exit 
 
 top-value : {n : Level} {A : Set n} → (tree : bt A) →  Maybe A 
 top-value leaf = nothing
@@ -152,5 +172,5 @@
 
 insertTreeSpec1 : {n : Level} {A : Set n}  → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
 insertTreeSpec1 {n} {A}  tree key value P =
-         insertTreeP tree key value P (λ  (tree₁ : bt A) (stack : List (bt A)) 
-            (P1 : treeInvariant tree₁ ∧ stackInvariant tree₁ stack ) → insertTreeSpec0 tree₁ value {!!} )
+         insertTreeP tree key value P (λ  (tree₁ repl : bt A) (rstack : List (bt A)) 
+            (P1 : treeInvariant tree₁ ∧ rstackInvariant repl rstack ) → insertTreeSpec0 tree₁ value {!!} )