Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 625:074fb29ebf57

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 22:30:40 +0900
parents bf27e2c7c6c5
children 6465673df5bc
comparison
equal deleted inserted replaced
624:bf27e2c7c6c5 625:074fb29ebf57
200 200
201 findPP : {n m : Level} {A : Set n} {t : Set m} 201 findPP : {n m : Level} {A : Set n} {t : Set m}
202 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) 202 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
203 → (Pre : findPR tree stack (λ t s → Lift n ⊤)) 203 → (Pre : findPR tree stack (λ t s → Lift n ⊤))
204 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (λ t s → Lift n ⊤) → bt-depth tree1 < bt-depth tree → t ) 204 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (λ t s → Lift n ⊤) → bt-depth tree1 < bt-depth tree → t )
205 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (λ t s → Lift n ⊤) → t) → t 205 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR tree1 stack1 (λ t s → Lift n ⊤) → t) → t
206 findPP key leaf st Pre next exit = exit leaf st Pre 206 findPP key leaf st Pre next exit = exit leaf st (case1 refl) Pre
207 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁ 207 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
208 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st P 208 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st (case2 {!!}) P
209 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 Pre next exit | tri< a ¬b ¬c =
210 next tree (n ∷ st) (record {ti = findPR.ti Pre ; si = findPP2 st (findPR.si Pre) ; ci = lift tt} ) findPP1 where 210 next tree (n ∷ st) (record {ti = findPR.ti Pre ; si = findPP2 st (findPR.si Pre) ; ci = lift tt} ) findPP1 where
211 tree0 = findPR.tree0 Pre 211 tree0 = findPR.tree0 Pre
212 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)
213 findPP2 = {!!} 213 findPP2 = {!!}
220 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
221 → (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
222 insertTreePP {n} {m} {A} {t} tree key value P exit = 222 insertTreePP {n} {m} {A} {t} tree key value P exit =
223 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!} 223 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!}
224 $ λ 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 )
225 $ λ t s P → replaceNodeP key value t {!!} 225 $ λ t s _ P → replaceNodeP key value t {!!}
226 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) 226 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
227 {λ 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)) }
228 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫ 228 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫
229 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!} 229 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!}
230 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit 230 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit
240 240
241 findPPC : {n m : Level} {A : Set n} {t : Set m} 241 findPPC : {n m : Level} {A : Set n} {t : Set m}
242 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) 242 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
243 → (Pre : findPR tree stack findP-contains) 243 → (Pre : findPR tree stack findP-contains)
244 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 findP-contains → bt-depth tree1 < bt-depth tree → t ) 244 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 findP-contains → bt-depth tree1 < bt-depth tree → t )
245 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 findP-contains → t) → t 245 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR tree1 stack1 findP-contains → t) → t
246 findPPC = {!!} 246 findPPC = {!!}
247 247
248 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ 248 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
249 containsTree {n} {m} {A} {t} tree tree1 key value P RT = 249 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
250 TerminatingLoopS (bt A ∧ List (bt A) ) 250 TerminatingLoopS (bt A ∧ List (bt A) )
251 {λ p → findPR (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p)) 251 {λ p → findPR (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p))
252 ⟪ tree1 , [] ⟫ {!!} 252 ⟪ tree1 , [] ⟫ {!!}
253 $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 253 $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )
254 $ λ t1 s1 P2 → insertTreeSpec0 t1 value {!!} 254 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value {!!} where
255 255 lemma3 : ?
256 lemma3 = ?
257