Mercurial > hg > Members > Moririn

changeset 697:e5140faf1602

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 Sat, 04 Dec 2021 14:47:03 +0900
parents 578f29a76857
children 28e0f7f4777d
files hoareBinaryTree.agda
diffstat 1 files changed, 9 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Fri Dec 03 11:14:19 2021 +0900
+++ b/hoareBinaryTree.agda	Sat Dec 04 14:47:03 2021 +0900
@@ -610,11 +610,16 @@
 findPPC key (node key₁ v1 tree tree₁) st Pre next exit with <-cmp key key₁
 findPPC key n st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
 findPPC {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st)
-       record { tree0 = findPR.tree0 Pre ; ti0 = findPR.ti0 Pre  ; ti = treeLeftDown tree tree₁ (findPR.ti Pre)  ; si =  findP1 a st (findPR.si Pre)
+       record { tree0 = findPR.tree0 Pre ; ti0 = findPR.ti0 Pre  ; ti = treeLeftDown tree tree₁ (findPR.ti Pre)  ; si =  s-left a (findPR.si Pre)
           ; ci = {!!} } depth-1< where
-   findP1 : key < key₁ → (st : List (bt A)) →  stackInvariant key (node key₁ v1 tree tree₁)
-         (findPR.tree0 Pre) st → stackInvariant key tree (findPR.tree0 Pre) (tree ∷ st)
-   findP1 a (x ∷ st) si = s-left a si
+   findP2 : findPC key tree (tree ∷ st)
+   findP2 with findPC.ci (findPR.ci Pre) | findPC.tree1 (findPR.ci Pre)
+   findP2 | r-node | leaf = {!!}
+   findP2 | r-node | node key value t t₁ = record { tree1 = t ; value = findPC.value (findPR.ci Pre)  ; ci =  {!!} }
+   findP2 | (r-right x ri) | t = ⊥-elim (nat-<> x a)
+   findP2 | (r-left x ri) | node key value t t₁ = record { tree1 = t ; value = findPC.value (findPR.ci Pre)  ; ci =  {!!} }
+   findP2 | r-left x ri | leaf = {!!}
+   -- findP2 (r-left x ri) = subst₂ (λ j k →  replacedTree key (findPC.value (findPR.ci Pre)) j k ) {!!} {!!} ri 
 findPPC key n@(node key₁ v1 tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st)
        record { tree0 = findPR.tree0 Pre ; ti0 = findPR.ti0 Pre ; ti = treeRightDown tree tree₁ (findPR.ti Pre) ; si =  s-right c (findPR.si Pre)
           ; ci = {!!} }  depth-2<