Mercurial > hg > Gears > GearsAgda

changeset 671:b5fde9727830

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use record invariant for replace
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Nov 2021 22:59:08 +0900
parents 0022b7ce7c16
children 3676e845d46f 7421e5c7e56c
files hoareBinaryTree.agda
diffstat 1 files changed, 27 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 22 21:59:06 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 22 22:59:08 2021 +0900
@@ -260,6 +260,14 @@
 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
 lemma5 (s≤s z≤n) ()
 
+record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
+   field
+     tree0 : bt A
+     ti : treeInvariant tree0
+     si : stackInvariant key tree tree0 stack
+     ri : replacedTree key value (replFromStack si) repl
+     ci : C tree repl stack     -- data continuation
+   
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
     → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
     → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value tree tree1 → t) → t
@@ -267,26 +275,26 @@
 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) → {tree : bt A} ( repl : bt A)
+     → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤) 
+     → (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 {tree0} {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (proj1 (proj2 Pre)) refl ) -- can't happen
-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₁ 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
-... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value  left right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫ ⟫ ≤-refl
-... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫ ⟫ ≤-refl
+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 (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 {!!} (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
 
 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
    → (r : Index) → (p : Invraiant r)