# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1636037525 -32400
# Node ID 8239583dac0b7837897c8abfb1c4d753a546d468
# Parent  79418701a2838e549df3c44a287c326219108ffb
add one more stack

diff -r 79418701a283 -r 8239583dac0b hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Thu Nov 04 16:35:11 2021 +0900
+++ b/hoareBinaryTree.agda	Thu Nov 04 23:52:05 2021 +0900
@@ -31,7 +31,7 @@
 data bt {n : Level} (A : Set n) : Set n where
   leaf : bt A
   node :  (key : ℕ) → (value : A) →
-    (left : bt A ) → (write : bt A ) → bt A
+    (left : bt A ) → (right : bt A ) → bt A
 
 bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
 bt-depth leaf = 0
@@ -81,22 +81,18 @@
 
 treeInvariantTest1  = treeInvariant (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf)))
 
-stackInvariant : {n : Level} {A : Set n} → (stack  : List (bt A)) → Set n
-stackInvariant {_} {A} [] = Lift _ ⊤
-stackInvariant {_} {A} (leaf ∷ stack) = Lift _ ⊤
-stackInvariant {_} {A} (node key value leaf leaf ∷ []) = Lift _ ⊤
-stackInvariant {_} {A} (node key value _ (node _ _ _ _) ∷ []) = Lift _ ⊥
-stackInvariant {_} {A} (node key value (node _ _ _ _) _ ∷ []) = Lift _ ⊥
-stackInvariant {_} {A} (x ∷ node key value leaf leaf ∷ tail ) = Lift _ ⊥
-stackInvariant {_} {A} (x ∷ tail @ (node key value leaf tree ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail
-stackInvariant {_} {A} (x ∷ tail @ (node key value tree leaf ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail
-stackInvariant {_} {A} (x ∷ tail @ (node key value left right ∷ _  )) = ( (left ≡ x) ∧ stackInvariant tail) ∨ ( (right ≡ x) ∧ stackInvariant tail)
-stackInvariant {_} {A} s = Lift _ ⊥
+stackInvariant : {n : Level} {A : Set n} → (tree : bt A) → (stack  : List (bt A)) → Set n
+stackInvariant {_} {A} _ [] = Lift _ ⊤
+stackInvariant {_} {A} tree (tree1 ∷ [] ) = tree1 ≡ tree
+stackInvariant {_} {A} tree (x ∷ tail @ (node key value leaf right ∷ _) ) = (right ≡ x) ∧ stackInvariant tree tail
+stackInvariant {_} {A} tree (x ∷ tail @ (node key value left leaf ∷ _) ) = (left ≡ x) ∧ stackInvariant tree tail
+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 _ ⊥
 
 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
-           →  treeInvariant tree ∧ stackInvariant stack  
-           → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → t ) → t
+           →  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 )
+           → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack → t ) → t
 findP key leaf st Pre _ exit = exit leaf st {!!}
 findP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
 findP key n st Pre _ exit | tri≈ ¬a b ¬c = exit n st {!!}
@@ -105,15 +101,15 @@
 
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → (tree : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant stack 
-     → (next : ℕ → A → (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-depth tree1 < bt-depth tree   → t )
-     → (exit : (tree1 : bt A) → treeInvariant tree1 → t) → t
-replaceP key value tree [] Pre next exit = exit tree {!!}
-replaceP key value tree (leaf ∷ st) Pre next exit = next key value tree st {!!} {!!}
-replaceP key value tree (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 {!!} {!!}
-... | 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 : 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 {!!} {!!} {!!}
 
 open import Relation.Binary.Definitions
 
@@ -139,12 +135,12 @@
 
 open _∧_
 
-insertTreeP : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → (exit : (tree : bt A) → treeInvariant tree  → t ) → t
-insertTreeP {n} {A} {t} tree key value P exit =
-   TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (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 → TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ t , s ⟫　P
-         (λ p P1 loop → replaceP key value (proj1 p) (proj2 p) P1 (λ k v t s P2 lt → loop ⟪ t , s ⟫ P2 lt) exit) 
+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} {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) 
        ) )
 
 top-value : {n : Level} {A : Set n} → (tree : bt A) →  Maybe A 
@@ -156,11 +152,5 @@
 
 insertTreeSpec1 : {n : Level} {A : Set n}  → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
 insertTreeSpec1 {n} {A}  tree key value P =
-         TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (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 → TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ t , s ⟫　P
-       $ λ p P1 loop → replaceP key value (proj1 p) (proj2 p) P1 (λ k v t s P2 lt → loop ⟪ t , s ⟫ P2 lt)
-       $ λ t1 P2 → TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ t1 , [] ⟫  ⟪ P2 , lift tt ⟫
-       $ λ p P3 loop → findP key (proj1 p)  (proj2 p) P3 (λ t s P3 lt → loop ⟪ t , s ⟫ P3 lt )
-       $ λ t2 s1 P4 → insertTreeSpec0 t2 value {!!}
-
+         insertTreeP tree key value P (λ  (tree₁ : bt A) (stack : List (bt A)) 
+            (P1 : treeInvariant tree₁ ∧ stackInvariant tree₁ stack ) → insertTreeSpec0 tree₁ value {!!} )