Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 623:753353a41da5

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 Mon, 08 Nov 2021 21:07:41 +0900
parents a1849f24fa66
children bf27e2c7c6c5
comparison
equal deleted inserted replaced
622:a1849f24fa66 623:753353a41da5
189 top-value (node key value tree tree₁) = just value 189 top-value (node key value tree tree₁) = just value
190 190
191 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ 191 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
192 insertTreeSpec0 _ _ _ = tt 192 insertTreeSpec0 _ _ _ = tt
193 193
194 record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where 194 record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where
195 field 195 field
196 tree0 : bt A 196 tree0 : bt A
197 ti : treeInvariant tree0 197 ti : treeInvariant tree0
198 si : stackInvariant tree tree0 stack 198 si : stackInvariant tree tree0 stack
199 ci : C tree stack
199 200
200 findPP : {n m : Level} {A : Set n} {t : Set m} 201 findPP : {n m : Level} {A : Set n} {t : Set m}
201 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) 202 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
202 → (Pre : findPR tree stack ) 203 → (C : bt A → List (bt A) → Set n ) (Pre : findPR tree stack {!!} )
203 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 → bt-depth tree1 < bt-depth tree → t ) 204 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 {!!} → bt-depth tree1 < bt-depth tree → t )
204 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 → t) → t 205 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 {!!} → t) → t
205 findPP key leaf st Pre next exit = exit leaf st Pre 206 findPP key leaf st C Pre next exit = exit leaf st Pre
206 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁ 207 findPP key (node key₁ v tree tree₁) st C Pre next exit with <-cmp key key₁
207 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st P 208 findPP key n st C P next exit | tri≈ ¬a b ¬c = exit n st P
208 findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c = 209 findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st C Pre next exit | tri< a ¬b ¬c =
209 next tree (n ∷ st) (record {ti = findPR.ti Pre ; si = findPP2 st (findPR.si Pre)} ) findPP1 where 210 next tree (n ∷ st) (record {ti = findPR.ti Pre ; si = findPP2 st (findPR.si Pre) ; ci = ?} ) findPP1 where
210 tree0 = findPR.tree0 Pre 211 tree0 = findPR.tree0 Pre
211 findPP2 : (st : List (bt A)) → stackInvariant {!!} tree0 st → stackInvariant {!!} tree0 (node key₁ v tree tree₁ ∷ st) 212 findPP2 : (st : List (bt A)) → stackInvariant {!!} tree0 st → stackInvariant {!!} tree0 (node key₁ v tree tree₁ ∷ st)
212 findPP2 = ? 213 findPP2 = {!!}
213 findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) 214 findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
214 findPP1 = {!!} 215 findPP1 = {!!}
215 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) 216 findPP key n@(node key₁ v tree tree₁) st C Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st)
216 findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) 217 findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
217 findPP2 = {!!} 218 findPP2 = {!!}
218 219
219 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree 220 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
220 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t 221 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t
221 insertTreePP {n} {m} {A} {t} tree key value P exit = 222 insertTreePP {n} {m} {A} {t} tree key value P exit =
222 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!} 223 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) {!!} } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!}
223 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 224 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )
224 $ λ t s P → replaceNodeP key value t {!!} 225 $ λ t s P → replaceNodeP key value t {!!}
225 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) 226 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
226 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } 227 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
227 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫ 228 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫
238 ci : replacedTree key1 value1 tree tree1 239 ci : replacedTree key1 value1 tree tree1
239 240
240 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ 241 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
241 containsTree {n} {m} {A} {t} tree tree1 key value P RT = 242 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
242 TerminatingLoopS (bt A ∧ List (bt A) ) 243 TerminatingLoopS (bt A ∧ List (bt A) )
243 {λ p → findPR (proj1 p) (proj2 p) ∧ findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p)) 244 {λ p → findPR (proj1 p) (proj2 p) {!!} ∧ findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p))
244 ⟪ tree1 , [] ⟫ ⟪ {!!} , record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { tree0 = {!!} ; ti = P ; si = lift tt } } ⟫ 245 ⟪ tree1 , [] ⟫ ⟪ {!!} , record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { tree0 = {!!} ; ti = P ; si = lift tt } } ⟫
245 $ λ p P loop → findPP key (proj1 p) (proj2 p) (proj1 P) (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt ) 246 $ λ p P loop → findPP key (proj1 p) (proj2 p) (proj1 P) (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt )
246 $ λ t1 s1 P2 → insertTreeSpec0 t1 value {!!} 247 $ λ t1 s1 P2 → insertTreeSpec0 t1 value {!!}
247 248