Mercurial > hg > Gears > GearsAgda

changeset 618:5702800c79bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 18:35:31 +0900
parents bae54f556438
children a3fbc9b57015
files hoareBinaryTree.agda
diffstat 1 files changed, 36 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Sun Nov 07 13:08:19 2021 +0900
+++ b/hoareBinaryTree.agda	Sun Nov 07 18:35:31 2021 +0900
@@ -35,7 +35,7 @@
 
 bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
 bt-depth leaf = 0
-bt-depth (node key value t t₁) = Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ )
+bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ ))
 
 find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
            → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
@@ -179,23 +179,43 @@
 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
 insertTreeSpec0 _ _ _ = tt
 
+record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) (C : Set n) : Set n where
+   field
+     ti : treeInvariant tree
+     si : stackInvariant tree stack
+     opt : C
+     opt1 : C → C
+   
 findPP : {n m : Level} {A : Set n} {t : Set m}
            → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
            → {Cond : bt A → List (bt A) → Set n}
-           → (Pre :  Cond  tree stack )
-           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → Cond tree1 stack1 →  bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → Cond tree1 stack1 → t) → t
-findPP key leaf tree0 st Pre exit = exit leaf tree0 st 
+           → (Pre :   bt A → List (bt A) →  findPR tree stack (Cond tree stack) )
+           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (Cond tree1 stack1) →  bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (Cond tree1 stack1) → t) → t
+findPP key leaf st Pre next exit = exit leaf st (Pre leaf st ) 
 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
-findPP key n st c _ exit | tri≈ ¬a b ¬c = exit n st c -- c : Cond (node key₁ v tree tree₁) st 
-findPP key n@(node key₁ v tree tree₁) st Pre next _ | tri< a ¬b ¬c = next tree (n ∷ st) {!!} {!!}  -- Cond n st → Cond tree  (n ∷ st)
-findPP key n@(node key₁ v tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} {!!} -- Cond n st → Cond tree₁ (n ∷ st)
+findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st (P n st) 
+findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c = next tree (n ∷ st) (record {ti = {!!} ; si = {!!} ; opt = {!!} ; opt1 = id } ) findPP1 where -- Cond n st → Cond tree  (n ∷ st)
+    findPP0 : {!!}
+    findPP0 = {!!}
+    findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
+    findPP1 =  {!!}
+findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st)
+    findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
+    findPP2 = {!!}
 
-record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
-   field
-     ti : treeInvariant tree
-     si : stackInvariant tree stack
-   
+insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
+     → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t
+insertTreePP {n} {m} {A} {t} tree key value P exit =
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) {!!} } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  {!!}
+       $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t ,  s  ⟫ {!!} lt )
+       $ λ 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)) (proj1 p)  ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
+               (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!}  , R ⟫ ⟫
+       $  λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) P1
+            (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1  , repl1  ⟫ ⟫ P2 lt )  exit 
+
 -- findP key tree stack = findPP key tree stack {findPR} → record { ti = tree-invariant tree ; si stack-invariant tree stack } → 
 
 record findP-contains {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
@@ -204,14 +224,13 @@
      value1 : A
      tree1 : bt A
      ci : replacedTree key1 value1 tree tree1
-     R : findPR tree stack
    
-containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → replacedTree key value tree tree1   → ⊤
+containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree  → ⊤
 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
    TerminatingLoopS (bt A ∧ List (bt A) )
      {λ p → findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p))
-              ⟪ tree1 , []  ⟫ record { key1 = key ; value1 = value ; tree1 = tree1 ; ci = {!!} ; R = record { ti = {!!} ; si = {!!} } }
-       $ λ p P loop → findPP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 
+              ⟪ tree1 , []  ⟫ record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { ti = P ; si = lift tt } }
+       $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 
        $ λ t s P → insertTreeSpec0 t value {!!}
 
 insertTreeSpec1 : {n : Level} {A : Set n}  → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤