Mercurial > hg > Gears > GearsAgda

changeset 676:49f1c24842cb

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 Tue, 23 Nov 2021 20:13:02 +0900
parents 7421e5c7e56c
children 681577b60c35
files hoareBinaryTree.agda
diffstat 1 files changed, 7 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Tue Nov 23 15:11:56 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 23 20:13:02 2021 +0900
@@ -118,14 +118,9 @@
     r-leaf : replacedTree key value leaf (node key value leaf leaf)
     r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 
     r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k < key →  replacedTree key value t1 t2 →  replacedTree key value (node k v1 t t1) (node k v1 t t2) 
+          → k < key →  replacedTree key value t t2 →  replacedTree key value (node k v1 t1 t) t
     r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → 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-right {tree} x  st) = tree
-replFromStack (s-left {tree} x  st) = tree
+          → k > key →  replacedTree key value t t2 →  replacedTree key value (node k v1 t t1) t 
 
 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
 add<  {i} j = begin
@@ -196,8 +191,8 @@
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
-rt-property1 {n} {A} key value .(node _ _ _ _) .(node _ _ _ _) (r-right x rt) ()
-rt-property1 {n} {A} key value .(node _ _ _ _) .(node _ _ _ _) (r-left x rt) ()
+rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = ?
+rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = ?
 
 depth-1< : {i j : ℕ} →   suc i ≤ suc (i Data.Nat.⊔ j )
 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
@@ -265,7 +260,7 @@
      tree0 : bt A
      ti : treeInvariant tree0
      si : stackInvariant key tree tree0 stack
-     ri : replacedTree key value (replFromStack si) repl
+     ri : replacedTree key value tree repl
      ci : C tree repl stack     -- data continuation
    
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
@@ -286,7 +281,7 @@
 replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
 ... | 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 = ?
+    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
@@ -297,7 +292,7 @@
     ... | 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 : replacedTree key value tree (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