Mercurial > hg > Gears > GearsAgda
changeset 801:772a6bb0b614
merged
| author | Moririn |
|---|---|
| date | Mon, 20 Nov 2023 18:17:48 +0900 |
| parents | 418ab1fa2aca |
| children | 6f27c2c18035 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 12 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Mon Nov 20 10:31:44 2023 +0900 +++ b/hoareBinaryTree1.agda Mon Nov 20 18:17:48 2023 +0900 @@ -692,6 +692,16 @@ rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)} → k < key → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) +RBtreeCopy : {n m : Level} {A : Set n} {t : Set m} {key : ℕ} {value : A} {c : Color} → (tree tree0 : bt (Color ∧ A) ) + → (stack : List (bt (Color ∧ A)) ) + → ( treeInvariant tree ∧ stackInvariant key tree tree0 stack) + → ( next : (tree tree0 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) + → ( treeInvariant tree ∧ stackInvariant key tree tree0 stack ) + → replacedRBTree key value tree0 tree → t ) + → ( exit : (repl : bt (Color ∧ A)) → replacedRBTree key value tree0 repl → t ) → t +RBtreeCopy = {!!} + + data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand @@ -910,8 +920,8 @@ 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 = {!!} + ... | tri≈ ¬a b ¬c = next {!!} {!!} {!!} {!!} ... | tri> ¬a ¬b c = {!!} insertCase1 : t insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)