Mercurial > hg > Gears > GearsAgda
changeset 797:03831d974342
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 28 Oct 2023 10:47:31 +0900 |
| parents | e1737f00a7aa |
| children | 794f6d8ddac2 bc75f442d646 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 12 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- 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 )