Mercurial > hg > Gears > GearsAgda
changeset 651:7b9d35f7c033
fix stack top and replaced tree
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 20 Nov 2021 14:24:22 +0900 |
| parents | 11388cab162f |
| children | 8c7446829b99 |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 22 insertions(+), 23 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Sat Nov 20 08:34:59 2021 +0900 +++ b/hoareBinaryTree.agda Sat Nov 20 14:24:22 2021 +0900 @@ -252,42 +252,41 @@ 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 replaceP : {n m : Level} {A : Set n} {t : Set m} - → (key : ℕ) → (value : A) → {tree0 tree : bt A} ( repl : bt A) - → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree tree0 stack ∧ replacedTree key value tree repl - → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) - → treeInvariant tree0 ∧ stackInvariant key tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) + → (key : ℕ) → (value : A) → {tree0 tree tree-st : bt A} ( repl : bt A) + → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack ∧ replacedTree key value tree repl + → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A)) + → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t -replaceP key value {tree0} {tree} repl [] Pre next exit with proj1 (proj2 Pre) +replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit with proj1 (proj2 Pre) ... | () -replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ []) Pre next exit = - exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (repl4 (proj1 (proj2 Pre))) (proj2 (proj2 Pre)) ⟫ where - repl4 : stackInvariant key tree tree0 (leaf ∷ []) → tree ≡ tree0 +replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit = + exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (repl4 (proj1 (proj2 Pre))) {!!} ⟫ where + repl41 : tree-st ≡ tree + repl41 = {!!} + repl4 : stackInvariant key tree-st tree0 (leaf ∷ []) → tree-st ≡ tree0 repl4 (s-single .leaf) = refl -replaceP key value {tree0} {tree} repl (leaf ∷ leaf ∷ st) Pre next exit = ⊥-elim ( repl3 (proj1 (proj2 Pre))) where -- can't happen - repl3 : stackInvariant key tree tree0 (leaf ∷ leaf ∷ st) → ⊥ +replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ leaf ∷ st) Pre next exit = ⊥-elim ( repl3 (proj1 (proj2 Pre))) where -- can't happen + repl3 : stackInvariant key tree-st tree0 (leaf ∷ leaf ∷ st) → ⊥ repl3 (s-right x ()) repl3 (s-left x ()) -replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ +replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) (node key₁ value₁ tree right ∷ st) ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where - repl5 : stackInvariant key tree tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st ) + repl5 : stackInvariant key tree-st tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st ) repl5 (s-right x si) with si-property1 _ _ _ _ si ... | refl = ⊥-elim (nat-<> a x) - repl5 (s-left x si) with si-property1 _ _ _ _ si - ... | refl = si + repl5 (s-left x si) with si-property1 _ _ _ _ si -- stackInvariant key (node key₁ value₁ leaf right) tree0 (node key₁ value₁ leaf right ∷ st) + -- stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st) + ... | refl = {!!} -- tree ≡ leaf ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3< ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3< -replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ +replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen -... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where - repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 st - repl2 (s-single .(node key₁ value₁ left right)) = {!!} - repl2 (s-right x si) with si-property1 _ _ _ _ si - ... | eq = {!!} - repl2 (s-left x si) with si-property1 _ _ _ _ si - ... | eq = ? - +... | tri< a ¬b ¬c with proj1 (proj2 Pre) +... | s-single .(node key₁ value₁ left right) = {!!} +... | s-right x si1 = {!!} +... | s-left x si1 = next key value (node key₁ value₁ repl right ) st ⟪ proj1 Pre , ⟪ si1 , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) → (r : Index) → (p : Invraiant r)