Mercurial > hg > Members > Moririn

changeset 755:3ce248076116

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 21:12:45 +0900
parents cda422725f79
children 08f752ecf32e
files hoareBinaryTree1.agda
diffstat 1 files changed, 31 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sun Apr 30 14:31:34 2023 +0900
+++ b/hoareBinaryTree1.agda	Sun Apr 30 21:12:45 2023 +0900
@@ -660,7 +660,9 @@
      → (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 = ?
+rotateLeft {n} {m} {A} {t} key value orig .orig rot repl rbo rbt rbr .(orig ∷ []) s-nil ri rr next exit = ?
+rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr .(tree ∷ _) (s-right x si) ri rr next exit = ?
+rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr .(tree ∷ _) (s-left x si) ri rr next exit = ?
 
 rotateRight : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {d0 : ℕ} 
@@ -681,7 +683,9 @@
      → (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 = ?
+rotateRight {n} {m} {A} {t} key value orig .orig rot repl rbo rbt rbr .(orig ∷ []) s-nil ri rr next exit = ?
+rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr .(tree ∷ _) (s-right x si) ri rr next exit = ?
+rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr .(tree ∷ _) (s-left x si) ri rr next exit = ?
 
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {d0 : ℕ} 
@@ -702,9 +706,19 @@
      → (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
-insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where
-    insertCase51 : (key1 : ℕ)  (si : ParentGrand ? ? ? ? )  → t
-    insertCase51 = ?
+insertCase5 {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = insertCase51 where
+    insertCase51 : t
+    insertCase51 with stackToPG tree orig stack si
+    ... | case1 eq = ?
+    ... | case2 (case1 eq ) = ?
+    ... | case2 (case2 pg) with PG.pg pg
+    ... | s2-s1p2 x x₁ = rotateRight ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
+       -- x     : PG.parent pg ≡ node kp vp tree n1
+       -- x₁    : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
+    ... | s2-1sp2 x x₁ = rotateLeft ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
+    ... | s2-s12p x x₁ = rotateLeft ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
+    ... | s2-1s2p x x₁ = rotateLeft ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
+    -- = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 
 
 
 -- if we have replacedNode on RBTree, we have RBtreeInvariant
@@ -716,17 +730,18 @@
      →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
      → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
      → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tree) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color}   -- no rotating case
-        → (to tr rr : bt (Color ∧ A)) 
+     → (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 
-        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tr) rr
+        → 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
-replaceRBP {n} {m} {A} {t} key value orig tree repl rbio rbit rbir stack si ri next exit = ? where
+replaceRBP {n} {m} {A} {t} key value orig tree repl rbio rbit rbir stack si ri next exit = insertCase1 where
     insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) 
       → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
       → (pg : ParentGrand tree parent uncle grand ) → t
@@ -734,27 +749,28 @@
     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 ⟪ 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 ⟪ Red , _ ⟫ _ _ ) grand stack si pg = next ? ? ? ? ? ? ? ? ? ? ? ?
     insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = 
-          insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? ? exit
+          insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next 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 ? ? ? ? ? ? ? ? ? ? ? ? ? ?   )
+          rotateLeft ? ? ? ? ? ? ? ? ? ? ? ? ? (λ a b c d e f h i j k l m  → insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit )
              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
+          rotateRight ? ? ? ? ? ? ? ? ? ? ? ? ? (λ a b c d e f h i j k l m  → insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit )
+             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
+          insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next 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)