changeset 675:7421e5c7e56c

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Nov 2021 15:11:56 +0900
parents b5fde9727830
children 49f1c24842cb
files hoareBinaryTree.agda
diffstat 1 files changed, 24 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 22 22:59:08 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 23 15:11:56 2021 +0900
@@ -108,7 +108,7 @@
 --  stack always contains original top at end
 --
 data stackInvariant {n : Level} {A : Set n}  (key : ℕ) : (top orig : bt A) → (stack  : List (bt A)) → Set n where
-    s-single :  {tree0 : bt A} → ¬ ( tree0 ≡ leaf ) →  stackInvariant key tree0 tree0 (tree0 ∷ [])
+    s-single :  {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
     s-right :  {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
         → key₁ < key  →  stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
     s-left :  {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
@@ -123,7 +123,7 @@
           → k > key →  replacedTree key value t1 t2 →  replacedTree key value (node k v1 t1 t) (node k v1 t2 t) 
 
 replFromStack : {n : Level} {A : Set n}  {key : ℕ} {top orig : bt A} → {stack  : List (bt A)} →  stackInvariant key top orig stack → bt A
-replFromStack (s-single {tree} _ ) = tree
+replFromStack (s-single {tree} ) = tree
 replFromStack (s-right {tree} x  st) = tree
 replFromStack (s-left {tree} x  st) = tree
 
@@ -150,22 +150,22 @@
 stack-last (x ∷ s) = stack-last s
 
 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
-stackInvariantTest1 = s-right (add< 2) (s-single  (λ ()))
+stackInvariantTest1 = s-right (add< 2) (s-single  )
 
 si-property0 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] )
-si-property0  (s-single _ ) ()
+si-property0  (s-single  ) ()
 si-property0  (s-right x si) ()
 si-property0  (s-left x si) ()
 
 si-property1 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 (tree1 ∷ stack)
    → tree1 ≡ tree
-si-property1 (s-single  _ ) = refl
+si-property1 (s-single   ) = refl
 si-property1 (s-right _  si) = refl
 si-property1 (s-left _  si) = refl
 
 si-property-last :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
    → stack-last stack ≡ just tree0
-si-property-last key t t0 (t ∷ [])  (s-single _)  = refl
+si-property-last key t t0 (t ∷ [])  (s-single )  = refl
 si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with  si-property1 si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with  si-property1  si
@@ -185,7 +185,7 @@
 
 stackTreeInvariant : {n  : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A))
    →  treeInvariant tree → stackInvariant key sub tree stack  → treeInvariant sub
-stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single  _) = ti
+stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single  ) = ti
 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si ) = ti-right (si1 si) where
    si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} →  stackInvariant key (node key₁ v1 tree₁ sub ) tree st → treeInvariant  (node key₁ v1 tree₁ sub )
    si1 {tree₁ }  {key₁ }  {v1 }  si = stackTreeInvariant  key (node key₁ v1 tree₁ sub ) tree st ti si
@@ -280,21 +280,27 @@
      → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
          → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
-replaceP key value {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 {!!} refl ) -- can't happen
-replaceP key value {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  {!!} -- tree0 ≡ leaf
-... | eq =  exit {!!} (node key value leaf leaf) ⟪ {!!} ,  r-leaf ⟫
+replaceP key value {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
+replaceP key value {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (replacePR.si Pre)-- tree0 ≡ leaf
+... | eq =  exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre ,  {!!} ⟫
 replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = exit {!!} (node key₁ value₁ repl right ) {!!} where
-    repl01 : node key₁ value₁ tree right ≡ {!!}
-    repl01 with si-property-last _ _ _ _ {!!}
-    ... | eq = {!!}
+... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , {!!} ⟫ where
+    repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right)
+    repl01 = ?
 ... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value  left right )  ⟪ {!!} , {!!} ⟫ -- can't happen
 ... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl )  ⟪ {!!} , {!!} ⟫
 replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
-replaceP key value {tree}  repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value {{!!}} (node key₁ value₁ tree right ) st {!!} ≤-refl
-... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl
-... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
+replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ | si-property1 (replacePR.si Pre)
+... | tri< a ¬b ¬c | refl = next key value {{!!}} (node key₁ value₁ repl right ) st Post ≤-refl where
+    Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
+    Post with replacePR.si Pre
+    ... | s-right x t = {!!}
+    ... | s-left lt si with si-property1 si
+    ... | refl = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si  ; ri = {!!} ; ci = lift tt } where
+        repl02 : replacedTree key value (replFromStack si) (node key₁ value₁ repl right)
+        repl02 = {!!}
+... | tri≈ ¬a b ¬c | refl = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl -- can't happen
+... | tri> ¬a ¬b c | refl = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
 
 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
    → (r : Index) → (p : Invraiant r)