Mercurial > hg > Gears > GearsAgda

changeset 615:83e595bba219

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 Fri, 05 Nov 2021 16:37:14 +0900
parents 0c174b6239a0
children 441f3cc79a0b
files hoareBinaryTree.agda
diffstat 1 files changed, 32 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Fri Nov 05 13:50:21 2021 +0900
+++ b/hoareBinaryTree.agda	Fri Nov 05 16:37:14 2021 +0900
@@ -95,22 +95,22 @@
 stackInvariant {_} {A} tree s = Lift _ ⊥
 
 data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (tree tree1 : bt A ) → Set n where
-    rleaf : replacedTree key value leaf (node key value leaf leaf)
-    rnode : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value t t₁) (node key value₁ t t₁) 
-    rleft : {k : ℕ } {v : A} → {t t1 t2 : bt A}
-          → ( replacedTree key value t1 t2 →  replacedTree key value (node k v t t1) (node k v t t2) )
-    rright : {k : ℕ } {v : A} → {t t1 t2 : bt A}
-          → ( replacedTree key value t1 t2 →  replacedTree key value (node k v t1 t) (node k v t2 t) )
+    r-leaf : replacedTree key value leaf (node key value leaf leaf)
+    r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 
+    r-right : {k : ℕ } {v : A} → {t t1 t2 : bt A}
+          → k > key → ( replacedTree key value t1 t2 →  replacedTree key value (node k v t t1) (node k v t t2) )
+    r-left : {k : ℕ } {v : A} → {t t1 t2 : bt A}
+          → k < key → ( replacedTree key value t1 t2 →  replacedTree key value (node k v t1 t) (node k v t2 t) )
 
-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 )
-           → (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 {!!}
-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) {!!} {!!}
+findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
+           →  treeInvariant tree ∧ stackInvariant tree0 stack  
+           → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree0 stack → bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree0 stack → t ) → t
+findP key leaf tree0 st Pre _ exit = exit leaf tree0 st {!!}
+findP key (node key₁ v tree tree₁) tree0 st Pre next exit with <-cmp key key₁
+findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st {!!}
+findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} {!!}
+findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} {!!}
 
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree )
     → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value tree tree1 → t) → t
@@ -152,16 +152,23 @@
 
 open _∧_
 
+RTtoTI0  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
+     → replacedTree key value tree repl → treeInvariant repl
+RTtoTI0  = {!!}
+
+RTtoTI1  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
+     → replacedTree key value tree repl → treeInvariant tree
+RTtoTI1  = {!!}
 
 insertTreeP : {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
 insertTreeP {n} {m} {A} {t} tree key value P 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)
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  ⟪ P , lift tt  ⟫
+       $ λ p P loop → findP key (proj1 p)  tree (proj2 p) {!!} (λ t _ s P1 lt → loop ⟪ t ,  s  ⟫ {!!} lt )
+       $ λ t _ s P → replaceNodeP key value t (proj1 P)
        $ λ 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 ⟫ ⟫　⟪ proj1 P , ⟪ proj2 P , R ⟫ ⟫
+               (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ proj1 P , ⟪ {!!}  , 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 
 
@@ -172,6 +179,12 @@
 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
 insertTreeSpec0 _ _ _ = tt
 
+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} {A} {t} tree tree1 key value P RT =
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree1 , [] ⟫  ⟪ RTtoTI0 tree tree1 key value P RT , lift tt  ⟫
+       $ λ p P loop → findP key (proj1 p) tree1  (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 → ⊤
 insertTreeSpec1 {n} {A}  tree key value P =
          insertTreeP tree key value P (λ  (tree₁ repl : bt A)