Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 619:a3fbc9b57015

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 Nov 2021 19:43:16 +0900
parents 5702800c79bc
children fe8c2d82c05c
comparison
equal deleted inserted replaced
618:5702800c79bc 619:a3fbc9b57015
177 top-value (node key value tree tree₁) = just value 177 top-value (node key value tree tree₁) = just value
178 178
179 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ 179 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
180 insertTreeSpec0 _ _ _ = tt 180 insertTreeSpec0 _ _ _ = tt
181 181
182 record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) (C : Set n) : Set n where 182 record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
183 field 183 field
184 tree0 : bt A
184 ti : treeInvariant tree 185 ti : treeInvariant tree
185 si : stackInvariant tree stack 186 si : stackInvariant tree0 stack
186 opt : C
187 opt1 : C → C
188 187
189 findPP : {n m : Level} {A : Set n} {t : Set m} 188 findPP : {n m : Level} {A : Set n} {t : Set m}
190 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) 189 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
191 → {Cond : bt A → List (bt A) → Set n} 190 → (Pre : bt A → List (bt A) → findPR tree stack )
192 → (Pre : bt A → List (bt A) → findPR tree stack (Cond tree stack) ) 191 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 → bt-depth tree1 < bt-depth tree → t )
193 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (Cond tree1 stack1) → bt-depth tree1 < bt-depth tree → t ) 192 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 → t) → t
194 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (Cond tree1 stack1) → t) → t
195 findPP key leaf st Pre next exit = exit leaf st (Pre leaf st ) 193 findPP key leaf st Pre next exit = exit leaf st (Pre leaf st )
196 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁ 194 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
197 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st (P n st) 195 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st (P n st)
198 findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c = next tree (n ∷ st) (record {ti = {!!} ; si = {!!} ; opt = {!!} ; opt1 = id } ) findPP1 where -- Cond n st → Cond tree (n ∷ st) 196 findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c =
199 findPP0 : {!!} 197 next tree (n ∷ st) (record {ti = findPP0 tree tree₁ (findPR.ti (Pre n st)) ; si = findPP2 st (findPR.si (Pre n st))} ) findPP1 where
200 findPP0 = {!!} 198 tree0 = findPR.tree0 (Pre n st)
199 findPP0 : (tree tree₁ : bt A) → treeInvariant ( node key₁ v tree tree₁ ) → treeInvariant tree
200 findPP0 leaf t x = tt
201 findPP0 (node key value tree tree₁) leaf x = proj1 x
202 findPP0 (node key value tree tree₁) (node key₁ value₁ t t₁) x = proj1 x
203 findPP2 : (st : List (bt A)) → stackInvariant tree0 st → stackInvariant tree0 (node key₁ v tree tree₁ ∷ st)
204 findPP2 [] (lift tt) = {!!}
205 findPP2 (leaf ∷ st) x = {!!}
206 findPP2 (node key value leaf leaf ∷ st) x = {!!}
207 findPP2 (node key value leaf (node key₁ value₁ x₂ x₃) ∷ st) x = {!!}
208 findPP2 (node key value (node key₁ value₁ x₁ x₃) leaf ∷ st) x = {!!}
209 findPP2 (node key value (node key₁ value₁ x₁ x₃) (node key₂ value₂ x₂ x₄) ∷ st) x = case1 ⟪ {!!} , {!!} ⟫
201 findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) 210 findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
202 findPP1 = {!!} 211 findPP1 = {!!}
203 findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st) 212 findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st)
204 findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) 213 findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
205 findPP2 = {!!} 214 findPP2 = {!!}
206 215
207 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree 216 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
208 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t 217 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t
209 insertTreePP {n} {m} {A} {t} tree key value P exit = 218 insertTreePP {n} {m} {A} {t} tree key value P exit =
210 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) {!!} } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!} 219 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!}
211 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 220 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )
212 $ λ t s P → replaceNodeP key value t {!!} 221 $ λ t s P → replaceNodeP key value t {!!}
213 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) 222 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
214 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } 223 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
215 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫ 224 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫
226 ci : replacedTree key1 value1 tree tree1 235 ci : replacedTree key1 value1 tree tree1
227 236
228 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ 237 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
229 containsTree {n} {m} {A} {t} tree tree1 key value P RT = 238 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
230 TerminatingLoopS (bt A ∧ List (bt A) ) 239 TerminatingLoopS (bt A ∧ List (bt A) )
231 {λ p → findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p)) 240 {λ p → findPR (proj1 p) (proj2 p) ∧ findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p))
232 ⟪ tree1 , [] ⟫ record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { ti = P ; si = lift tt } } 241 ⟪ tree1 , [] ⟫ ⟪ {!!} , record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { tree0 = {!!} ; ti = P ; si = lift tt } } ⟫
233 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 242 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt )
234 $ λ t s P → insertTreeSpec0 t value {!!} 243 $ λ t s P → insertTreeSpec0 t value {!!}
235 244
236 insertTreeSpec1 : {n : Level} {A : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤ 245 insertTreeSpec1 : {n : Level} {A : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
237 insertTreeSpec1 {n} {A} tree key value P = 246 insertTreeSpec1 {n} {A} tree key value P =
238 insertTreeP tree key value P (λ (tree₁ repl : bt A) 247 insertTreeP tree key value P (λ (tree₁ repl : bt A)