# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1682899524 -32400
# Node ID 08f752ecf32e3358f4571dc562c2c1ce42497bb5
# Parent  3ce24807611612397b42857e2d7beeaefc599a12
...

diff -r 3ce248076116 -r 08f752ecf32e hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Sun Apr 30 21:12:45 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon May 01 09:05:24 2023 +0900
@@ -649,7 +649,7 @@
      → (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
+     → (next : {key2 d2 : ℕ} {c2 : Color} 
         → (to tr rot rr : bt (Color ∧ A)) 
         →  RBtreeInvariant orig d0 
         →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
@@ -660,9 +660,12 @@
      → (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 {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 = ?
+rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateLeft1 where
+    rotateLeft1 : t
+    rotateLeft1 with stackToPG tree orig stack si
+    ... | case1 x = ?
+    ... | case2 (case1 x) = ?
+    ... | case2 (case2 pg) = ?
 
 rotateRight : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {d0 : ℕ} 
@@ -672,7 +675,7 @@
      → (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
+     → (next : {key2 d2 : ℕ} {c2 : Color}  
         → (to tr rot rr : bt (Color ∧ A)) 
         →  RBtreeInvariant orig d0 
         →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
@@ -683,9 +686,12 @@
      → (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 {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 = ?
+rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateRight1 where
+    rotateRight1 : t
+    rotateRight1 with stackToPG tree orig stack si
+    ... | case1 x = ?
+    ... | case2 (case1 x) = ?
+    ... | case2 (case2 pg) = ?
 
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {d0 : ℕ} 
@@ -695,7 +701,7 @@
      → (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
+     → (next : {key2 d2 : ℕ} {c2 : Color}   
         → (to tr rot rr : bt (Color ∧ A)) 
         →  RBtreeInvariant orig d0 
         →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
@@ -753,24 +759,24 @@
     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 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
+          insertCase5 key value orig tree ? repl rbio ? ? stack si ? ri ? ? 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 ? ? ? ? ? ? ? ? ? ? ? ? ? (λ a b c d e f h i j k l m  → insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit )
-             exit
+          rotateLeft key value orig tree ? repl rbio ? ? stack si ? ri ? ? 
+             (λ a b c d e f h i j k l m  → insertCase5 key value a b c d ? ? h i j k l ? ? 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 ? ? ? ? ? ? ? ? ? ? ? ? ? (λ a b c d e f h i j k l m  → insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit )
-             exit
+          rotateRight key value orig tree ? repl rbio ? ? stack si ? ri ? ? 
+             (λ a b c d e f h i j k l m  → insertCase5 key value a b c d ? ? h i j k l ? ? 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 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
+          insertCase5 key value orig tree ? repl rbio ? ? stack si ? ri ? ? 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)