Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 798:794f6d8ddac2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
10/28
author Moririn
date Sat, 28 Oct 2023 19:11:12 +0900
parents 03831d974342
children 418ab1fa2aca
comparison
equal deleted inserted replaced
797:03831d974342 798:794f6d8ddac2
875 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree 875 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
876 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) 876 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
877 -- replaced done, clear stack and reconstruct tree 877 -- replaced done, clear stack and reconstruct tree
878 -- we can do this in a codeGear, but to accept context switch during reconstruction, we have to call next 878 -- we can do this in a codeGear, but to accept context switch during reconstruction, we have to call next
879 -- this means we have to check prime simple case such as replaced not is exactly the same value / color / key. 879 -- this means we have to check prime simple case such as replaced not is exactly the same value / color / key.
880 insertCase11 : ? 880 insertCase11 : {!!}
881 insertCase11 = ? 881 insertCase11 = {!!}
882 insertCase10 : (tr0 : bt (Color ∧ A)) → tr0 ≡ RBI.rot r → color tr0 ≡ Black → t 882 insertCase10 : (tr0 : bt (Color ∧ A)) → tr0 ≡ RBI.rot r → color tr0 ≡ Black → t
883 insertCase10 leaf eq refl = exit repl stack ? r -- no stack, replace top node 883 insertCase10 leaf eq refl = exit repl stack {!!} r -- no stack, replace top node
884 insertCase10 tr0@(node key₁ ⟪ Black , value₁ ⟫ left right) tr0=rot refl with <-cmp key key₁ 884 insertCase10 tr0@(node key₁ ⟪ Black , value₁ ⟫ left right) tr0=rot refl with <-cmp key key₁
885 ... | tri< a ¬b ¬c = exit ? stack ? ? 885 ... | tri< a ¬b ¬c = exit {!!} stack {!!} {!!}
886 ... | tri≈ ¬a b ¬c = ? 886 ... | tri≈ ¬a b ¬c = {!!}
887 ... | tri> ¬a ¬b c = ? 887 ... | tri> ¬a ¬b c = {!!}
888 insertCase1 : t 888 insertCase1 : t
889 insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r) 889 insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)
890 ... | case1 eq = exit repl stack eq r -- no stack, replace top node 890 ... | case1 eq = exit repl stack eq r -- no stack, replace top node
891 ... | case2 (case1 eq) = insertCase12 orig refl (RBI.si r) where 891 ... | case2 (case1 eq) = insertCase12 orig refl (RBI.si r) where
892 -- one level stack, orig is parent of repl 892 -- one level stack, orig is parent of repl
893 rb01 : stackInvariant key (RBI.tree r) orig stack 893 rb01 : stackInvariant key (RBI.tree r) orig stack
894 rb01 = RBI.si r 894 rb01 = RBI.si r
895 insertCase12 : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig 895 insertCase12 : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
896 → stackInvariant key (RBI.tree r) orig stack 896 → stackInvariant key (RBI.tree r) orig stack
897 → t 897 → t
898 insertCase12 leaf eq1 si = ? -- can't happen 898 insertCase12 leaf eq1 si = {!!} -- can't happen
899 insertCase12 tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left (RBI.rot r)) in eqcr 899 insertCase12 tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left (RBI.rot r)) in eqcr
900 ... | tri< a ¬b ¬c | cr = ? 900 ... | tri< a ¬b ¬c | cr = {!!}
901 ... | tri≈ ¬a b ¬c | cr = ? -- can't happen 901 ... | tri≈ ¬a b ¬c | cr = {!!} -- can't happen
902 ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where 902 ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where
903 -- 903 --
904 -- orig B 904 -- orig B
905 -- / \ 905 -- / \
906 -- left tree → rot → repl R 906 -- left tree → rot → repl R
930 ; ri = proj2 rb05 930 ; ri = proj2 rb05
931 ; repl-red = refl 931 ; repl-red = refl
932 ; repl-eq = rb07 932 ; repl-eq = rb07
933 } where 933 } where
934 rb07 : black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl 934 rb07 : black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl
935 rb07 = ? 935 rb07 with <-cmp key key₁
936 -- rb05 should more general 936 ... | tri< a ¬b ¬c = {!!}
937 ... | tri≈ ¬a b ¬c = {!!}
938 ... | tri> ¬a ¬b c = {!!}
939 -- rb05 should more general
937 rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧ replacedRBTree key value 940 rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧ replacedRBTree key value
938 (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl) 941 (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl)
939 rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl 942 rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl
940 ... | rb-single key₂ value₂ | refl | rb-single key value = ? 943 ... | rb-single key₂ value₂ | refl | rb-single key₃ value₃ = ⟪ rb-right-red {!!} refl (RBI.replrb r) , {!!} ⟫
941 ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = ? 944 ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = {!!}
942 ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = ? 945 ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = {!!}
943 ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = ? 946 ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = {!!}
944 ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = ? 947 ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = {!!}
945 ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = ? 948 ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = {!!}
946 ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = ? 949 ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = {!!}
947 ... | rb-right-black x x₁ t | refl | rb = ? 950 ... | rb-right-black x x₁ t | refl | rb = {!!}
948 ... | rb-left-black x x₁ t | refl | rb = ? 951 ... | rb-left-black x x₁ t | refl | rb = {!!}
949 ... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb = ? 952 ... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb = {!!}
950 insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r) 953 insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
951 ... | Black = exit ? ? ? ? 954 ... | Black = exit {!!} {!!} {!!} {!!}
952 ... | Red = exit ? ? ? ? 955 ... | Red = exit {!!} {!!} {!!} {!!}
953 -- r = orig RBI.tree b 956 -- r = orig RBI.tree b
954 -- / \ => / \ 957 -- / \ => / \
955 -- b b → r RBI.tree r r = orig o (r/b) 958 -- b b → r RBI.tree r r = orig o (r/b)
956 ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 959 ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)
957 960