# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1652230571 -32400
# Node ID 52938e8a54a228094c68282da626347c3bff5402
# Parent  a36147bb596de08171b1959c2fa1a95911c34f48
one step further on find

diff -r a36147bb596d -r 52938e8a54a2 ModelChecking.agda
--- a/ModelChecking.agda	Tue May 10 18:44:46 2022 +0900
+++ b/ModelChecking.agda	Wed May 11 09:56:11 2022 +0900
@@ -240,6 +240,16 @@
     next1 :  bt Data → Context  → ℕ → bt Data
     next1 t c1 n = t
 
+test01-tree : bt Data
+test01-tree = node 1 (D_AtomicNat record { ptr = 1 ; value = 0 } ) leaf leaf
+
+test01-assert : test01-tree ≡ test01
+test01-assert = refl
+
+tail1 :  Maybe (List (bt Data)) →  Maybe (List (bt Data)) 
+tail1 (just x) = tail x
+tail1 nothing = nothing
+
 test2 : List Context 
 test2 = init-AtomicNat1 init-context $  λ c left → alloc-data c
  $ λ c n → insertTree (Context.memory c) n  (D_AtomicNat (a n))
@@ -247,11 +257,14 @@
     a : ℕ → AtomicNat
     a ptr = record { ptr = ptr ; value = 0 }
 
-test21 : ℕ ∧ Maybe (List (bt Data))
+test21 : ℕ ∧ (List (bt Data))
 test21 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
- $ λ c n → find n (Context.memory c) (Context.memory c ∷ [])  (λ d st → ⟪ n , just st ⟫ ) $ λ t st → ⟪ n , nothing ⟫  where
+ $ λ c n → find-loop n (Context.memory c) (Context.memory c ∷ [])   $ λ t st → ⟪ n , st  ⟫  where
     a : ℕ → AtomicNat
     a ptr = record { ptr = ptr ; value = 0 }
+    b : Maybe (List (bt Data)) → Maybe (bt Data)
+    b (just x) = head x
+    b nothing = nothing
 
 test22 : ℕ ∧ (Maybe (List (bt Data)))
 test22 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
@@ -259,6 +272,15 @@
     a : ℕ → AtomicNat
     a ptr = record { ptr = ptr ; value = 0 }
 
+test23 : ℕ ∧ (Maybe ((bt Data)))
+test23 = find n test01-tree (test01-tree ∷ []) (λ t st → find n t st (λ t st → ⟪ 1 , b (tail st) ⟫) (λ t st → ⟪ 2 , b ((just st)) ⟫))  $ λ t st → ⟪ 0 , b (tail st) ⟫  where
+    n = 2
+    a : ℕ → AtomicNat
+    a ptr = record { ptr = ptr ; value = 0 }
+    b : Maybe (List (bt Data)) → Maybe (bt Data)
+    b (just x) = head x
+    b nothing = nothing
+
 test : List Context 
 test = init-AtomicNat1 init-context $ λ c left → init-AtomicNat1 c $ λ c1 right → init-Phil-1 (c1 ∷ []) left right
 
diff -r a36147bb596d -r 52938e8a54a2 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Tue May 10 18:44:46 2022 +0900
+++ b/hoareBinaryTree.agda	Wed May 11 09:56:11 2022 +0900
@@ -56,6 +56,7 @@
 find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
            → (next : (tree1 : bt A) → (stack : List (bt A)) → t)
            → (exit : (tree1 : bt A) → (stack : List (bt A)) → t) → t
+find key _ (leaf ∷ st) _ exit = exit leaf []
 find key leaf st _ exit = exit leaf st 
 find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
 find key n st _ exit | tri≈ ¬a refl ¬c = exit n st