Mercurial > hg > Gears > GearsAgda

changeset 818:eba0fb12a923

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 Wed, 24 Jan 2024 20:24:41 +0900
parents dfa764ddced2
children 66726208b9f4
files hoareBinaryTree1.agda
diffstat 1 files changed, 25 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed Jan 24 19:52:12 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Jan 24 20:24:41 2024 +0900
@@ -881,6 +881,25 @@
     ... | case2 (case1 x) = {!!}
     ... | case2 (case2 pg) = {!!}
 
+insertCase6 : {n m : Level} {A : Set n} {t : Set m}
+     → (key : ℕ) → (value : A)
+     → (orig tree : bt (Color ∧ A))
+     → (stack : List (bt (Color ∧ A)))
+     → (r : RBI key value orig tree stack )
+     → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A)))
+        → (r : RBI key value orig tree1 stack1 )
+        → length stack1 < length stack  → t )
+     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+        →  stack1 ≡ (orig ∷ [])
+        →  RBI key value orig repl stack1
+        → t ) → t
+insertCase6 {n} {m} {A} {t} key value = {!!} where
+    -- check inner repl case
+    --     node-key parent < node-key grand  → rotateRight grand 
+    --     node-key grand  < node-key parent → rotateLeft  grand 
+    insertCase61 : t
+    insertCase61 = ?
+
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A)
      → (orig tree : bt (Color ∧ A))
@@ -894,18 +913,13 @@
         →  RBI key value orig repl stack1
         → t ) → t
 insertCase5 {n} {m} {A} {t} key value = {!!} where
+    -- check inner repl case
+    --     node-key parent < node-key repl < node-key grand  → rotateLeft  parent    then insertCase6
+    --     node-key grand  < node-key repl < node-key parent → rotateRight parent    then insertCase6
+    --     else insertCase6
     insertCase51 : t
-    insertCase51 with stackToPG {!!} {!!} {!!} {!!}
-    ... | 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)
+    insertCase51 = ?
+
 
 
 --