Mercurial > hg > Gears > GearsAgda

changeset 619:a3fbc9b57015

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 Sun, 07 Nov 2021 19:43:16 +0900
parents 5702800c79bc
children fe8c2d82c05c
files hoareBinaryTree.agda
diffstat 1 files changed, 24 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Sun Nov 07 18:35:31 2021 +0900
+++ b/hoareBinaryTree.agda	Sun Nov 07 19:43:16 2021 +0900
@@ -179,25 +179,34 @@
 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
 insertTreeSpec0 _ _ _ = tt
 
-record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) (C : Set n) : Set n where
+record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
    field
+     tree0 : bt A
      ti : treeInvariant tree
-     si : stackInvariant tree stack
-     opt : C
-     opt1 : C → C
+     si : stackInvariant tree0 stack
    
 findPP : {n m : Level} {A : Set n} {t : Set m}
            → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
-           → {Cond : bt A → List (bt A) → Set n}
-           → (Pre :   bt A → List (bt A) →  findPR tree stack (Cond tree stack) )
-           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (Cond tree1 stack1) →  bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (Cond tree1 stack1) → t) → t
+           → (Pre :   bt A → List (bt A) →  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 Pre next exit = exit leaf st (Pre leaf st ) 
 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 n st) 
-findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c = next tree (n ∷ st) (record {ti = {!!} ; si = {!!} ; opt = {!!} ; opt1 = id } ) findPP1 where -- Cond n st → Cond tree  (n ∷ st)
-    findPP0 : {!!}
-    findPP0 = {!!}
+findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c =
+          next tree (n ∷ st) (record {ti = findPP0 tree tree₁ (findPR.ti (Pre n st)) ; si = findPP2 st (findPR.si (Pre n st))} ) findPP1 where 
+    tree0 =  findPR.tree0 (Pre n st)
+    findPP0 : (tree tree₁ : bt A) → treeInvariant ( node key₁ v tree tree₁ ) → treeInvariant tree
+    findPP0 leaf t x = tt
+    findPP0 (node key value tree tree₁) leaf x = proj1 x
+    findPP0 (node key value tree tree₁) (node key₁ value₁ t t₁) x = proj1 x
+    findPP2 : (st : List (bt A)) → stackInvariant tree0 st →  stackInvariant tree0 (node key₁ v tree tree₁ ∷ st)
+    findPP2 [] (lift tt) = {!!}
+    findPP2 (leaf ∷ st) x = {!!}
+    findPP2 (node key value leaf leaf ∷ st) x = {!!}
+    findPP2 (node key value leaf (node key₁ value₁ x₂ x₃) ∷ st) x = {!!}
+    findPP2 (node key value (node key₁ value₁ x₁ x₃) leaf ∷ st) x = {!!}
+    findPP2 (node key value (node key₁ value₁ x₁ x₃) (node key₂ value₂ x₂ x₄) ∷ st) x = case1 ⟪ {!!} , {!!} ⟫
     findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
     findPP1 =  {!!}
 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)
@@ -207,7 +216,7 @@
 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 , [] ⟫  {!!}
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) } (λ 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 ))
@@ -228,9 +237,9 @@
 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 → findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p))
-              ⟪ tree1 , []  ⟫ record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { ti = P ; si = lift tt } }
-       $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 
+     {λ 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) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt ) 
        $ λ t s P → insertTreeSpec0 t value {!!}
 
 insertTreeSpec1 : {n : Level} {A : Set n}  → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤