Mercurial > hg > Gears > GearsAgda

changeset 629:7a19d4b43795

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 Tue, 09 Nov 2021 09:31:43 +0900
parents ec2506b532ba
children 24bec7639079
files hoareBinaryTree.agda
diffstat 1 files changed, 17 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 08 23:44:24 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 09 09:31:43 2021 +0900
@@ -229,26 +229,33 @@
        $  λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!}
             (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1  , repl1  ⟫ ⟫ {!!} lt )  exit 
 
-record findP-contains {n : Level} {A : Set n} (key1 : ℕ) (value1 : A) (tree : bt A ) (stack : List (bt A)) : Set n where
+record findPC {n : Level} {A : Set n} (key1 : ℕ) (value1 : A) (tree : bt A ) (stack : List (bt A)) : Set n where
    field
      tree1 : bt A
      ci : replacedTree key1 value1 tree tree1
    
 findPPC : {n m : Level} {A : Set n} {t : Set m}
            → (key : ℕ) → (value : A) → (tree : bt A ) → (stack : List (bt A))
-           → (Pre :  findPR key tree stack (findP-contains key value))
-           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 (findP-contains key value) →  bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key)  → findPR key tree1 stack1 (findP-contains key value) → t) → t
-findPPC = {!!}
+           → (Pre :  findPR key tree stack (findPC key value))
+           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 (findPC key value) →  bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key)  → findPR key tree1 stack1 (findPC key value) → t) → t
+findPPC key value leaf st Pre next exit = exit leaf st (case1 refl) Pre  
+findPPC key value (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
+findPPC key value n st P next exit | tri≈ ¬a b ¬c = exit n st (case2 {!!}) P 
+findPPC {_} {_} {A} key value n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c =
+          next tree (n ∷ st) (record {ti = findPR.ti Pre  ; si = {!!} ; ci =  {!!} } ) {!!} 
+findPPC key value n st P next exit | tri> ¬a ¬b c = {!!}
 
 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 → findPR key (proj1 p) (proj2 p) (findP-contains key value ) } (λ p → bt-depth (proj1 p))
+     {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p))
               ⟪ tree1 , []  ⟫ {!!}
        $ λ p P loop → findPPC key value (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )  
-       $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma7 {!!} (findPR.si P2 ) found?  ) where
-           lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } →
-              replacedTree key value1 tree t1 → stackInvariant key t1 tree s1  → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key)  →   top-value t1 ≡ just value
-           lemma7 = {!!}
+       $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where
+           lemma6 : (t1 : bt A) (s1 : List (bt A)) (found? : (t1 ≡ leaf) ∨ (node-key t1 ≡ just key)) (P2 : findPR key t1 s1 (findPC key value)) → top-value t1 ≡ just value
+           lemma6 t1 s1 found? P2 = lemma7 t1 s1 (findPR.tree0 P2) ( findPC.tree1  (findPR.ci P2)) ( findPC.ci  (findPR.ci P2)) (findPR.si P2) found? where
+              lemma7 :  (t1 : bt A) ( s1 : List (bt A) ) (tree0 tree1 : bt A) →
+                 replacedTree key value t1 tree1 → stackInvariant key t1 tree0 s1  → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key)  →   top-value t1 ≡ just value
+              lemma7 = {!!}