Mercurial > hg > Gears > GearsAgda
changeset 747:70ed4cbeaafb
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 25 Apr 2023 09:05:03 +0900 |
| parents | 4edec19e8356 |
| children | 1d7803a2c4c0 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 29 insertions(+), 49 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Tue Apr 25 08:16:02 2023 +0900 +++ b/hoareBinaryTree1.agda Tue Apr 25 09:05:03 2023 +0900 @@ -574,31 +574,12 @@ -- data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where -- rb-leaf : replacedRBTree key value leaf (node key ⟪ Black , value ⟫ leaf leaf) -data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where - rb-leaf : (key : ℕ) → RBTree A key Black 0 - rb-single : (key : ℕ) → (value : A) → (c : Color) → RBTree A key c 1 - t-right-red : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d - t-right-black : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ }→ RBTree A key₁ c d - → RBTree A key Black (suc d) - t-left-red : (key₁ : ℕ) { key : ℕ} → (value : A) → key < key₁ → {d : ℕ} → RBTree A key Black d - → RBTree A key₁ Red d - t-left-black : (key₁ : ℕ) {key : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ} → RBTree A key c d - → RBTree A key₁ Black (suc d) - t-node-red : (key₁ : ℕ) { key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {d : ℕ} - → RBTree A key Black d - → RBTree A key₂ Black d - → RBTree A key₁ Red d - t-node-black : (key₁ : ℕ) {key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {c c1 : Color} {d : ℕ} - → RBTree A key c d - → RBTree A key₂ c1 d - → RBTree A key₁ Black (suc d) +color : {n : Level} (A : Set n) → (rb : bt (Color ∧ A)) → Color +color {n} A rb = ? -color : {n : Level} (A : Set n) → (rb : bt (A ∧ Color)) → Color -color {n} A {k} {d} {c} rb = ? - -RB→bt : {n : Level} (A : Set n) → (rb : bt (A ∧ Color)) → bt A +RB→bt : {n : Level} (A : Set n) → (rb : bt (Color ∧ A)) → bt A RB→bt {n} A leaf = leaf -RB→bt {n} A (node key ⟪ c , value ⟫ x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) +RB→bt {n} A (node key ⟪ c , value ⟫ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } @@ -619,7 +600,7 @@ rr-right : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A} → ka < kb → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁ - → rotatedTree (node ka va (node kb vb d e) tc) (node kb vb d₁ (node ka va e₁ c₁) ) + → rotatedTree (node ka va (node kb vb d e) c) (node kb vb d₁ (node ka va e₁ c₁) ) -- b a -- d a b c -- e c d e @@ -671,12 +652,12 @@ → ParentGrand orig parent grand → ℕ rbsi-len {n} {A} {s} {p} {g} st = ? -findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (orig : RBTree A key1 c1 d1 ) - → (stack : List (bt A)) → stackInvariant key (RB→bt A tree) (RB→bt A orig) stack - → (next : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack → rbt-depth A tree1 < rbt-depth A tree → t ) - → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack - → (rbt-depth A tree1 ≡ 0 ) ∨ ( rbt-key A tree1 ≡ just key ) → t ) → t -findRBP {n} {m} {A} {t} key {key1} tree orig st si next exit = ? +-- findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (orig : RBTree A key1 c1 d1 ) +-- → (stack : List (bt A)) → stackInvariant key (RB→bt A tree) (RB→bt A orig) stack +-- → (next : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack → rbt-depth A tree1 < rbt-depth A tree → t ) +-- → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack +-- → (rbt-depth A tree1 ≡ 0 ) ∨ ( rbt-key A tree1 ≡ just key ) → t ) → t +--findRBP {n} {m} {A} {t} key {key1} tree orig st si next exit = ? rotateRight : ? rotateRight = ? @@ -686,14 +667,14 @@ insertCase5 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} - → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 ) + → (orig tree repl : bt (Color ∧ A) ) → (si : ParentGrand ? ? ?) → (ri : rotatedTree (RB→bt A tree) (RB→bt A repl)) - → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) + → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 repl1 : bt (Color ∧ A)) → (si1 : ParentGrand ? ? ?) → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1)) → rbsi-len si1 < rbsi-len si → t ) - → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) + → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 repl1 : bt (Color ∧ A)) → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1)) → t ) → t insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where @@ -702,25 +683,24 @@ replaceRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → {key0 key1 d0 d1 : ℕ} {c0 c1 : Color} - → (orig : RBTree A key0 c0 d0 ) → (tree : RBTree A key1 c1 d1 ) - → (stack : List (bt A)) → (si : stackInvariant key (RB→bt A tree) (RB→bt A orig) stack ) - → (next : {key2 d2 : ℕ} {c2 : Color} → (tree2 : RBTree A key2 c2 d2 ) - → {tr to : bt A} → RB→bt A tree2 ≡ tr → RB→bt A orig ≡ to - → (stack1 : List (bt A)) → stackInvariant key tr to stack1 + → (orig tree : bt (Color ∧ A)) + → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) + → (next : {key2 d2 : ℕ} {c2 : Color} + → (to tr : bt (Color ∧ A)) + → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 → length stack1 < length stack → t ) - → (exit : {k1 d1 : ℕ} {c1 : Color} → (repl1 : RBTree A k1 c1 d1 ) → (rot : bt A ) - → (ri : rotatedTree (RB→bt A orig) rot ) → replacedTree key value rot (RB→bt A repl1) → t ) → t -replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = insertCase1 stack _ _ refl refl si where - insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree : RBTree A k0 c0 d0) - → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) - → (stack : List (bt A)) → (tr to pt gt : bt A) → RB→bt A tree ≡ tr → RB→bt A parent ≡ pt → RB→bt A grand ≡ gt → RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) - → (pg : ParentGrand tr pt gt ) → t - insertCase2 tree parent grand stack tr to treq toeq si pg = ? - insertCase1 : (stack : List (bt A)) → (tr to : bt A) → RB→bt A tree ≡ tr → RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) → t - insertCase1 stack tr to eqt eqo si with stackToPG tr to stack si + → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) ) + → (ri : rotatedTree (RB→bt A orig) (RB→bt A rot) ) → replacedTree key value (RB→bt A rot) (RB→bt A repl) → t ) → t +replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = ? where + insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree parent grand : bt (Color ∧ A)) + → (stack : List (bt (Color ∧ A))) → (tr to : bt (Color ∧ A)) → (si : stackInvariant key tr to stack ) + → (pg : ParentGrand tree parent grand ) → t + insertCase2 tree parent grand stack tr to = ? + insertCase1 : (stack : List (bt (Color ∧ A))) → (to tr : bt (Color ∧ A)) → (si : stackInvariant key tr to stack ) → t + insertCase1 stack to tr si with stackToPG tr to stack si ... | case1 eq = ? ... | case2 (case1 eq ) = ? - ... | case2 (case2 pg) = insertCase2 ? ? ? ? ? ? ? ? ? ? ? ? ? (PG.pg pg) where + ... | case2 (case2 pg) = insertCase2 ? ? ? ? ? ? ? (PG.pg pg) where si00 : stackInvariant key ? ? ? si00 = ?