Mercurial > hg > Gears > GearsAgda

changeset 694:da42fe4eda54

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
complete insertTreeP
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Dec 2021 15:03:21 +0900
parents 49dd82f49fa1
children ce6cd128595d
files hoareBinaryTree.agda
diffstat 1 files changed, 16 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Thu Dec 02 00:27:11 2021 +0900
+++ b/hoareBinaryTree.agda	Thu Dec 02 15:03:21 2021 +0900
@@ -281,9 +281,15 @@
    
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
     → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
-    → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value tree tree1 → t) → t
-replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf 
-replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) r-node
+    → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value (child-replaced key tree) tree1 → t) → t
+replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf
+replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P)
+     (subst (λ j → replacedTree k v1 j  (node k v1 t t₁) ) repl00 r-node) where -- (child-replaced k (node k value t t₁))
+         repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁)
+         repl00 with <-cmp k k
+         ... | tri< a ¬b ¬c = ⊥-elim (¬b refl)
+         ... | tri≈ ¬a b ¬c = refl
+         ... | tri> ¬a ¬b c = ⊥-elim (¬b refl)
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A)
@@ -535,10 +541,15 @@
        $ λ t s P C → replaceNodeP key value t C (proj1 P)
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A )
             {λ p → replacePR key value  (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p)  (λ _ _ _ → Lift n ⊤ ) }
-               (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = {!!} ; ci = lift tt } -- replacedTree key value (child-replaced key t) t1
+               (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt } -- replacedTree key value (child-replaced key t) t1
        $  λ p P1 loop → replaceP key value  (proj2 (proj2 p)) (proj1 p) P1
             (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1  ⟫ ⟫ P2 lt )  exit 
 
+insertTestP1 = insertTreeP leaf 1 1 _ (λ _ x _ → x )
+insertTestP2 = insertTreeP insertTestP1 2 1 _ (λ _ x _  → x )
+insertTestP3 = insertTreeP insertTestP2 3 2 _ (λ _ x _  → x )
+insertTestP4 = insertTreeP insertTestP3 2 2 _ (λ _ x _  → x )
+
 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
@@ -580,7 +591,7 @@
        $ λ t s _ P → replaceNodeP key value t {!!} {!!}
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
             {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant key (proj1 (proj2 p)) tree (proj1 p)  ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
-               (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!}  , R ⟫ ⟫
+               (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!}  , {!!} ⟫ ⟫
        $  λ p P1 loop → replaceP key value  (proj2 (proj2 p)) (proj1 p) {!!}
             (λ key value repl1 stack P2 lt → loop ⟪ stack , ⟪ {!!} , repl1  ⟫ ⟫ {!!} lt )  exit