Mercurial > hg > Gears > GearsAgda

changeset 613:eeb9eb38e5e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
data replacedTree
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Nov 2021 12:58:24 +0900
parents 57d6c594da08
children 0c174b6239a0
files hoareBinaryTree.agda
diffstat 1 files changed, 26 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Fri Nov 05 09:35:20 2021 +0900
+++ b/hoareBinaryTree.agda	Fri Nov 05 12:58:24 2021 +0900
@@ -94,13 +94,13 @@
 stackInvariant {_} {A} tree (x ∷ tail @ (node key value left right ∷ _  )) = ( (left ≡ x) ∧ stackInvariant tree tail) ∨ ( (right ≡ x) ∧ stackInvariant tree tail)
 stackInvariant {_} {A} tree s = Lift _ ⊥
 
-rstackInvariant : {n : Level} {A : Set n} → (tree : bt A) → (stack  : List (bt A)) → Set n
-rstackInvariant {_} {A} _ [] = Lift _ ⊤
-rstackInvariant {_} {A} tree (tree1 ∷ [] ) = tree1 ≡ tree
-rstackInvariant {_} {A} tree (node key value leaf right ∷ x ∷ y )  = (right ≡ x) ∧ rstackInvariant tree (x ∷ y)
-rstackInvariant {_} {A} tree (node key value left leaf ∷ x ∷ y )  = (left ≡ x) ∧ rstackInvariant tree (x ∷ y)
-rstackInvariant {_} {A} tree (node key value left right ∷ x  ∷ y  ) = ( (left ≡ x) ∧ rstackInvariant tree (x ∷ y)) ∨ ( (right ≡ x) ∧ rstackInvariant tree (x ∷ y))
-rstackInvariant {_} {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) )
 
 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
            →  treeInvariant tree ∧ stackInvariant tree stack  
@@ -113,20 +113,20 @@
 findP key n@(node key₁ v tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} {!!}
 
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree )
-    → ((tree : bt A) → treeInvariant tree → (rstack : List (bt A))  → rstackInvariant tree rstack → t) → t
-replaceNodeP k v leaf P next = next (node k v leaf leaf) {!!} {!!} {!!}
-replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!} {!!}
+    → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value tree tree1 → t) → t
+replaceNodeP k v leaf P next = next (node k v leaf leaf) {!!} {!!} 
+replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!}
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack ∧ rstackInvariant repl rstack
-     → (next : ℕ → A → (tree1 : bt A) → (stack rstack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ rstackInvariant repl rstack → bt-depth tree1 < bt-depth tree   → t )
-     → (exit : (tree1 repl : bt A) → (rstack : List (bt A))  → treeInvariant tree1 ∧ rstackInvariant repl rstack → t) → t
-replaceP key value tree repl [] rs Pre next exit = exit tree repl {!!} {!!}  
-replaceP key value tree repl (leaf ∷ st) rs Pre next exit = next key value tree st {!!} {!!} {!!}
-replaceP key value tree repl (node key₁ value₁ left right ∷ st) rs 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 {!!} {!!} {!!}
+     → (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 )
+     → (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 (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 {!!} {!!} 
 
 open import Relation.Binary.Definitions
 
@@ -153,15 +153,15 @@
 open _∧_
 
 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
-     → (exit : (tree repl : bt A) → (rstack : List (bt A)) → treeInvariant tree ∧ rstackInvariant repl rstack  → t ) → t
+     → (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 R → TerminatingLoopS (bt A ∧ List (bt A) ∧ List (bt A))
-            {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p))  ∧ rstackInvariant t1 (proj2 (proj2 p))}
-               (λ p → bt-depth (proj1 p)) ⟪ t , ⟪ s , r ⟫ ⟫　⟪ proj1 P , ⟪ proj2 P , R ⟫ ⟫
-       $  λ p P1 loop → replaceP key value (proj1 p) t1 (proj1 (proj2 p)) (proj2 (proj2 p)) P1 (λ k v t s s1 P2 lt → loop ⟪ t , ⟪  s , s1 ⟫ ⟫ P2 lt ) exit 
+       $ λ 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 
 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
@@ -171,7 +171,7 @@
 
 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) (rstack : List (bt A)) 
-            (P1 : treeInvariant tree₁ ∧ rstackInvariant repl rstack ) → insertTreeSpec0 tree₁ value (lemma1 {!!} ) ) where
+         insertTreeP tree key value P (λ  (tree₁ repl : bt A) 
+            (P1 : treeInvariant tree₁ ∧ replacedTree key value tree₁ repl ) → insertTreeSpec0 tree₁ value (lemma1 {!!} ) ) where
                 lemma1 : (tree₁ : bt A) → top-value tree₁ ≡ just value
                 lemma1 = {!!}