# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1591512279 -32400
# Node ID 0dbbcab02864e994ecc774a88c2f672a39f72807
# Parent  803c423c2855db7547df0b20603653ae53470fdb
...

diff -r 803c423c2855 -r 0dbbcab02864 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Wed Mar 04 19:00:29 2020 +0900
+++ b/hoareBinaryTree1.agda	Sun Jun 07 15:44:39 2020 +0900
@@ -19,13 +19,13 @@
 
 
 data bt {n : Level} (A : Set n) : Set n where
-  bt-leaf :  bt A
+  bt-empty :  bt A
   bt-node : (key : ℕ) → A →
     (ltree : bt A) → (rtree : bt A) → bt A
 
 bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
     → ( bt A → List (bt A) → t ) → t
-bt-find {n} {m} {A} {t}  key leaf@(bt-leaf) stack exit = exit leaf stack
+bt-find {n} {m} {A} {t}  key leaf@(bt-empty) stack exit = exit leaf stack
 bt-find {n} {m} {A} {t}  key (bt-node key₁ AA tree tree₁) stack next with <-cmp key key₁
 bt-find {n} {m} {A} {t}  key node@(bt-node key₁ AA tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack
 bt-find {n} {m} {A} {t}  key node@(bt-node key₁ AA ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (node ∷ stack) next
@@ -35,17 +35,15 @@
 bt-replace {n} {m} {A} {t} ikey a otree stack next = bt-replace0 otree where
     bt-replace1 : bt A → List (bt A) → t
     bt-replace1 tree [] = next tree
-    bt-replace1 node ((bt-leaf) ∷ stack) = bt-replace1 node stack
+    bt-replace1 node ((bt-empty) ∷ stack) = bt-replace1 node stack
     bt-replace1 node ((bt-node key₁ b x x₁) ∷ stack) = bt-replace1 (bt-node key₁ b node x₁) stack
     bt-replace0 : (tree : bt A) → t
     bt-replace0 tree@(bt-node key _ ltr rtr) = bt-replace1 (bt-node ikey a ltr rtr) stack  -- find case
-    bt-replace0 bt-leaf = bt-replace1 (bt-node ikey a bt-leaf bt-leaf) stack
-
+    bt-replace0 bt-empty = bt-replace1 (bt-node ikey a bt-empty bt-empty) stack
 
 
-
-bt-empty : {n : Level} {A : Set n} → bt A
-bt-empty = bt-leaf
+bt-Empty : {n : Level} {A : Set n} → bt A
+bt-Empty = bt-empty
 
 bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → (bt A → t ) → t
 bt-insert key a tree next = bt-find key tree [] (λ mtree stack → bt-replace key a mtree  stack (λ tree → next tree) )
@@ -60,13 +58,42 @@
 insert-test1 :  bt ℕ
 insert-test1 = bt-insert 5 7 bt-empty (λ x → bt-insert 15 17 x (λ y → y))
 
+insert-test2 :  {n : Level} {t : Set n} →  ( bt ℕ → t ) → t
+insert-test2 next = bt-insert 15 17 bt-empty
+   $ λ x1 → bt-insert 5 7 x1
+   $ λ x2 → bt-insert 1 3 x2
+   $ λ x3 → bt-insert 4 2 x3
+   $ λ x4 → bt-insert 1 4 x4
+   $ λ y → next y
+
+insert-test3 :  bt ℕ
+insert-test3 = bt-insert 15 17 bt-empty
+   $ λ x1 → bt-insert 5 7 x1
+   $ λ x2 → bt-insert 1 3 x2
+   $ λ x3 → bt-insert 4 2 x3
+   $ λ x4 → bt-insert 1 4 x4
+   $ λ y → y
+
+insert-find0 : bt ℕ
+insert-find0  = insert-test2 $ λ tree → bt-find 1 tree [] $ λ x y → x 
+
+insert-find1 : List (bt ℕ)
+insert-find1  = insert-test2 $ λ tree → bt-find 1 tree [] $ λ x y → y 
+
+--
+--   1  After insert, all node except inserted node is preserved
+--   2  After insert, specified key node is inserted
+--   3  tree node order is consistent
+--
+--      4  noes on stack + current node = original top node                        .... invriant bt-find
+--      5  noes on stack + current node = original top node with replaced node     .... invriant bt-replace 
 
 tree+stack0 : {n : Level} {A : Set n} → (tree mtree : bt A) →  (stack : List (bt A))  → Set n
 tree+stack0 {n} {A} tree mtree [] = {!!}
 tree+stack0 {n} {A} tree mtree (x ∷ stack) = {!!}
 
 tree+stack : {n : Level} {A : Set n} → (tree mtree : bt A) →  (stack : List (bt A))  → Set n
-tree+stack {n} {A} bt-leaf mtree stack = (mtree ≡ bt-leaf) ∧ (stack ≡ [])
+tree+stack {n} {A} bt-empty mtree stack = (mtree ≡ bt-empty) ∧ (stack ≡ [])
 tree+stack {n} {A} (bt-node key x tree tree₁) mtree stack = bt-replace key x mtree stack (λ ntree → ntree ≡ tree) 
 
 data _implies_  (A B : Set ) : Set (succ Z) where
@@ -79,7 +106,7 @@
 bt-find-hoare1  : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (stack : List (bt A))
   → (tree+stack tree mtree stack)
   → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t
-bt-find-hoare1 {n} {m} {A} {t}  key leaf@(bt-leaf) mtree stack t+s exit = exit leaf stack {!!}
+bt-find-hoare1 {n} {m} {A} {t}  key leaf@(bt-empty) mtree stack t+s exit = exit leaf stack {!!}
 bt-find-hoare1 {n} {m} {A} {t}  key (bt-node key₁ AA tree tree₁) mtree stack t+s next with <-cmp key key₁
 bt-find-hoare1 {n} {m} {A} {t}  key node@(bt-node key₁ AA tree tree₁) mtree stack t+s exit | tri≈ ¬a b ¬c = exit node stack {!!}
 bt-find-hoare1 {n} {m} {A} {t}  key node@(bt-node key₁ AA ltree rtree) mtree stack t+s next | tri< a ¬b ¬c = bt-find-hoare1 {n} {m} {A} {t} key ltree {!!} (node ∷ stack) {!!} {!!}