Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 760:927c02120a73

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 Thu, 04 May 2023 18:40:10 +0900
parents 8435718138d1
children 6ae130db4c5b 56de8e7dca7a
comparison
equal deleted inserted replaced
759:8435718138d1 760:927c02120a73
632 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-right x₂ si))) = case2 (case2 632 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-right x₂ si))) = case2 (case2
633 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } ) 633 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
634 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-left x₂ si))) = case2 (case2 634 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-left x₂ si))) = case2 (case2
635 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } ) 635 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
636 636
637 stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A }
638 → {stack : List (bt A)} → stackInvariant key tree orig stack
639 → stack ≡ orig ∷ [] → tree ≡ orig
640 stackCase1 s-nil refl = refl
641
642 stackCase2 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A }
643 → {stack : List (bt A)} → stackInvariant key tree orig stack
644 → stack ≡ tree ∷ orig ∷ [] → {k1 : ℕ} {v1 : A} → (orig ≡ node k1 v1 tree leaf) ∨ (orig ≡ node k1 v1 leaf tree )
645 stackCase2 (s-right x s-nil) refl = case2 ?
646 stackCase2 (s-left x si) refl = ?
637 647
638 PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) ) 648 PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) )
639 → RBtreeInvariant orig d0 649 → RBtreeInvariant orig d0
640 → (stack : List (bt (Color ∧ A))) → (pg : PG (Color ∧ A) tree stack ) 650 → (stack : List (bt (Color ∧ A))) → (pg : PG (Color ∧ A) tree stack )
641 → RBtreeInvariant tree ds ∧ RBtreeInvariant (PG.parent pg) dp ∧ RBtreeInvariant (PG.grand pg) dg 651 → RBtreeInvariant tree ds ∧ RBtreeInvariant (PG.parent pg) dp ∧ RBtreeInvariant (PG.grand pg) dg
751 → {d : ℕ} → RBtreeInvariant tr d → {dr : ℕ} → RBtreeInvariant rr dr 761 → {d : ℕ} → RBtreeInvariant tr d → {dr : ℕ} → RBtreeInvariant rr dr
752 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 762 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1
753 → rotatedTree tr rot 763 → rotatedTree tr rot
754 → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr 764 → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
755 → length stack1 < length stack → t ) 765 → length stack1 < length stack → t )
756 → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) ) 766 → (exit : (rot repl : bt (Color ∧ A) )
757 → {d : ℕ} → RBtreeInvariant repl d 767 → {d : ℕ} → RBtreeInvariant repl d
758 → (ri : rotatedTree to rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t 768 → (ri : rotatedTree to rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl → t ) → t
759 replaceRBP {n} {m} {A} {t} key value orig tree rot repl rbio rbit rbir stack si roti {c} ri next exit = ? where 769 replaceRBP {n} {m} {A} {t} key value orig tree rot repl rbio rbit rbir stack si roti {c} ri next exit = ? where
760 insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) 770 insertCase2 : (tree parent uncle grand : bt (Color ∧ A))
761 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 771 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack )
762 → (pg : ParentGrand tree parent uncle grand ) → t 772 → (pg : ParentGrand tree parent uncle grand ) → t
763 insertCase2 tree leaf uncle grand stack si (s2-s1p2 () x₁) 773 insertCase2 tree leaf uncle grand stack si (s2-s1p2 () x₁)
789 -- tree is right of parent, parent is right of grand 799 -- tree is right of parent, parent is right of grand
790 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree 800 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
791 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) 801 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
792 insertCase1 : t 802 insertCase1 : t
793 insertCase1 with stackToPG tree orig stack si 803 insertCase1 with stackToPG tree orig stack si
794 ... | case1 eq = exit rot repl rbir {!!} ? -- (subst₂ (λ j k → replacedTree key ⟪ {!!} , value ⟫ j k ) {!!} {!!} r-node ) 804 ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri
795 ... | case2 (case1 eq ) = {!!} 805 ... | case2 (case1 eq ) = ? where
806 insertCase12 : t
807 insertCase12 = ?
808 -- exit rot repl rbir ? ?
796 ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 809 ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)
797 810
798 811