Mercurial > hg > Gears > GearsAgda

changeset 624:bf27e2c7c6c5

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 Mon, 08 Nov 2021 21:36:28 +0900
parents 753353a41da5
children 074fb29ebf57
files hoareBinaryTree.agda
diffstat 1 files changed, 21 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 08 21:07:41 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 08 21:36:28 2021 +0900
@@ -200,27 +200,27 @@
    
 findPP : {n m : Level} {A : Set n} {t : Set m}
            → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
-           → (C : bt A → List (bt A) → Set n ) (Pre :  findPR tree stack {!!} )
-           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 {!!} →  bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 {!!} → t) → t
-findPP key leaf st C Pre next exit = exit leaf st Pre  
-findPP key (node key₁ v tree tree₁) st C Pre next exit with <-cmp key key₁
-findPP key n st C P next exit | tri≈ ¬a b ¬c = exit n st P 
-findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st C Pre next exit | tri< a ¬b ¬c =
-          next tree (n ∷ st) (record {ti = findPR.ti Pre  ; si = findPP2 st (findPR.si Pre) ; ci = ?} ) findPP1 where 
+           → (Pre :  findPR tree stack (λ t s → Lift n ⊤))
+           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (λ t s → Lift n ⊤) →  bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (λ t s → Lift n ⊤) → t) → t
+findPP key leaf st Pre next exit = exit leaf st Pre  
+findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
+findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st P 
+findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c =
+          next tree (n ∷ st) (record {ti = findPR.ti Pre  ; si = findPP2 st (findPR.si Pre) ; ci = lift tt} ) findPP1 where 
     tree0 =  findPR.tree0 Pre 
     findPP2 : (st : List (bt A)) → stackInvariant {!!} tree0 st →  stackInvariant {!!} tree0 (node key₁ v tree tree₁ ∷ st)
     findPP2 = {!!}
     findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
     findPP1 =  {!!}
-findPP key n@(node key₁ v tree tree₁) st C Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st)
+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 = {!!}
 
 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 , [] ⟫  {!!}
+insertTreePP {n} {m} {A} {t} tree key value  P exit =
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ 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 ))
@@ -238,11 +238,18 @@
      tree1 : bt A
      ci : replacedTree key1 value1 tree tree1
    
+findPPC : {n m : Level} {A : Set n} {t : Set m}
+           → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
+           → (Pre :  findPR tree stack findP-contains)
+           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 findP-contains →  bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 findP-contains → t) → t
+findPPC = {!!}
+
 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 (proj1 p) (proj2 p) {!!} ∧ findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p))
-              ⟪ tree1 , []  ⟫ ⟪ {!!} , record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { tree0 = {!!} ; ti = P ; si = lift tt } } ⟫
-       $ λ p P loop → findPP key (proj1 p) (proj2 p) (proj1 P) (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt ) 
+     {λ p → findPR (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p))
+              ⟪ tree1 , []  ⟫ {!!}
+       $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )  
        $ λ t1 s1 P2 → insertTreeSpec0 t1 value {!!}