Mercurial > hg > Gears > GearsAgda
changeset 756:08f752ecf32e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 May 2023 09:05:24 +0900 |
| parents | 3ce248076116 |
| children | edfeedb45595 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 21 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sun Apr 30 21:12:45 2023 +0900 +++ b/hoareBinaryTree1.agda Mon May 01 09:05:24 2023 +0900 @@ -649,7 +649,7 @@ → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) → rotatedTree tree rot → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl - → (next : {key2 d2 : ℕ} {c2 : Color} -- rotating case + → (next : {key2 d2 : ℕ} {c2 : Color} → (to tr rot rr : bt (Color ∧ A)) → RBtreeInvariant orig d0 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant rr dr @@ -660,9 +660,12 @@ → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) ) → {d : ℕ} → RBtreeInvariant repl d → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t -rotateLeft {n} {m} {A} {t} key value orig .orig rot repl rbo rbt rbr .(orig ∷ []) s-nil ri rr next exit = ? -rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr .(tree ∷ _) (s-right x si) ri rr next exit = ? -rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr .(tree ∷ _) (s-left x si) ri rr next exit = ? +rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateLeft1 where + rotateLeft1 : t + rotateLeft1 with stackToPG tree orig stack si + ... | case1 x = ? + ... | case2 (case1 x) = ? + ... | case2 (case2 pg) = ? rotateRight : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → {d0 : ℕ} @@ -672,7 +675,7 @@ → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) → rotatedTree tree rot → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl - → (next : {key2 d2 : ℕ} {c2 : Color} -- rotating case + → (next : {key2 d2 : ℕ} {c2 : Color} → (to tr rot rr : bt (Color ∧ A)) → RBtreeInvariant orig d0 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant rr dr @@ -683,9 +686,12 @@ → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) ) → {d : ℕ} → RBtreeInvariant repl d → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t -rotateRight {n} {m} {A} {t} key value orig .orig rot repl rbo rbt rbr .(orig ∷ []) s-nil ri rr next exit = ? -rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr .(tree ∷ _) (s-right x si) ri rr next exit = ? -rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr .(tree ∷ _) (s-left x si) ri rr next exit = ? +rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateRight1 where + rotateRight1 : t + rotateRight1 with stackToPG tree orig stack si + ... | case1 x = ? + ... | case2 (case1 x) = ? + ... | case2 (case2 pg) = ? insertCase5 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → {d0 : ℕ} @@ -695,7 +701,7 @@ → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) → rotatedTree tree rot → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl - → (next : {key2 d2 : ℕ} {c2 : Color} -- rotating case + → (next : {key2 d2 : ℕ} {c2 : Color} → (to tr rot rr : bt (Color ∧ A)) → RBtreeInvariant orig d0 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant rr dr @@ -753,24 +759,24 @@ insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) leaf grand stack si pg = ? insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = next ? ? ? ? ? ? ? ? ? ? ? ? insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = - insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit + insertCase5 key value orig tree ? repl rbio ? ? stack si ? ri ? ? next exit -- tree is left of parent, parent is left of grand -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1 -- grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁) insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1sp2 x x₁) = - rotateLeft ? ? ? ? ? ? ? ? ? ? ? ? ? (λ a b c d e f h i j k l m → insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit ) - exit + rotateLeft key value orig tree ? repl rbio ? ? stack si ? ri ? ? + (λ a b c d e f h i j k l m → insertCase5 key value a b c d ? ? h i j k l ? ? next exit ) exit -- tree is right of parent, parent is left of grand rotateLeft -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree -- grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁) insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s12p x x₁) = - rotateRight ? ? ? ? ? ? ? ? ? ? ? ? ? (λ a b c d e f h i j k l m → insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit ) - exit + rotateRight key value orig tree ? repl rbio ? ? stack si ? ri ? ? + (λ a b c d e f h i j k l m → insertCase5 key value a b c d ? ? h i j k l ? ? next exit ) exit -- tree is left of parent, parent is right of grand, rotateRight -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1s2p x x₁) = - insertCase5 ? ? ? ? ? ? ? ? ? ? ? ? ? next exit + insertCase5 key value orig tree ? repl rbio ? ? stack si ? ri ? ? next exit -- tree is right of parent, parent is right of grand -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)