Mercurial > hg > Members > Moririn
changeset 762:56de8e7dca7a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 May 2023 10:14:53 +0900 |
| parents | 927c02120a73 |
| children | 799325a71422 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 7 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Thu May 04 18:40:10 2023 +0900 +++ b/hoareBinaryTree1.agda Fri May 05 10:14:53 2023 +0900 @@ -639,12 +639,6 @@ → stack ≡ orig ∷ [] → tree ≡ orig stackCase1 s-nil refl = refl -stackCase2 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A } - → {stack : List (bt A)} → stackInvariant key tree orig stack - → stack ≡ tree ∷ orig ∷ [] → {k1 : ℕ} {v1 : A} → (orig ≡ node k1 v1 tree leaf) ∨ (orig ≡ node k1 v1 leaf tree ) -stackCase2 (s-right x s-nil) refl = case2 ? -stackCase2 (s-left x si) refl = ? - PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) ) → RBtreeInvariant orig d0 → (stack : List (bt (Color ∧ A))) → (pg : PG (Color ∧ A) tree stack ) @@ -803,8 +797,13 @@ insertCase1 with stackToPG tree orig stack si ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri ... | case2 (case1 eq ) = ? where - insertCase12 : t - insertCase12 = ? + insertCase12 : (orig : bt (Color ∧ A)) + → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key tree orig stack ) + → stack ≡ tree ∷ orig ∷ [] → t + insertCase12 (node k1 ⟪ Red , v1 ⟫ t1 tree) (s-right x s-nil) refl = exit rot repl rbir ? ? + insertCase12 (node k1 ⟪ Black , v1 ⟫ t1 tree) (s-right x s-nil) refl = ? + insertCase12 (node k1 ⟪ Red , v1 ⟫ tree t1) (s-left x s-nil) refl = ? + insertCase12 (node k1 ⟪ Black , v1 ⟫ tree t1) (s-left x s-nil) refl = ? -- exit rot repl rbir ? ? ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)