Mercurial > hg > Gears > GearsAgda
view redBlackTreeTest.agda @ 571:1eccf1f18a59
add more detail
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 27 Apr 2018 19:19:40 +0900 |
parents | a6aa2ff5fea4 |
children | eb75d9971451 |
line wrap: on
line source
module redBlackTreeTest where open import RedBlackTree open import stack open import Level hiding (zero) renaming ( suc to succ ) open import Data.Empty open import Data.Nat open import Relation.Nullary open import Algebra open import Data.Nat.Properties as NatProp open Tree open Node open RedBlackTree.RedBlackTree open Stack -- tests putTree1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → k → a → (RedBlackTree {n} {m} {t} a k → t) → t putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree) ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next)) open import Relation.Binary.PropositionalEquality open import Relation.Binary.Core open import Function check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} check1 Nothing _ = False check1 (Just n) x with Data.Nat.compare (value n) x ... | equal _ = True ... | _ = False check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} check2 Nothing _ = False check2 (Just n) x with compare2 (value n) x ... | EQ = True ... | _ = False test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True )) test1 = refl test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → putTree1 t 2 2 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True ))) test2 = refl open ≡-Reasoning test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 $ λ t → putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → putTree1 t 4 4 $ λ t → getRedBlackTree t 1 $ λ t x → check2 x 1 ≡ True test3 = begin check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1 ≡⟨ refl ⟩ True ∎ test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 $ λ t → putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → putTree1 t 4 4 $ λ t → getRedBlackTree t 4 $ λ t x → x -- test5 : Maybe (Node ℕ ℕ) test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 $ λ t → putTree1 t 6 6 $ λ t0 → clearSingleLinkedStack (nodeStack t0) $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 ) $ λ t1 s n1 → replaceNode t1 s n1 $ λ t → getRedBlackTree t 3 -- $ λ t x → SingleLinkedStack.top (stack s) -- $ λ t x → n1 $ λ t x → root t where findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t findNode1 t s n1 Nothing next = next t s n1 findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t → -- putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} ) -- test51 = refl test6 : Maybe (Node ℕ ℕ) test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) test7 : Maybe (Node ℕ ℕ) test7 = clearSingleLinkedStack (nodeStack tree2) (λ s → replaceNode tree2 s n2 (λ t → root t)) where tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} k1 = 1 n2 = leafNode 0 0 value1 = 1 test8 : Maybe (Node ℕ ℕ) test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 $ λ t → putTree1 t 2 2 (λ t → root t) test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True )) test9 = refl test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → putRedBlackTree t 2 2 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True ))) test10 = refl test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 $ λ t → putRedBlackTree t 2 2 $ λ t → putRedBlackTree t 3 3 $ λ t → getRedBlackTree t 2 $ λ t x → root t redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareT } compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y ) compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) where open import Relation.Binary checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} checkT Nothing _ = False checkT (Just n) x with compTri (value n) x ... | tri≈ _ _ _ = True ... | _ = False checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (Just n) x ≡ True checkEQ x n refl with compTri (value n) x ... | tri≈ _ refl _ = refl ... | tri> _ neq gt = ⊥-elim (neq refl) ... | tri< lt neq _ = ⊥-elim (neq refl) checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq checkEQ' x y refl with x ≟ y ... | yes refl = refl ... | no neq = ⊥-elim ( neq refl ) --- search -> checkEQ --- findNode -> search putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) → (k : ℕ) (x : ℕ) → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)) putTest1 n k x with n ... | Just n1 = lemma0 where tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT } lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))) lemma2 s with compTri k (key n1) ... | tri≈ le refl gt = lemma5 s where open stack.SingleLinkedStack open stack.Element lemma6 : (s : SingleLinkedStack (Node ℕ ℕ) ) → (n2 : Element (Node ℕ ℕ) ) → ReplaceNode.replaceNode1 (tree0 s) s (record n1 { key = k ; value = x } ) (λ t → GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t)) (record { top = Element.next n2 }) (Just (Element.datum n2)) lemma6 s n2 with (top s ) ... | Just n3 with compTri (key (datum n2)) (key (datum n3)) ... | tri< _ neq _ = {!!} -- lemma6 ( record {top = next n3} ) {!!} ... | tri> _ neq _ = {!!} -- lemma6 ( record {top = next n3} ) {!!} ... | tri≈ _ eq _ = {!!} lemma6 s n2 | Nothing = {!!} lemma5 : (s : SingleLinkedStack (Node ℕ ℕ) ) → popSingleLinkedStack ( record { top = Just (cons n1 (SingleLinkedStack.top s)) } ) ( \ s1 _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) ) lemma5 s with (top s) ... | Just n2 with compTri k k ... | tri< _ neq _ = ⊥-elim (neq refl) ... | tri> _ neq _ = ⊥-elim (neq refl) ... | tri≈ _ refl _ = lemma6 s n2 lemma5 s | Nothing with compTri k k ... | tri≈ _ refl _ = checkEQ x _ refl ... | tri< _ neq _ = ⊥-elim (neq refl) ... | tri> _ neq _ = ⊥-elim (neq refl) ... | tri> le eq gt = {!!} ... | tri< le eq gt = {!!} lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))) lemma0 = lemma2 (record {top = Nothing}) ... | Nothing = lemma1 where lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k ( λ t x1 → checkT x1 x ≡ True) lemma1 with compTri k k ... | tri≈ _ refl _ = checkEQ x _ refl ... | tri< _ neq _ = ⊥-elim (neq refl) ... | tri> _ neq _ = ⊥-elim (neq refl)