Mercurial > hg > Gears > GearsAgda

comparison redBlackTreeTest.agda @ 570:a6aa2ff5fea4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate clearStack
author ryokka
date Thu, 26 Apr 2018 20:09:55 +0900
parents f24a73245f36
children 1eccf1f18a59
comparison
equal deleted inserted replaced
569:f24a73245f36 570:a6aa2ff5fea4
142 ... | tri≈ _ refl _ = refl 142 ... | tri≈ _ refl _ = refl
143 ... | tri> _ neq gt = ⊥-elim (neq refl) 143 ... | tri> _ neq gt = ⊥-elim (neq refl)
144 ... | tri< lt neq _ = ⊥-elim (neq refl) 144 ... | tri< lt neq _ = ⊥-elim (neq refl)
145 145
146 checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq 146 checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq
147 checkEQ' x y refl with x ≟ y 147 checkEQ' x y refl with x ≟ y
148 ... | yes refl = refl 148 ... | yes refl = refl
149 ... | no neq = ⊥-elim ( neq refl ) 149 ... | no neq = ⊥-elim ( neq refl )
150 150
151 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) 151 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
152 → (k : ℕ) (x : ℕ) 152 → (k : ℕ) (x : ℕ)
153 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x 153 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
154 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)) 154 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))
155 putTest1 n k x with n 155 putTest1 n k x with n
156 ... | Just n1 = lemma2 ( record { top = Nothing } ) 156 ... | Just n1 = lemma0
157 where 157 where
158 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → 158 tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
159 putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compareT }) k x (λ t → 159 tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
160 GetRedBlackTree.checkNode t k (λ t₁ x1 → checkT x1 x ≡ True) (root t)) 160 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
161 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))
161 lemma2 s with compTri k (key n1) 162 lemma2 s with compTri k (key n1)
162 ... | tri≈ le refl gt = lemma3 163 ... | tri≈ le refl gt = {!!} -- lemma3
163 where 164 where
164 lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 165 lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
165 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black 166 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black
166 } ) ; nodeStack = s ; compare = λ x₁ y → compareT x₁ y } ) k ( λ t x1 → checkT x1 x ≡ True) 167 } ) ; nodeStack = s ; compare = λ x₁ y → compareT x₁ y } ) k ( λ t x1 → checkT x1 x ≡ True)
167 lemma3 with compTri k k 168 lemma3 with compTri k k
168 ... | tri≈ _ refl _ = checkEQ x _ refl 169 ... | tri≈ _ refl _ = checkEQ x _ refl
169 ... | tri< _ neq _ = ⊥-elim (neq refl) 170 ... | tri< _ neq _ = ⊥-elim (neq refl)
170 ... | tri> _ neq _ = ⊥-elim (neq refl) 171 ... | tri> _ neq _ = ⊥-elim (neq refl)
171 ... | tri> le eq gt = {!!} 172 ... | tri> le eq gt = {!!}
172 ... | tri< le eq gt = {!!} 173 ... | tri< le eq gt = {!!}
173 ... | Nothing = lemma1 174 lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
175 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))))
176 lemma0 = lemma2 (record {top = Nothing})
177 ... | Nothing = lemma1
174 where 178 where
175 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 179 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
176 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red 180 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
177 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k 181 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k
178 ( λ t x1 → checkT x1 x ≡ True) 182 ( λ t x1 → checkT x1 x ≡ True)