Mercurial > hg > Members > Moririn

comparison hoareBinaryTree1.agda @ 751:4ecad6cfef4b

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 Wed, 26 Apr 2023 09:20:38 +0900
parents 61e16b7489b8
children 44837beece64
comparison
equal deleted inserted replaced
750:61e16b7489b8 751:4ecad6cfef4b
639 → (next : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) 639 → (next : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t )
640 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack 640 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack
641 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t 641 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
642 findRBT = ? 642 findRBT = ?
643 643
644 rotateRight : ?
645 rotateRight = ?
646
647 rotateLeft : ?
648 rotateLeft = ?
649
650 insertCase5 : {n m : Level} {A : Set n} {t : Set m} 644 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
651 → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} 645 → (key : ℕ) → (value : A) → {d0 : ℕ}
652 → (orig tree repl : bt (Color ∧ A) ) 646 → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
653 → (si : ParentGrand ? ? ?) 647 → RBtreeInvariant orig d0
654 → (ri : rotatedTree (RB→bt A tree) (RB→bt A repl)) 648 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant repl dr
655 → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 repl1 : bt (Color ∧ A)) 649 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack )
656 → (si1 : ParentGrand ? ? ?) 650 → rotatedTree tree rot
657 → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1)) 651 → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
658 → length ? < length ? → t ) 652 → (next : {key2 d2 : ℕ} {c2 : Color} -- rotating case
659 → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 repl1 : bt (Color ∧ A)) 653 → (to tr rot rr : bt (Color ∧ A))
660 → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1)) 654 → RBtreeInvariant orig d0
661 → t ) → t 655 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant rr dr
656 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1
657 → rotatedTree tr rot
658 → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
659 → length stack1 < length stack → t )
660 → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
661 → {d : ℕ} → RBtreeInvariant repl d
662 → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
662 insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where 663 insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where
663 insertCase51 : (key1 : ℕ) (si : ParentGrand ? ? ? ) → t 664 insertCase51 : (key1 : ℕ) (si : ParentGrand ? ? ? ) → t
664 insertCase51 = ? 665 insertCase51 = ?
666 rotateRight : ?
667 rotateRight = ?
668 rotateLeft : ?
669 rotateLeft = ?
670
665 671
666 -- if we have replacedNode on RBTree, we have RBtreeInvariant 672 -- if we have replacedNode on RBTree, we have RBtreeInvariant
667 673
668 replaceRBP : {n m : Level} {A : Set n} {t : Set m} 674 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
669 → (key : ℕ) → (value : A) → {d0 : ℕ} 675 → (key : ℕ) → (value : A) → {d0 : ℕ}
670 → (orig tree repl : bt (Color ∧ A)) {d0 : ℕ} 676 → (orig tree repl : bt (Color ∧ A)) {d0 : ℕ}
671 → RBtreeInvariant orig d0 677 → RBtreeInvariant orig d0
672 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant repl dr 678 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant repl dr
673 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 679 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack )
674 → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tree) repl 680 → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tree) repl
675 → (next : {key2 d2 : ℕ} {c2 : Color} 681 → (next : {key2 d2 : ℕ} {c2 : Color} -- no rotating case
676 → (to tr rr : bt (Color ∧ A)) 682 → (to tr rr : bt (Color ∧ A))
677 → RBtreeInvariant orig d0 683 → RBtreeInvariant orig d0
678 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant rr dr 684 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant rr dr
679 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 685 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1
680 → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tr) rr 686 → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tr) rr
686 insertCase2 : (tree parent grand : bt (Color ∧ A)) 692 insertCase2 : (tree parent grand : bt (Color ∧ A))
687 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 693 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack )
688 → (pg : ParentGrand tree parent grand ) → t 694 → (pg : ParentGrand tree parent grand ) → t
689 insertCase2 tree parent grand stack si pg with color A parent 695 insertCase2 tree parent grand stack si pg with color A parent
690 ... | Black = ? -- tree stuctre is preserved 696 ... | Black = ? -- tree stuctre is preserved
691 ... | Red = insertCase3 grand refl where 697 ... | Red = ? where -- insertCase3 grand refl where
692 -- 698 --
693 -- in some case, stack is poped and loop to replaceRBP 699 -- in some case, stack is poped and loop to replaceRBP
694 -- it means, we have to create replacedTree 700 -- it means, we have to create replacedTree
695 insertCase3 : ( tp tg : bt (Color ∧ A) ) → tp ≡ parent → tg ≡ grand → t 701 insertCase3 : ( tp tg : bt (Color ∧ A) ) → tp ≡ parent → tg ≡ grand → t
696 insertCase3 tp leaf eq = ? 702 insertCase3 tp leaf eq = ?