Mercurial > hg > Members > Moririn

changeset 754:cda422725f79

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 Sun, 30 Apr 2023 14:31:34 +0900
parents 7127770c2176
children 3ce248076116
files hoareBinaryTree1.agda
diffstat 1 files changed, 81 insertions(+), 47 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri Apr 28 14:13:39 2023 +0900
+++ b/hoareBinaryTree1.agda	Sun Apr 30 14:31:34 2023 +0900
@@ -560,15 +560,15 @@
 RB→bt {n} A leaf = leaf
 RB→bt {n} A (node key ⟪ c , value ⟫ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
 
-data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where
+data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
     s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
-        → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent grand 
+        → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand 
     s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
-        → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent grand 
+        → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand 
     s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
-        → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent grand 
+        → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand 
     s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
-        → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent grand 
+        → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand 
 
 -- with color
 data rotatedTree  {n : Level} {A : Set n}  : (before after : bt A ) → Set n where
@@ -590,8 +590,8 @@
 
 record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where
     field
-       parent grand : bt A
-       pg : ParentGrand self parent grand
+       parent grand uncle : bt A
+       pg : ParentGrand self parent uncle grand
        rest : List (bt A)
        stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
 
@@ -641,6 +641,48 @@
                  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
 findRBT = ?
 
+rotateLeft : {n m : Level} {A : Set n} {t : Set m}
+     → (key : ℕ) → (value : A) → {d0 : ℕ} 
+     → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
+     →  RBtreeInvariant orig d0 
+     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
+     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
+     → rotatedTree tree rot
+     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
+     → (next : {key2 d2 : ℕ} {c2 : Color}   -- rotating case
+        → (to tr rot rr : bt (Color ∧ A)) 
+        →  RBtreeInvariant orig d0 
+        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
+        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
+        → rotatedTree tr rot
+        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+        → length stack1 < length stack  → t )
+     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
+        →  {d : ℕ} → RBtreeInvariant repl d 
+        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+rotateLeft = ?
+
+rotateRight : {n m : Level} {A : Set n} {t : Set m}
+     → (key : ℕ) → (value : A) → {d0 : ℕ} 
+     → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
+     →  RBtreeInvariant orig d0 
+     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
+     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
+     → rotatedTree tree rot
+     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
+     → (next : {key2 d2 : ℕ} {c2 : Color}   -- rotating case
+        → (to tr rot rr : bt (Color ∧ A)) 
+        →  RBtreeInvariant orig d0 
+        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
+        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
+        → rotatedTree tr rot
+        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+        → length stack1 < length stack  → t )
+     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
+        →  {d : ℕ} → RBtreeInvariant repl d 
+        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+rotateRight = ?
+
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {d0 : ℕ} 
      → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
@@ -661,12 +703,8 @@
         →  {d : ℕ} → RBtreeInvariant repl d 
         → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
 insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where
-    insertCase51 : (key1 : ℕ)  (si : ParentGrand ? ? ? )  → t
+    insertCase51 : (key1 : ℕ)  (si : ParentGrand ? ? ? ? )  → t
     insertCase51 = ?
-    rotateRight : ?
-    rotateRight = ?
-    rotateLeft : ?
-    rotateLeft = ?
 
 
 -- if we have replacedNode on RBTree, we have RBtreeInvariant
@@ -689,45 +727,41 @@
         →  {d : ℕ} → RBtreeInvariant repl d 
         → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
 replaceRBP {n} {m} {A} {t} key value orig tree repl rbio rbit rbir stack si ri next exit = ? where
-    insertCase2 : (tree parent grand : bt (Color ∧ A)) 
+    insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) 
       → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
-      → (pg : ParentGrand tree parent grand ) → t
-    insertCase2 tree parent grand stack si pg with color A parent
-    ... | Black = ?   -- tree stuctre is preserved
-    ... | Red = ? where  -- insertCase3 grand refl where
-        --
-        --  in some case, stack is poped and loop to replaceRBP
-        --     it means, we have to create replacedTree
-        --     g     
-        --   u   p    
-        --     _   s   
-        insertCase3 : ( tp tg : bt (Color ∧ A) ) → tp ≡ parent → tg ≡ grand → t
-        insertCase3 tp leaf tp=p tg=g = ?
-        insertCase3 tp (node kg value leaf tr₁) tp=p tg=g = ?
-        insertCase3 leaf (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) tp=p tg=g = ? -- can't happen
-        insertCase3 (node kp value₁ tp tp₁) (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) tp=p tg=g with <-cmp ku kp
-        ... | tri< a ¬b ¬c = next ? ? ? ? ? ? ? ? ? ?
-        ... | tri≈ ¬a b ¬c = ? -- can't happen
-        ... | tri> ¬a ¬b c = next ? ? ? ? ? ? ? ? ? ?
-        insertCase3 leaf (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) tp=p tg=g = ? -- can't happen
-        insertCase3 (node kp value₁ tpl tpr) (node kg value (node ku ⟪ Black , vu ⟫ tgl tgr) tr₁) tp=p tg=g with <-cmp ku kp
-        ... | tri< a ¬b ¬c = ? where
-            insertCase4 : ( right-tp left-tg : bt (Color ∧ A) ) → right-tp ≡ tpr → left-tg ≡ tgl → t
-            insertCase4 leaf lg eq1 eq2 = ?
-            insertCase4 (node krp value rp rp₁) leaf eq1 eq2 = ?
-            insertCase4 (node krp value rp rp₁) (node klg value₁ lg lg₁) eq1 eq2 with <-cmp key krp | <-cmp kp klg
-            ... | ttt4 | ttt5 = ? where
-                insertCase41 : ( left-tp right-tg : bt (Color ∧ A) ) → left-tp ≡ tpl → right-tg ≡ tgr → t
-                insertCase41 leaf rg eq3 eq4 = ?
-                insertCase41 (node klp value lp lp₁) leaf eq3 eq4 = ?
-                insertCase41 (node klp value lp lp₁) (node krg value₁ rg rg₁) eq3 eq4 with <-cmp key klp | <-cmp kp krg
-                ... | ttt4 | ttt5 = ? where
-        ... | tri≈ ¬a b ¬c = ? -- can't happen
-        ... | tri> ¬a ¬b c = ?
+      → (pg : ParentGrand tree parent uncle grand ) → t
+    insertCase2 tree leaf uncle grand stack si (s2-s1p2 () x₁) 
+    insertCase2 tree leaf uncle grand stack si (s2-1sp2 () x₁) 
+    insertCase2 tree leaf uncle grand stack si (s2-s12p () x₁) 
+    insertCase2 tree leaf uncle grand stack si (s2-1s2p () x₁) 
+    insertCase2 tree parent@(node kp ⟪ Red , _ ⟫ _ _) uncle grand stack si pg = next ? ? ? ? ? ? ? ? ? ?
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) leaf grand stack si pg = ?
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = next ? ? ? ? ? ? ? ? ? ?
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = 
+          insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? ? exit
+      -- tree is left of parent, parent is left of grand
+      --  node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
+      --  grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1sp2 x x₁) = 
+          rotateLeft ? ? ? ? ? ? ? ? ? ? ? ? ? ? -- insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? ?   )
+             exit
+      -- tree is right of parent, parent is left of grand  rotateLeft
+      --  node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
+      --  grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s12p x x₁) = 
+          rotateRight ? ? ? ? ? ? ? ? ? ? ? ? ? ? exit
+      -- tree is left of parent, parent is right of grand, rotateRight
+      -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
+      --  grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1s2p x x₁) = 
+          insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? ? exit
+      -- tree is right of parent, parent is right of grand
+      -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
+      -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
     insertCase1 with stackToPG tree orig stack si
     ... | case1 eq = ?
     ... | case2 (case1 eq ) = ?
-    ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.grand pg) stack si (PG.pg pg) 
+    ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)