Mercurial > hg > Members > Moririn

comparison hoareBinaryTree1.agda @ 723:43180a01bfbe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 10 Apr 2023 10:43:00 +0900
parents b088fa199d3d
children 35891ec243a0
comparison
equal deleted inserted replaced
722:b088fa199d3d 723:43180a01bfbe
548 548
549 data Color : Set where 549 data Color : Set where
550 Red : Color 550 Red : Color
551 Black : Color 551 Black : Color
552 552
553 data rbInvariant {n : Level} {A : Set n} : bt A → Color → ℕ → Set n where 553 data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where
554 rb-leaf : rbInvariant leaf Black 0 554 rb-leaf : (key : ℕ) → RBTree A key Black 0
555 rb-single : (key : ℕ) → (value : A) → (c : Color) → rbInvariant (node key value leaf leaf) c 1 555 rb-single : (key : ℕ) → (value : A) → (c : Color) → RBTree A key c 1
556 t-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → {d : ℕ } → rbInvariant (node key₁ value₁ t₁ t₂) Black d 556 t-right-red : {key key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d
557 → rbInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) Red d 557 t-right-black : {key key₁ : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ }→ RBTree A key₁ c d
558 t-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → {c : Color} → {d : ℕ }→ rbInvariant (node key₁ value₁ t₁ t₂) c d 558 → RBTree A key Black (suc d)
559 → rbInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) Black (suc d) 559 t-left-red : {key key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ} → RBTree A key Black d
560 t-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → {d : ℕ} → rbInvariant (node key value t₁ t₂) Black d 560 → RBTree A key₁ Red d
561 → rbInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) Red d 561 t-left-black : {key key₁ : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ} → RBTree A key c d
562 t-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → {c : Color} → {d : ℕ} → rbInvariant (node key value t₁ t₂) c d 562 → RBTree A key₁ Black (suc d)
563 → rbInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) Black (suc d) 563 t-node-red : {key key₁ key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {d : ℕ}
564 t-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} {d : ℕ} 564 → RBTree A key Black d
565 → rbInvariant (node key value t₁ t₂) Black d 565 → RBTree A key₂ Black d
566 → rbInvariant (node key₂ value₂ t₃ t₄) Black d 566 → RBTree A key₁ Red d
567 → rbInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) Red d 567 t-node-black : {key key₁ key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {c c1 : Color} {d : ℕ}
568 t-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} {c c1 : Color} {d : ℕ} 568 → RBTree A key c d
569 → rbInvariant (node key value t₁ t₂) c d 569 → RBTree A key₂ c1 d
570 → rbInvariant (node key₂ value₂ t₃ t₄) c1 d 570 → RBTree A key₁ Black (suc d)
571 → rbInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) Black (suc d) 571
572 572 data rbstackInvariant {n : Level} {A : Set n} {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) : (key₁ : ℕ ) → Set n where
573 s-single : rbstackInvariant orig key
574 s-right : {key₁ key₂ : ℕ} → {c1 : Color} {d1 : ℕ} → key₁ < key₂ → (top : RBTree A key₁ c1 d1)
575 → rbstackInvariant orig key₁ → rbstackInvariant orig key
576 s-left : {key₁ key₂ : ℕ} → {c1 : Color} {d1 : ℕ} → key₂ < key₁ → (top : RBTree A key₁ c1 d1)
577 → rbstackInvariant orig key₁ → rbstackInvariant orig key
578
579 RB→bt : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → bt A
580 RB→bt {n} A (rb-leaf _) = leaf
581 RB→bt {n} A (rb-single key value _) = node key value leaf leaf
582 RB→bt {n} A (t-right-red {key} value x rb) = node key value leaf (RB→bt A rb)
583 RB→bt {n} A (t-right-black {key} value x rb) = node key value leaf (RB→bt A rb)
584 RB→bt {n} A (t-left-red {_} {key} value x rb) = node key value (RB→bt A rb) leaf
585 RB→bt {n} A (t-left-black {_} {key} value x rb) = node key value (RB→bt A rb) leaf
586 RB→bt {n} A (t-node-red {_} {key} value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁)
587 RB→bt {n} A (t-node-black {_} {key} value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁)
588
589 rbt-depth : ?
590 rbt-depth = ?
591
592 rbt-key : ?
593 rbt-key = ?
594
595
596 findRBP : {n m : Level} {A : Set n} {t : Set m} → (key key1 d d1 : ℕ) → (c : Color) → (tree : RBTree A key c d ) (tree1 : RBTree A key1 ? d1 )
597 → rbstackInvariant tree key1
598 → (next : (key0 d0 : ℕ ) (tree1 : RBTree A key0 ? d0 ) → rbstackInvariant tree1 key0 → rbt-depth tree1 < rbt-depth tree → t )
599 → (exit : (key0 d0 : ℕ) (tree0 : RBTree A key0 ? d0 ) → rbstackInvariant tree1 key0
600 → (tree1 ≡ ? ) ∨ ( rbt-key tree1 ≡ just key ) → t ) → t
601 findRBP = ?
602
603
604