Mercurial > hg > Members > Moririn

comparison hoareBinaryTree1.agda @ 762:56de8e7dca7a

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 Fri, 05 May 2023 10:14:53 +0900
parents 927c02120a73
children 799325a71422
comparison
equal deleted inserted replaced
760:927c02120a73 762:56de8e7dca7a
637 stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A } 637 stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A }
638 → {stack : List (bt A)} → stackInvariant key tree orig stack 638 → {stack : List (bt A)} → stackInvariant key tree orig stack
639 → stack ≡ orig ∷ [] → tree ≡ orig 639 → stack ≡ orig ∷ [] → tree ≡ orig
640 stackCase1 s-nil refl = refl 640 stackCase1 s-nil refl = refl
641 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 = ?
647
648 PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) ) 642 PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) )
649 → RBtreeInvariant orig d0 643 → RBtreeInvariant orig d0
650 → (stack : List (bt (Color ∧ A))) → (pg : PG (Color ∧ A) tree stack ) 644 → (stack : List (bt (Color ∧ A))) → (pg : PG (Color ∧ A) tree stack )
651 → RBtreeInvariant tree ds ∧ RBtreeInvariant (PG.parent pg) dp ∧ RBtreeInvariant (PG.grand pg) dg 645 → RBtreeInvariant tree ds ∧ RBtreeInvariant (PG.parent pg) dp ∧ RBtreeInvariant (PG.grand pg) dg
652 PGtoRBinvariant = {!!} 646 PGtoRBinvariant = {!!}
801 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) 795 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
802 insertCase1 : t 796 insertCase1 : t
803 insertCase1 with stackToPG tree orig stack si 797 insertCase1 with stackToPG tree orig stack si
804 ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 798 ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri
805 ... | case2 (case1 eq ) = ? where 799 ... | case2 (case1 eq ) = ? where
806 insertCase12 : t 800 insertCase12 : (orig : bt (Color ∧ A))
807 insertCase12 = ? 801 → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key tree orig stack )
802 → stack ≡ tree ∷ orig ∷ [] → t
803 insertCase12 (node k1 ⟪ Red , v1 ⟫ t1 tree) (s-right x s-nil) refl = exit rot repl rbir ? ?
804 insertCase12 (node k1 ⟪ Black , v1 ⟫ t1 tree) (s-right x s-nil) refl = ?
805 insertCase12 (node k1 ⟪ Red , v1 ⟫ tree t1) (s-left x s-nil) refl = ?
806 insertCase12 (node k1 ⟪ Black , v1 ⟫ tree t1) (s-left x s-nil) refl = ?
808 -- exit rot repl rbir ? ? 807 -- exit rot repl rbir ? ?
809 ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 808 ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)
810 809
811 810