# HG changeset patch # User Shinji KONO # Date 1698457651 -32400 # Node ID 03831d974342eaf46d3687f3b9ca5dadb7be1ff2 # Parent e1737f00a7aa62dfb53ee34db4aec5a02de1e69e ... diff -r e1737f00a7aa -r 03831d974342 hoareBinaryTree1.agda --- a/hoareBinaryTree1.agda Thu Oct 26 18:11:17 2023 +0900 +++ b/hoareBinaryTree1.agda Sat Oct 28 10:47:31 2023 +0900 @@ -874,6 +874,17 @@ -- 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) + -- replaced done, clear stack and reconstruct tree + -- we can do this in a codeGear, but to accept context switch during reconstruction, we have to call next + -- this means we have to check prime simple case such as replaced not is exactly the same value / color / key. + insertCase11 : ? + insertCase11 = ? + insertCase10 : (tr0 : bt (Color ∧ A)) → tr0 ≡ RBI.rot r → color tr0 ≡ Black → t + insertCase10 leaf eq refl = exit repl stack ? r -- no stack, replace top node + insertCase10 tr0@(node key₁ ⟪ Black , value₁ ⟫ left right) tr0=rot refl with <-cmp key key₁ + ... | tri< a ¬b ¬c = exit ? stack ? ? + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ? insertCase1 : t insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r) ... | case1 eq = exit repl stack eq r -- no stack, replace top node @@ -896,7 +907,7 @@ -- -- B => B B => B -- / \ / \ / \ rotate L / \ - -- L L1 L R3 L R -- bad B B + -- L L0 L R3 L R -- bad B B -- / \ / \ / \ 1 : child-replace --- L L2 L B L L 2: child-replace ( unbalanced ) -- / \ 3: child-replace ( rotated / balanced )