Mercurial > hg > Members > Moririn

changeset 729:5599bd559f3e

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, 11 Apr 2023 19:08:39 +0900
parents 0786c97b4919
children dbef4bd0f69b
files hoareBinaryTree1.agda
diffstat 1 files changed, 50 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Apr 10 19:15:34 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue Apr 11 19:08:39 2023 +0900
@@ -57,7 +57,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-nil :  {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)} 
@@ -94,22 +94,22 @@
 stack-last (x ∷ s) = stack-last s
 
 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
-stackInvariantTest1 = s-right (add< 3) (s-single  )
+stackInvariantTest1 = s-right (add< 3) (s-nil  )
 
 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-nil  ) ()
 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-nil   ) = 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-nil )  = 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
@@ -129,7 +129,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-nil  ) = 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
@@ -515,7 +515,7 @@
 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
      → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t
 insertTreeP {n} {m} {A} {t} tree key value P0 exit =
-   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫  ⟪ P0 , s-single ⟫
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫  ⟪ P0 , s-nil ⟫
        $ λ p P loop → findP key (proj1 p)  tree (proj2 p) P (λ t s P1 lt → loop ⟪ t ,  s  ⟫ P1 lt ) 
        $ λ t s P C → replaceNodeP key value t C (proj1 P)
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A )
@@ -564,7 +564,7 @@
        → RBTree A key₁ Black (suc d)
 
 data rbstackInvariant {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) : (key₁ : ℕ ) → Set n where
-    s-single :  rbstackInvariant orig key
+    s-nil :  rbstackInvariant orig key
     s-right :  {key₁ key₂ : ℕ} → {c1 : Color} {d1 : ℕ} → key₁ < key₂  →  (top : RBTree A key₁ c1 d1) 
         → rbstackInvariant orig key₁ → rbstackInvariant orig key
     s-left :   {key₁ key₂ : ℕ} → {c1 : Color} {d1 : ℕ} → key₂ < key₁  →  (top : RBTree A key₁ c1 d1) 
@@ -572,7 +572,7 @@
 
 rbsi-len :  {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) {key₁ : ℕ } 
      → rbstackInvariant orig key₁ → ℕ
-rbsi-len orig s-single = 0
+rbsi-len orig s-nil = 0
 rbsi-len orig (s-right x top ri) = suc (rbsi-len orig ri)
 rbsi-len orig (s-left x top ri)  = suc (rbsi-len orig ri)
 
@@ -620,23 +620,48 @@
 findRBP {n} {m} {A} {t} key tree (t-node-red _ value x x₁ tree1 tree2) si next exit = ?
 findRBP {n} {m} {A} {t} key tree (t-node-black _ value x x₁ tree1 tree2) si next exit = ?
 
-record ReplaceRBT {n : Level} {A : Set n} (key : ℕ) (value : A) {key1 key2 d1 d2 : ℕ} {c1 c2 : Color}
-     (tree : RBTree A key1 c1 d1) (repl : RBTree A key2 c2 d2)   : Set n where
-   field
-     key0 d0 : ℕ
-     c0 : Color
-     orig : RBTree A key0 c0 d0
-     si : rbstackInvariant orig key0
-     ri : replacedTree key value (RB→bt A tree) (RB→bt A repl)
-   si-len : ℕ
-   si-len = rbsi-len orig si
+insertCase5 : {n m : Level} {A : Set n} {t : Set m}
+     → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color}  
+     → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
+     → (si : rbstackInvariant orig key1)
+     → (ri : replacedTree key value (RB→bt A tree) (RB→bt A repl))
+     → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) 
+         → (si1 : rbstackInvariant orig k1)
+         → (ri : replacedTree key value (RB→bt A tree1) (RB→bt A repl1))
+         → rbsi-len orig si1 < rbsi-len orig si → t )
+     → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
+         → (ri : replacedTree key value (RB→bt A orig) (RB→bt A repl1))
+         → t ) → t
+insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where
+    rotateRight : ?
+    rotateRight = ?
+    rotateLeft : ?
+    rotateLeft = ?
+    insertCase51 : (key1 : ℕ)  (si : rbstackInvariant orig key1)  → t
+    insertCase51 = ?
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {key1 key2 d1 d2 : ℕ} {c1 c2 : Color}  → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
-     → (RR : ReplaceRBT key value tree repl  )
-     → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl : RBTree A k2 c2 d2 ) → (RR1 : ReplaceRBT key value tree1 repl ) 
-         → ReplaceRBT.si-len RR1 < ReplaceRBT.si-len RR    → t )
-     → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl : RBTree A k2 c2 d2 ) → t ) → t
-replaceRBP = ?
+     → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color}  
+     → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
+     → (si : rbstackInvariant orig key1)
+     → (ri : replacedTree key value (RB→bt A tree) (RB→bt A repl))
+     → (next : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
+         → (ri : replacedTree key value (RB→bt A orig) (RB→bt A repl1))
+         → t ) → t
+replaceRBP {n} {m} {A} {t} key value orig tree repl si ri next = ? where
+    insertCase4 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → (parent : RBTree A ? ? ?) → (grand : RBTree A ? ? ?) → t
+    insertCase4 = ?
+    insertCase3 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → (parent : RBTree A ? ? ?) → (grand : RBTree A ? ? ?) → t
+    insertCase3 = ?
+    insertCase2 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → (parent : RBTree A ? ? ?) → (grand : RBTree A ? ? ?) → t
+    insertCase2 key1 si parent grand = ?
+    replaceRBP1 : (key1 : ℕ)  (si : rbstackInvariant orig key1)  → t
+    replaceRBP1 key1 s-nil = ?
+    replaceRBP1 key1 (s-right {key₁} {key₂} x top s-nil) = ?
+    replaceRBP1 key1 (s-right {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si ? ?
+    replaceRBP1 key1 (s-right {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = ?
+    replaceRBP1 key1 (s-left {key₁} {key₂} x top s-nil) = ?
+    replaceRBP1 key1 (s-left {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = ?
+    replaceRBP1 key1 (s-left {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = ?