Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 612:57d6c594da08

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 Fri, 05 Nov 2021 09:35:20 +0900
parents db42d1033857
children eeb9eb38e5e2
comparison
equal deleted inserted replaced
611:db42d1033857 612:57d6c594da08
116 → ((tree : bt A) → treeInvariant tree → (rstack : List (bt A)) → rstackInvariant tree rstack → t) → t 116 → ((tree : bt A) → treeInvariant tree → (rstack : List (bt A)) → rstackInvariant tree rstack → t) → t
117 replaceNodeP k v leaf P next = next (node k v leaf leaf) {!!} {!!} {!!} 117 replaceNodeP k v leaf P next = next (node k v leaf leaf) {!!} {!!} {!!}
118 replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!} {!!} 118 replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!} {!!}
119 119
120 replaceP : {n m : Level} {A : Set n} {t : Set m} 120 replaceP : {n m : Level} {A : Set n} {t : Set m}
121 → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack ∧ rstackInvariant tree rstack 121 → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack ∧ rstackInvariant repl rstack
122 → (next : ℕ → A → (tree1 repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ rstackInvariant repl rstack → bt-depth tree1 < bt-depth tree → t ) 122 → (next : ℕ → A → (tree1 : bt A) → (stack rstack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ rstackInvariant repl rstack → bt-depth tree1 < bt-depth tree → t )
123 → (exit : (tree1 repl : bt A) → (rstack : List (bt A)) → treeInvariant tree1 ∧ rstackInvariant repl rstack → t) → t 123 → (exit : (tree1 repl : bt A) → (rstack : List (bt A)) → treeInvariant tree1 ∧ rstackInvariant repl rstack → t) → t
124 replaceP key value tree repl [] rs Pre next exit = exit tree repl {!!} {!!} 124 replaceP key value tree repl [] rs Pre next exit = exit tree repl {!!} {!!}
125 replaceP key value tree repl (leaf ∷ st) rs Pre next exit = next key value tree repl st {!!} {!!} {!!} 125 replaceP key value tree repl (leaf ∷ st) rs Pre next exit = next key value tree st {!!} {!!} {!!}
126 replaceP key value tree repl (node key₁ value₁ left right ∷ st) rs Pre next exit with <-cmp key key₁ 126 replaceP key value tree repl (node key₁ value₁ left right ∷ st) rs Pre next exit with <-cmp key key₁
127 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) repl st {!!} {!!} {!!} 127 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st {!!} {!!} {!!}
128 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) repl st {!!} {!!} {!!} 128 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st {!!} {!!} {!!}
129 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) repl st {!!} {!!} {!!} 129 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st {!!} {!!} {!!}
130 130
131 open import Relation.Binary.Definitions 131 open import Relation.Binary.Definitions
132 132
133 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ 133 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
134 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x 134 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
159 $ λ p P loop → findP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) 159 $ λ p P loop → findP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
160 $ λ t s P → replaceNodeP key value t (proj1 P) 160 $ λ t s P → replaceNodeP key value t (proj1 P)
161 $ λ t1 P1 r R → TerminatingLoopS (bt A ∧ List (bt A) ∧ List (bt A)) 161 $ λ t1 P1 r R → TerminatingLoopS (bt A ∧ List (bt A) ∧ List (bt A))
162 {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p)) ∧ rstackInvariant t1 (proj2 (proj2 p))} 162 {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p)) ∧ rstackInvariant t1 (proj2 (proj2 p))}
163 (λ p → bt-depth (proj1 p)) ⟪ t , ⟪ s , r ⟫ ⟫　⟪ proj1 P , ⟪ proj2 P , R ⟫ ⟫ 163 (λ p → bt-depth (proj1 p)) ⟪ t , ⟪ s , r ⟫ ⟫　⟪ proj1 P , ⟪ proj2 P , R ⟫ ⟫
164 $ λ p P1 loop → replaceP key value (proj1 p) {!!} (proj1 (proj2 p)) (proj2 (proj2 p)) {!!} (λ k v t repl s s1 P2 lt → loop ⟪ t , ⟪ {!!} , s1 ⟫ ⟫ {!!} {!!} ) exit 164 $ λ p P1 loop → replaceP key value (proj1 p) t1 (proj1 (proj2 p)) (proj2 (proj2 p)) P1 (λ k v t s s1 P2 lt → loop ⟪ t , ⟪ s , s1 ⟫ ⟫ P2 lt ) exit
165
166 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A 165 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A
167 top-value leaf = nothing 166 top-value leaf = nothing
168 top-value (node key value tree tree₁) = just value 167 top-value (node key value tree tree₁) = just value
169 168
170 insertTreeSpec0 : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ 169 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
171 insertTreeSpec0 _ _ _ = tt 170 insertTreeSpec0 _ _ _ = tt
172 171
173 insertTreeSpec1 : {n : Level} {A : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤ 172 insertTreeSpec1 : {n : Level} {A : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
174 insertTreeSpec1 {n} {A} tree key value P = 173 insertTreeSpec1 {n} {A} tree key value P =
175 insertTreeP tree key value P (λ (tree₁ repl : bt A) (rstack : List (bt A)) 174 insertTreeP tree key value P (λ (tree₁ repl : bt A) (rstack : List (bt A))
176 (P1 : treeInvariant tree₁ ∧ rstackInvariant repl rstack ) → insertTreeSpec0 tree₁ value {!!} ) 175 (P1 : treeInvariant tree₁ ∧ rstackInvariant repl rstack ) → insertTreeSpec0 tree₁ value (lemma1 {!!} ) ) where
176 lemma1 : (tree₁ : bt A) → top-value tree₁ ≡ just value
177 lemma1 = {!!}