Mercurial > hg > Gears > GearsAgda

changeset 670:0022b7ce7c16

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 Mon, 22 Nov 2021 21:59:06 +0900
parents 077e2f3e417f
children b5fde9727830
files hoareBinaryTree.agda
diffstat 1 files changed, 13 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 22 19:23:20 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 22 21:59:06 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} →  stackInvariant key tree0 tree0 (tree0 ∷ [])
+    s-single :  {tree0 : bt A} → ¬ ( tree0 ≡ leaf ) →  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
@@ -276,9 +276,12 @@
 replaceP key value {tree0} {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (proj1 (proj2 Pre)) -- tree0 ≡ leaf
 ... | refl =  exit tree0 (node key value leaf leaf) ⟪ proj1 Pre ,  r-leaf ⟫
 replaceP key value {tree0} {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) ⟪ proj1 Pre , {!!} ⟫
-... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value  left right )  ⟪ proj1 Pre , {!!} ⟫
-... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree )  ⟪ proj1 Pre , {!!} ⟫
+... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ repl right ) ⟪ proj1 Pre ,  subst (λ k → replacedTree key value k _ ) repl01 (r-left a (proj2 (proj2 Pre))) ⟫ where
+    repl01 : node key₁ value₁ tree right ≡ tree0
+    repl01 with si-property-last _ _ _ _ (proj1 (proj2 Pre))
+    ... | refl = {!!}
+... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value  left right )  ⟪ proj1 Pre , {!!} ⟫ -- can't happen
+... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left repl )  ⟪ proj1 Pre , {!!} ⟫
 replaceP {n} {_} {A} key value {tree0} {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
 replaceP key value {tree0} {tree}  repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit  with <-cmp key key₁
 ... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫  ⟫ ≤-refl