Mercurial > hg > Gears > GearsAgda

changeset 614:0c174b6239a0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
connected
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Nov 2021 13:50:21 +0900
parents eeb9eb38e5e2
children 83e595bba219
files hoareBinaryTree.agda
diffstat 1 files changed, 12 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Fri Nov 05 12:58:24 2021 +0900
+++ b/hoareBinaryTree.agda	Fri Nov 05 13:50:21 2021 +0900
@@ -119,14 +119,14 @@
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack ∧ replacedTree key value tree repl
-     → (next : ℕ → A → (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ replacedTree key value tree tree1 → bt-depth tree1 < bt-depth tree   → t )
+     → (next : ℕ → A → (tree1 repl : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ replacedTree key value tree1 repl → bt-depth tree1 < bt-depth tree   → t )
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
 replaceP key value tree repl [] Pre next exit = exit tree repl {!!} 
-replaceP key value tree repl (leaf ∷ st) Pre next exit = next key value tree st {!!} {!!}
+replaceP key value tree repl (leaf ∷ st) Pre next exit = next key value tree {!!} st {!!} {!!}
 replaceP key value tree repl (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 {!!} {!!} 
+... | 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
 
@@ -152,16 +152,19 @@
 
 open _∧_
 
+
 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)
-       $ λ t1 P1 R → TerminatingLoopS (bt A ∧ List (bt A) ∧ replacedTree key value t t1 )
-            {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p))  ∧ replacedTree key value (proj1 p) {!!} }
-               (λ p → bt-depth (proj1 p)) ⟪ t , ⟪ s , {!!} ⟫ ⟫　⟪ proj1 P , ⟪ proj2 P , {!!} ⟫ ⟫
-       $  λ p P1 loop → {!!} -- replaceP key value (proj1 p) t1 (proj1 (proj2 p)) ?   -- (λ k v t s s1 P2 P3 lt → loop ⟪ t , ⟪  s , ? ⟫ ⟫ ? lt ) exit 
+       $ λ 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 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 
+
 top-value : {n : Level} {A : Set n} → (tree : bt A) →  Maybe A 
 top-value leaf = nothing
 top-value (node key value tree tree₁) = just value