Mercurial > hg > Gears > GearsAgda

changeset 617:bae54f556438

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 13:08:19 +0900
parents 441f3cc79a0b
children 5702800c79bc
files hoareBinaryTree.agda
diffstat 1 files changed, 13 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Sun Nov 07 12:35:03 2021 +0900
+++ b/hoareBinaryTree.agda	Sun Nov 07 13:08:19 2021 +0900
@@ -191,29 +191,28 @@
 findPP key n@(node key₁ v tree tree₁) st Pre next _ | tri< a ¬b ¬c = next tree (n ∷ st) {!!} {!!}  -- Cond n st → Cond tree  (n ∷ st)
 findPP key n@(node key₁ v tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} {!!} -- Cond n st → Cond tree₁ (n ∷ st)
 
-record findPR {n : Level} {A : Set n} (tree : bt A ) → (stack : List (bt A)) : Set n where
+record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
    field
-     ti : tree-invariant tree
-     si : stack-invariant tree stack
+     ti : treeInvariant tree
+     si : stackInvariant tree stack
    
 -- findP key tree stack = findPP key tree stack {findPR} → record { ti = tree-invariant tree ; si stack-invariant tree stack } → 
 
-record findP-contains {n : Level} {A : Set n} (tree : bt A ) → (stack : List (bt A)) : Set n where
+record findP-contains {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
    field
-     key : ℕ
-     value : A
+     key1 : ℕ
+     value1 : A
      tree1 : bt A
-     ci : replacedTree key value tree tree1
-     ti : tree-invariant tree
-     si : stack-invariant tree stack
+     ci : replacedTree key1 value1 tree tree1
+     R : findPR tree stack
    
 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → replacedTree key value tree tree1   → ⊤
 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
-   TerminatingLoopS (bt A ∧ List (bt A) ∧ replacedTree key value {!!} {!!} )
-     {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p)) ∧ replacedTree key value {!!} {!!} } (λ p → bt-depth (proj1 p))
-              ⟪ tree1 , ⟪ [] , RT ⟫  ⟫  ⟪ RTtoTI0 tree tree1 key value P RT , ⟪ lift tt  , {!!} ⟫ ⟫
-       $ λ p P loop → findP key (proj1 p) tree1  (proj1 (proj2 p)) {!!} (λ t _ s P1 lt → loop ⟪ t ,  ⟪ s  , {!!} ⟫ ⟫ {!!} lt )
-       $ λ t _ s P → insertTreeSpec0 t value {!!}
+   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 = tree1 ; ci = {!!} ; R = record { ti = {!!} ; si = {!!} } }
+       $ λ p P loop → findPP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 
+       $ λ t s P → insertTreeSpec0 t value {!!}
 
 insertTreeSpec1 : {n : Level} {A : Set n}  → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
 insertTreeSpec1 {n} {A}  tree key value P =