Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 769:ce0d41a84c2b

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 Sun, 07 May 2023 20:19:18 +0900
parents 1bb96bc9eb45
children a4bc901bba36
comparison
equal deleted inserted replaced
768:1bb96bc9eb45 769:ce0d41a84c2b
609 parent grand uncle : bt A 609 parent grand uncle : bt A
610 pg : ParentGrand self parent uncle grand 610 pg : ParentGrand self parent uncle grand
611 rest : List (bt A) 611 rest : List (bt A)
612 stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest ) 612 stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
613 613
614 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) (C : bt (Color ∧ A) → bt (Color ∧ A) → List (bt (Color ∧ A)) → Set n) : Set n where
615 field
616 d rd : ℕ
617 tree0 rot : bt (Color ∧ A)
618 tree0rb : RBtreeInvariant tree0 d
619 replrb : RBtreeInvariant repl rd
620 d=rd : ( d ≡ rd ) ∨ ( suc d ≡ rd )
621 rotated : rotatedTree tree rot
622 si : stackInvariant key tree tree0 stack
623 ri : replacedRBTree key value (child-replaced key rot ) repl
624 ci : C tree repl stack -- data continuation
625
614 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) 626 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
615 → (stack : List (bt A)) → stackInvariant key tree orig stack 627 → (stack : List (bt A)) → stackInvariant key tree orig stack
616 → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack 628 → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack
617 stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl 629 stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl
618 stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right x s-nil) = case2 (case1 refl) 630 stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right x s-nil) = case2 (case1 refl)