Mercurial > hg > Gears > GearsAgda
annotate redBlackTreeTest.agda @ 575:73fc32092b64
push local rbtree
| author | ryokka |
|---|---|
| date | Fri, 01 Nov 2019 17:42:51 +0900 |
| parents | 70b09cbefd45 |
| children | 7bacba816277 |
| rev | line source |
|---|---|
| 537 | 1 module redBlackTreeTest where |
| 2 | |
|
554
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
3 open import Level hiding (zero) renaming ( suc to succ ) |
| 537 | 4 |
| 553 | 5 open import Data.Empty |
| 575 | 6 open import Data.List |
| 7 open import Data.Maybe | |
| 8 open import Data.Bool | |
| 537 | 9 open import Data.Nat |
| 575 | 10 open import Data.Nat.Properties as NatProp |
| 11 | |
| 553 | 12 open import Relation.Nullary |
| 575 | 13 open import Relation.Binary |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
14 |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
15 open import Algebra |
| 575 | 16 |
| 17 open import RedBlackTree | |
| 18 open import stack | |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
19 |
| 537 | 20 open Tree |
| 21 open Node | |
| 22 open RedBlackTree.RedBlackTree | |
| 23 open Stack | |
| 24 | |
| 25 -- tests | |
| 26 | |
| 575 | 27 putTree1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → k → a → ((RedBlackTree {n} {m} {t} a k) → t) → t |
| 543 | 28 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree) |
| 575 | 29 ... | nothing = next (record tree {root = just (leafNode k1 value) }) |
| 30 ... | just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next)) | |
| 537 | 31 |
| 32 open import Relation.Binary.PropositionalEquality | |
| 33 open import Relation.Binary.Core | |
| 34 open import Function | |
| 35 | |
| 36 | |
| 575 | 37 -- check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool |
| 38 -- check1 nothing _ = false | |
| 39 -- check1 (just n) x with Data.Nat.compare (value n) x | |
| 40 -- ... | equal _ = true | |
| 41 -- ... | _ = false | |
| 537 | 42 |
| 575 | 43 check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool |
| 44 check2 nothing _ = false | |
| 45 check2 (just n) x with compare2 (value n) x | |
| 46 ... | EQ = true | |
| 47 ... | _ = false | |
| 549 | 48 |
| 575 | 49 test1 : {m : Level} {A B C : Set} → putTree1 {Level.zero} {succ Level.zero} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ {!!} {!!} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true )) |
| 50 test1 = {!!} | |
| 537 | 51 |
| 575 | 52 -- test2 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( |
| 53 -- λ t → putTree1 t 2 2 ( | |
| 54 -- λ t → getRedBlackTree t 1 ( | |
| 55 -- λ t x → check2 {m} x 1 ≡ true ))) | |
| 56 -- test2 = refl | |
| 537 | 57 |
| 575 | 58 -- open ≡-Reasoning |
| 59 -- test3 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 | |
| 60 -- $ λ t → putTree1 t 2 2 | |
| 61 -- $ λ t → putTree1 t 3 3 | |
| 62 -- $ λ t → putTree1 t 4 4 | |
| 63 -- $ λ t → getRedBlackTree t 1 | |
| 64 -- $ λ t x → check2 {m} x 1 ≡ true | |
| 65 -- test3 {m} = begin | |
| 66 -- check2 {m} (just (record {key = 1 ; value = 1 ; color = Black ; left = nothing ; right = just (leafNode 2 2)})) 1 | |
| 67 -- ≡⟨ refl ⟩ | |
| 68 -- true | |
| 69 -- ∎ | |
| 542 | 70 |
| 575 | 71 -- test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 |
| 72 -- $ λ t → putTree1 t 2 2 | |
| 73 -- $ λ t → putTree1 t 3 3 | |
| 74 -- $ λ t → putTree1 t 4 4 | |
| 75 -- $ λ t → getRedBlackTree t 4 | |
| 76 -- $ λ t x → x | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
77 |
| 575 | 78 -- -- test5 : Maybe (Node ℕ ℕ) |
| 79 -- test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 | |
| 80 -- $ λ t → putTree1 t 6 6 | |
| 81 -- $ λ t0 → clearSingleLinkedStack (nodeStack t0) | |
| 82 -- $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 ) | |
| 83 -- $ λ t1 s n1 → replaceNode t1 s n1 | |
| 84 -- $ λ t → getRedBlackTree t 3 | |
| 85 -- -- $ λ t x → SingleLinkedStack.top (stack s) | |
| 86 -- -- $ λ t x → n1 | |
| 87 -- $ λ t x → root t | |
| 88 -- where | |
| 89 -- findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t | |
| 90 -- findNode1 t s n1 nothing next = next t s n1 | |
| 91 -- findNode1 t s n1 ( just n2 ) next = findNode t s n1 n2 next | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
92 |
| 575 | 93 -- -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t → |
| 94 -- -- putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ just (record { key = 1; value = 1; left = just (record { key = 2 ; value = 2 } ); right = nothing} ) | |
| 95 -- -- test51 = refl | |
| 539 | 96 |
| 575 | 97 -- test6 : Maybe (Node ℕ ℕ) |
| 98 -- test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) | |
| 539 | 99 |
| 100 | |
| 575 | 101 -- test7 : Maybe (Node ℕ ℕ) |
| 102 -- test7 = clearSingleLinkedStack (nodeStack tree2) (λ s → replaceNode tree2 s n2 (λ t → root t)) | |
| 103 -- where | |
| 104 -- tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} | |
| 105 -- k1 = 1 | |
| 106 -- n2 = leafNode 0 0 | |
| 107 -- value1 = 1 | |
| 539 | 108 |
| 575 | 109 -- test8 : Maybe (Node ℕ ℕ) |
| 110 -- test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 | |
| 111 -- $ λ t → putTree1 t 2 2 (λ t → root t) | |
| 544 | 112 |
| 113 | |
| 575 | 114 -- test9 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true )) |
| 115 -- test9 = refl | |
| 544 | 116 |
| 575 | 117 -- test10 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( |
| 118 -- λ t → putRedBlackTree t 2 2 ( | |
| 119 -- λ t → getRedBlackTree t 1 ( | |
| 120 -- λ t x → check2 {m} x 1 ≡ true ))) | |
| 121 -- test10 = refl | |
| 545 | 122 |
| 575 | 123 -- test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 |
| 124 -- $ λ t → putRedBlackTree t 2 2 | |
| 125 -- $ λ t → putRedBlackTree t 3 3 | |
| 126 -- $ λ t → getRedBlackTree t 2 | |
| 127 -- $ λ t x → root t | |
| 545 | 128 |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
129 |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
130 compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y ) |
| 575 | 131 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder) |
| 565 | 132 where open import Relation.Binary |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
133 |
| 575 | 134 checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool |
| 135 checkT nothing _ = false | |
| 136 checkT (just n) x with compTri (value n) x | |
| 137 ... | tri≈ _ _ _ = true | |
| 138 ... | _ = false | |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
139 |
| 575 | 140 checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (just n) x ≡ true |
| 565 | 141 checkEQ x n refl with compTri (value n) x |
| 566 | 142 ... | tri≈ _ refl _ = refl |
| 143 ... | tri> _ neq gt = ⊥-elim (neq refl) | |
| 144 ... | tri< lt neq _ = ⊥-elim (neq refl) | |
| 565 | 145 |
| 575 | 146 -- checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq |
| 147 -- checkEQ' x y refl with x ≟ y | |
| 148 -- ... | yes refl = refl | |
| 149 -- ... | no neq = ⊥-elim ( neq refl ) | |
| 546 | 150 |
| 571 | 151 --- search -> checkEQ |
| 152 --- findNode -> search | |
| 153 | |
| 575 | 154 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} {A B C : Set Level.zero } → RedBlackTree {Level.zero} {m} {t} {A} {B} {C} a ℕ |
| 155 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; nodeComp = λ x x₁ → {!!} } -- record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compTri } | |
| 156 | |
| 157 | |
| 573 | 158 open stack.SingleLinkedStack |
| 159 open stack.Element | |
| 160 | |
| 161 {-# TERMINATING #-} | |
| 575 | 162 inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool |
| 163 inStack {l} n s with ( top s ) | |
| 164 ... | nothing = true | |
| 165 ... | just n1 with compTri (key n) (key (datum n1)) | |
| 166 ... | tri> _ neq _ = inStack {l} n ( record { top = next n1 } ) | |
| 167 ... | tri< _ neq _ = inStack {l} n ( record { top = next n1 } ) | |
| 168 ... | tri≈ _ refl _ = false | |
| 573 | 169 |
| 170 record StackTreeInvariant ( n : Node ℕ ℕ ) | |
| 575 | 171 ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where |
| 573 | 172 field |
| 575 | 173 sti : {m : Level} → replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT {m} x1 (value n) ≡ true) |
| 174 notInStack : {m : Level} → inStack {m} n s ≡ true → ⊥ | |
| 573 | 175 |
| 176 open StackTreeInvariant | |
| 177 | |
| 575 | 178 |
| 179 -- testn : {!!} | |
| 180 -- testn = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 | |
| 181 -- $ λ t → putTree1 t 1 1 | |
| 182 -- $ λ t → putTree1 t 3 3 (λ ta → record {root = root ta ; nodeStack = nodeStack ta }) | |
| 183 | |
| 184 | |
| 185 -- List と Node で書こうとしたがなんだかんだListに直したほうが楽そうだった | |
| 186 | |
| 187 nullNode = (record {key = 0 ; value = 0 ; right = nothing ; left = nothing ; color = Red}) | |
| 188 | |
| 189 -- treeTotal : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → (List ℕ → t) → t | |
| 190 -- treeTotal {m} {t} s tr next with (left tr) | (right tr) | |
| 191 -- treeTotal {m} {t} s tr next | nothing | nothing = next ((key tr) ∷ []) | |
| 192 -- treeTotal {m} {t} s tr next | nothing | just x = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li)) | |
| 193 -- treeTotal {m} {t} s tr next | just x | nothing = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li)) | |
| 194 -- treeTotal {m} {t} s tr next | just x | just x₁ = treeTotal {m} {t} s x (λ li1 → treeTotal {m} {t} s x₁ (λ li2 → next (s ++ li1 ++ li2))) | |
| 195 treeTotal : { n m : Level } {a : Set n} {t : Set m} → ( s : List a ) → ( tr : (Node a a) ) → List a | |
| 196 treeTotal {n} {m} {a} {t} s tr with (left tr) | (right tr) | |
| 197 treeTotal {n} {m} {a} {t} s tr | nothing | nothing = (key tr) ∷ [] | |
| 198 treeTotal {n} {m} {a} {t} s tr | nothing | just x = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x) | |
| 199 treeTotal {n} {m} {a} {t} s tr | just x | nothing = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x) | |
| 200 treeTotal {n} {m} {a} {t} s tr | just x | just x₁ = s ++ ((key tr) ∷ (treeTotal {n} {m} {a} {t} s x) ++ (treeTotal {n} {m} {a} {t} s x₁)) | |
| 201 | |
| 202 | |
| 203 -- treeTotalA : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → List ℕ | |
| 204 | |
| 205 -- (treeTotal {_} {ℕ} ([]) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} testn 5 5 {!!})))) | |
| 206 | |
| 207 -- exput : (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ ℕ))) (λ total → {!!})) ≡ {!!} | |
| 208 -- exput = {!!} | |
| 209 | |
| 210 | |
| 211 -- aaa = (treeTotal {_} {_} {ℕ} {_} (5 ∷ []) ((record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black }))) | |
| 212 | |
| 213 | |
| 214 -- fuga = putTree1 {_} {_} {ℕ} {ℕ} (record {root = just (record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black }) ; nodeStack = ( record {top = nothing}) ; compare = (λ x x₁ → EQ) }) 5 5 (λ aaa → aaa ) | |
| 215 | |
| 216 -- nontree ++ 2 :: [] | |
| 217 | |
| 218 -- piyo = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 ( λ t1 → findNode t1 (record {top = nothing}) (leafNode 2 2) (Data.Maybe.fromMaybe nullNode (root t1)) (λ tree stack node → {!!})) | |
| 219 | |
| 220 | |
| 221 -- exn2l : {!!} ≡ (treeTotal {_} {ℕ} ([]) (putTree1 {_} {_} {ℕ} {ℕ} {!!} 5 5 (λ t → {!!}))) -- (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root testn))) | |
| 222 -- exn2l = refl | |
| 223 | |
| 224 | |
| 225 | |
| 226 | |
| 227 | |
| 228 -- record FS {n m : Level } {a : Set n} {t : Set m} (oldTotal : List a) ( s : List a ) ( tr : (Node a a) ) : Set where | |
| 229 -- field | |
| 230 -- total : treeTotal {n} {m} {a} {t} s tr ≡ oldTotal | |
| 231 -- -- usage = FS.total -- relation | |
| 232 | |
| 233 -- data P { n m : Level } { t : Set m } : Set where | |
| 234 -- P₀ : (old : List ℕ) ( s : List ℕ ) → (tr : (Node ℕ ℕ) ) → FS {m} {t} old s tr → P | |
| 235 | |
| 236 | |
| 237 | |
| 238 -- ttt = putTree1 {_} {_} {ℕ} {ℕ} | |
| 239 | |
| 240 -- record TreeInterface {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set n where | |
| 241 -- field | |
| 242 -- tree : treeImpl | |
| 243 -- list : List ℕ | |
| 244 -- node : Node ℕ ℕ | |
| 245 -- putTreeHoare : (FS {_} {ℕ} list list node) → putTree1 {!!} {!!} {!!} {!!} | |
| 246 | |
| 247 stack2list : {n m : Level} {t : Set m} {a : Set n} → (s : SingleLinkedStack a) → List a | |
| 248 stack2list stack with top stack | |
| 249 stack2list stack | just x = (datum x) ∷ (elm2list {_} {_} {ℕ} x) | |
| 250 where | |
| 251 elm2list : {n m : Level} {t : Set m} {a : Set n} → (elm : (Element a)) → List a | |
| 252 elm2list el with next el | |
| 253 elm2list el | just x = (datum el) ∷ (elm2list {_} {_} {ℕ} x) | |
| 254 elm2list el | nothing = (datum el) ∷ [] | |
| 255 stack2list stack | nothing = [] | |
| 256 | |
| 257 | |
| 258 -- list2element : {n m : Level} {t : Set m} {a : Set n} → (l : List a) → Maybe (Element a) | |
| 259 -- list2element [] = nothing | |
| 260 -- list2element (x ∷ l) = just (cons x (list2element {_} {_} {ℕ} l)) | |
| 261 | |
| 262 -- ltest = list2element (1 ∷ 2 ∷ 3 ∷ []) | |
| 263 | |
| 264 list2stack : {n m : Level} {t : Set m} {a : Set n} {st : SingleLinkedStack a} → (l : List a) → SingleLinkedStack a | |
| 265 list2stack {n} {m} {t} {a} {s} (x ∷ l) = pushSingleLinkedStack s x (λ s1 → list2stack {n} {m} {t} {a} {s1} l ) | |
| 266 list2stack {n} {m} {t} {a} {s} [] = s | |
| 267 | |
| 268 | |
| 269 | |
| 270 -- stest = list2stack (1 ∷ 2 ∷ 3 ∷ []) | |
| 271 | |
| 272 open Node | |
| 273 | |
| 274 exfind : { m : Level } { t : Set m} → (dt : ℕ) → (node : (Node ℕ ℕ)) → (st : List ℕ) → findNode {_} {_} {ℕ} {ℕ} (redBlackInSomeState ℕ (just node)) (emptySingleLinkedStack) (leafNode dt dt) (node) (λ t1 st1 n1 → (( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) ≡ ( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) )) | |
| 275 exfind dt node st with left node | right node | |
| 276 exfind dt node st | just x | just x₁ = {!!} | |
| 277 exfind dt node st | just x | nothing = {!!} | |
| 278 exfind dt node st | nothing | just x = {!!} | |
| 279 exfind dt node st | nothing | nothing with (compTri dt (key node)) | |
| 280 exfind dt node st | nothing | nothing | tri< a ¬b ¬c = {!!} | |
| 281 exfind dt node st | nothing | nothing | tri≈ ¬a b ¬c = {!!} | |
| 282 exfind dt node st | nothing | nothing | tri> ¬a ¬b c = {!!} | |
| 283 | |
| 284 -- exput : (ni : ℕ) → (tn : Node ℕ ℕ) → (ts : List ℕ) → (treeTotal {_} {ℕ} (ni ∷ ts) tn) | |
| 285 -- ≡ (treeTotal {_} {ℕ} (ts) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} (record { root = just tn } ) ni ni (λ tt → tt))))) | |
| 286 -- exput datum node [] with (right node) | (left node) | |
| 287 -- exput datum node [] | nothing | nothing = {!!} | |
| 288 -- exput datum node [] | just x | just x₁ = {!!} | |
| 289 -- exput datum node [] | just x | nothing = {!!} | |
| 290 -- exput datum node [] | nothing | just x = {!!} | |
| 291 -- exput datum node (x ∷ stack₁) = {!!} | |
| 292 | |
| 293 | |
| 294 -- proofTree : {n m : Level} {t : Set m} {a : Set n} (old stackl : List ℕ) → (node : Node ℕ ℕ) → (FS {_} {ℕ} old stackl node) → (tree : RedBlackTree ℕ ℕ) → (key : ℕ) → findNode {{!!}} {{!!}} {{!!}} {{!!}} tree (list2stack {!!} (record {top = nothing})) (leafNode key key) node (λ tree1 stack1 datum → {!!}) | |
| 295 -- -- -- -- putTree1 tree key key (λ t → (FS {_} {ℕ} old stackl (Data.Maybe.fromMaybe nullNode (root tree))) ) | |
| 296 -- proofTree old stack node fs t k = {!!} | |
| 297 | |
| 298 -- FS は 証明そのものになると思ってたけど実は違いそう | |
| 299 -- oldTotal と 現在の node, stack の組み合わせを比較する | |
| 300 -- oldTotal はどうやって作る? >< | |
| 301 -- treeTotal は list と node を受け取って それの total を出すのでそれで作る(list に put するデータなどを入れることで適当に作れる) | |
| 302 | |
| 303 -- p : {n m : Level} {t : Set m} {a : Set n} → ( s : SingleLinkedStack ℕ ) ( tr : (Node ℕ ℕ) ) ( tree : RedBlackTree ℕ ℕ ) (k : ℕ) → (FS (treeTotal (k ∷ (stack2list s)) tr) (stack2list s) tr) → putTree1 tree k k (λ atree → FS (treeTotal (stack2list s) (Data.Maybe.fromMaybe (tr) (root atree))) {!!} {!!}) | |
| 304 -- p stack node tree key = {!!} | |
| 305 | |
| 306 -- tt = (FS {_} {ℕ} [] [] (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ {_} ℕ {ℕ})))) | |
| 307 | |
| 308 -- ttt : (a : P) → P | |
| 309 -- ttt a = P₀ {!!} {!!} (record { key = {!!} ; value = {!!} ; right = {!!} ; left = {!!} ; color = {!!} }) (record { total = {!!} }) | |
| 310 | |
| 311 | |
| 312 -- FS では stack tree をあわせた整合性を示したい | |
| 313 -- そのためには...? | |
| 314 -- stack は前の node (というか一段上)が入ってる | |
| 315 -- tree は現在の node がある | |
| 316 | |
| 317 | |
| 318 -- tr(Node ℕ ℕ) s (List (Node)) | |
| 319 -- 3 [] | |
| 320 -- / \ | |
| 321 -- 2 5 | |
| 322 -- / / \ | |
| 323 -- 1 4 6 | |
| 324 | |
| 325 -- search 6 (6 > 3) | |
| 326 -- tr(Node ℕ ℕ) s (List (Node)) | |
| 327 -- 5 just (node (1 2 nothing) 3 (4 5 6) | |
| 328 -- / \ [] | |
| 329 -- 4 6 | |
| 330 | |
| 331 -- search 6 (6 > 5) | |
| 332 -- tr(Node ℕ ℕ) s (List (Node)) | |
| 333 -- 6 just (node (4 5 6)) | |
| 334 -- just (node (1 2 nothing) 3 (4 5 6) | |
| 335 -- [] | |
| 336 | |
| 337 -- just 6 → true みたいな感じ | |
| 338 | |
| 339 -- stack に node ごと入れるのは間違い…？ | |
| 340 -- 一応非破壊な感じがする(新しく作り直してる) | |
| 341 -- どう釣り合いをとるか | |
| 342 | |
| 343 -- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t | |
| 344 -- stack+tree {n} stack mid org = st stack mid org where | |
| 345 -- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ) | |
| 346 -- st [] _ _ = nothing | |
| 347 -- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org) | |
| 348 -- st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org | |
| 349 -- st (x ∷ []) n n1 | _ | _ = nothing | |
| 350 -- st (x ∷ a) n n1 with st a n n1 | |
| 351 -- st (x ∷ a) n n1 | just x₁ = {!!} | |
| 352 -- st (x ∷ a) n n1 | nothing = nothing | |
| 353 | |
| 354 | |
| 355 -- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t | |
| 356 -- stack+tree {n} stack mid org cg = st stack mid org | |
| 357 -- where | |
| 358 -- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ) | |
| 359 -- st [] _ _ = nothing | |
| 360 -- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org) | |
| 361 -- st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org | |
| 362 -- st (x ∷ []) n n1 | _ | _ = nothing | |
| 363 -- st (x ∷ a) n n1 with st a n n1 | |
| 364 -- st (x ∷ a) n n1 | just x₁ = {!!} | |
| 365 -- st (x ∷ a) n n1 | nothing = nothing | |
| 366 | |
| 367 -- findNodePush : {n : Level} → (stack : List (Node ℕ ℕ)) → (mid : Node ℕ ℕ) → (org : Node ℕ ℕ) → stack+tree stack mid org ≡ just ? | |
| 368 -- → ? {return (? ∷ stack),mid'} → stack+tree (? ∷ stack) (mid') org ≡ just ? | |
| 369 -- findNodePush | |
| 370 | |
| 371 -- stack+tree が just だって言えたらよい | |
| 372 -- {}2 は orig の どっちかのNode | |
| 373 |