Mercurial > hg > Gears > GearsAgda
changeset 805:28323f2e6dc4
write depth
author | mori |
---|---|
date | Mon, 18 Dec 2023 18:58:21 +0900 |
parents | a03d00eba6b7 |
children | a11ebb914b7c |
files | hoareBinaryTree1.agda |
diffstat | 1 files changed, 9 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Mon Dec 11 19:51:04 2023 +0900 +++ b/hoareBinaryTree1.agda Mon Dec 18 18:58:21 2023 +0900 @@ -203,7 +203,7 @@ ... | tri< a ¬b ¬c = left ... | tri≈ ¬a b ¬c = node key₁ value left right ... | tri> ¬a ¬b c = right - +{- record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where field tree0 : bt A @@ -526,7 +526,7 @@ -- other element is preserved? -- deletion? - +-} data Color : Set where Red : Color Black : Color @@ -626,7 +626,9 @@ → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1) → rotatedTree (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1))) (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr)) - +RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A) +RightDown leaf = leaf +RightDown (node key ⟪ c , value ⟫ t1 t2) = t2 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} → (tleft tright : bt (Color ∧ A)) → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) @@ -977,11 +979,13 @@ ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri≈ ¬a b ¬c = {!!} -- key is unique ? ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri> ¬a ¬b c = ⊥-elim (¬a {!!}) ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb | t = {!!} -- cant happen ? red - red - ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ leaf {!!} {!!} {!!} {!!}) (RBI.replrb r) , {!!} ⟫ -- t₁ t₂ = leaf , c₁ = Red + ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ leaf (RightDown repl) rb-leaf (RBtreeRightDown leaf (RightDown repl) (RBI.replrb r)) (RBI.replrb r)) (RBI.replrb r) , {!!} ⟫ -- t₁ t₂ = leaf , c₁ = Red ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri≈ ¬a b ¬c = {!!} ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim {!!} ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb | t = {!!} --red -red - ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | t = {!!} + ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ ? ? ? ? ? ) ? , ? ⟫ + ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri≈ ¬a b ¬c = {!!} + ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim ? ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ | t = {!!} -- red-red ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | t = {!!} --... | rb-right-black x x₁ t | refl | rb | t = ? --⟪ proj1 {!!} , {!!} ⟫