Mercurial > hg > Members > Moririn
annotate hoareBinaryTree.agda @ 619:a3fbc9b57015
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Nov 2021 19:43:16 +0900 |
| parents | 5702800c79bc |
| children | fe8c2d82c05c |
| rev | line source |
|---|---|
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
1 module hoareBinaryTree where |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
2 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
3 open import Level renaming (zero to Z ; suc to succ) |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
4 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
5 open import Data.Nat hiding (compare) |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
6 open import Data.Nat.Properties as NatProp |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
7 open import Data.Maybe |
| 588 | 8 -- open import Data.Maybe.Properties |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
9 open import Data.Empty |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
10 open import Data.List |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
11 open import Data.Product |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
12 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
13 open import Function as F hiding (const) |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
14 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
15 open import Relation.Binary |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
16 open import Relation.Binary.PropositionalEquality |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
17 open import Relation.Nullary |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
18 open import logic |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
19 |
|
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
20 |
| 588 | 21 _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set |
| 22 d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d)) | |
| 23 | |
| 24 iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y | |
| 25 iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ } | |
| 26 | |
| 590 | 27 -- |
| 28 -- | |
| 29 -- no children , having left node , having right node , having both | |
| 30 -- | |
| 597 | 31 data bt {n : Level} (A : Set n) : Set n where |
| 604 | 32 leaf : bt A |
| 33 node : (key : ℕ) → (value : A) → | |
| 610 | 34 (left : bt A ) → (right : bt A ) → bt A |
| 600 | 35 |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
36 bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
37 bt-depth leaf = 0 |
| 618 | 38 bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ )) |
| 606 | 39 |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
40 find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A) |
| 604 | 41 → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t |
| 42 find key leaf st _ exit = exit leaf st | |
| 43 find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁ | |
| 44 find key n st _ exit | tri≈ ¬a b ¬c = exit n st | |
| 45 find key n@(node key₁ v tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) | |
| 46 find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) | |
| 597 | 47 |
| 604 | 48 {-# TERMINATING #-} |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
49 find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t |
| 611 | 50 find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where |
| 604 | 51 find-loop1 : bt A → List (bt A) → t |
| 52 find-loop1 tree st = find key tree st find-loop1 exit | |
| 600 | 53 |
| 611 | 54 replaceNode : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → (bt A → t) → t |
| 55 replaceNode k v leaf next = next (node k v leaf leaf) | |
| 56 replaceNode k v (node key value t t₁) next = next (node k v t t₁) | |
| 57 | |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
58 replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t |
| 604 | 59 replace key value tree [] next exit = exit tree |
| 60 replace key value tree (leaf ∷ st) next exit = next key value tree st | |
| 61 replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁ | |
| 62 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st | |
| 63 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st | |
| 64 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
65 |
| 604 | 66 {-# TERMINATING #-} |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
67 replace-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (exit : bt A → t) → t |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
68 replace-loop {_} {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where |
| 604 | 69 replace-loop1 : (key : ℕ) → (value : A) → bt A → List (bt A) → t |
| 70 replace-loop1 key value tree st = replace key value tree st replace-loop1 exit | |
|
586
0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff
changeset
|
71 |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
72 insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t |
| 611 | 73 insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st exit |
| 587 | 74 |
| 604 | 75 insertTest1 = insertTree leaf 1 1 (λ x → x ) |
| 611 | 76 insertTest2 = insertTree insertTest1 2 1 (λ x → x ) |
| 587 | 77 |
| 605 | 78 open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) |
| 79 | |
| 80 treeInvariant : {n : Level} {A : Set n} → (tree : bt A) → Set | |
| 81 treeInvariant leaf = ⊤ | |
| 82 treeInvariant (node key value leaf leaf) = ⊤ | |
| 83 treeInvariant (node key value leaf n@(node key₁ value₁ t₁ t₂)) = (key < key₁) ∧ treeInvariant n | |
| 84 treeInvariant (node key value n@(node key₁ value₁ t t₁) leaf) = treeInvariant n ∧ (key < key₁) | |
| 85 treeInvariant (node key value n@(node key₁ value₁ t t₁) m@(node key₂ value₂ t₂ t₃)) = treeInvariant n ∧ (key < key₁) ∧ (key₁ < key₂) ∧ treeInvariant m | |
| 86 | |
| 87 treeInvariantTest1 = treeInvariant (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf))) | |
| 88 | |
| 610 | 89 stackInvariant : {n : Level} {A : Set n} → (tree : bt A) → (stack : List (bt A)) → Set n |
| 90 stackInvariant {_} {A} _ [] = Lift _ ⊤ | |
| 91 stackInvariant {_} {A} tree (tree1 ∷ [] ) = tree1 ≡ tree | |
| 92 stackInvariant {_} {A} tree (x ∷ tail @ (node key value leaf right ∷ _) ) = (right ≡ x) ∧ stackInvariant tree tail | |
| 93 stackInvariant {_} {A} tree (x ∷ tail @ (node key value left leaf ∷ _) ) = (left ≡ x) ∧ stackInvariant tree tail | |
| 94 stackInvariant {_} {A} tree (x ∷ tail @ (node key value left right ∷ _ )) = ( (left ≡ x) ∧ stackInvariant tree tail) ∨ ( (right ≡ x) ∧ stackInvariant tree tail) | |
| 95 stackInvariant {_} {A} tree s = Lift _ ⊥ | |
| 606 | 96 |
| 613 | 97 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where |
| 615 | 98 r-leaf : replacedTree key value leaf (node key value leaf leaf) |
| 99 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) | |
| 100 r-right : {k : ℕ } {v : A} → {t t1 t2 : bt A} | |
| 101 → k > key → ( replacedTree key value t1 t2 → replacedTree key value (node k v t t1) (node k v t t2) ) | |
| 102 r-left : {k : ℕ } {v : A} → {t t1 t2 : bt A} | |
| 103 → k < key → ( replacedTree key value t1 t2 → replacedTree key value (node k v t1 t) (node k v t2 t) ) | |
| 611 | 104 |
| 615 | 105 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) |
| 106 → treeInvariant tree ∧ stackInvariant tree0 stack | |
| 107 → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree0 stack → bt-depth tree1 < bt-depth tree → t ) | |
| 108 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree0 stack → t ) → t | |
| 109 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st {!!} | |
| 110 findP key (node key₁ v tree tree₁) tree0 st Pre next exit with <-cmp key key₁ | |
| 111 findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st {!!} | |
| 112 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} {!!} | |
| 113 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} {!!} | |
| 606 | 114 |
| 611 | 115 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree ) |
| 613 | 116 → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t |
| 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₁) {!!} {!!} | |
| 606 | 119 |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
120 replaceP : {n m : Level} {A : Set n} {t : Set m} |
| 613 | 121 → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack ∧ replacedTree key value tree repl |
| 614 | 122 → (next : ℕ → A → (tree1 repl : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ replacedTree key value tree1 repl → bt-depth tree1 < bt-depth tree → t ) |
| 613 | 123 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t |
| 124 replaceP key value tree repl [] Pre next exit = exit tree repl {!!} | |
| 614 | 125 replaceP key value tree repl (leaf ∷ st) Pre next exit = next key value tree {!!} st {!!} {!!} |
| 613 | 126 replaceP key value tree repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ |
| 614 | 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 ) {!!} st {!!} {!!} | |
| 129 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) {!!} st {!!} {!!} | |
| 606 | 130 |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
131 open import Relation.Binary.Definitions |
| 606 | 132 |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
133 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
134 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
135 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
136 lemma3 refl () |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
137 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
138 lemma5 (s≤s z≤n) () |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
139 |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
140 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
141 → (r : Index) → (p : Invraiant r) |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
142 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
143 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
144 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
145 ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
146 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
147 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
148 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
149 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
150 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
151 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
152 |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
153 open _∧_ |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
154 |
| 615 | 155 RTtoTI0 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree |
| 156 → replacedTree key value tree repl → treeInvariant repl | |
| 157 RTtoTI0 = {!!} | |
| 158 | |
| 159 RTtoTI1 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl | |
| 160 → replacedTree key value tree repl → treeInvariant tree | |
| 161 RTtoTI1 = {!!} | |
| 614 | 162 |
| 611 | 163 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree |
| 613 | 164 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t |
| 610 | 165 insertTreeP {n} {m} {A} {t} tree key value P exit = |
| 615 | 166 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , lift tt ⟫ |
| 167 $ λ p P loop → findP key (proj1 p) tree (proj2 p) {!!} (λ t _ s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) | |
| 168 $ λ t _ s P → replaceNodeP key value t (proj1 P) | |
| 614 | 169 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) |
| 170 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } | |
| 615 | 171 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫ ⟪ proj1 P , ⟪ {!!} , R ⟫ ⟫ |
| 614 | 172 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) P1 |
| 173 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt ) exit | |
| 174 | |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
175 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
176 top-value leaf = nothing |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
177 top-value (node key value tree tree₁) = just value |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
178 |
| 612 | 179 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
180 insertTreeSpec0 _ _ _ = tt |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
181 |
| 619 | 182 record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where |
| 618 | 183 field |
| 619 | 184 tree0 : bt A |
| 618 | 185 ti : treeInvariant tree |
| 619 | 186 si : stackInvariant tree0 stack |
| 618 | 187 |
| 616 | 188 findPP : {n m : Level} {A : Set n} {t : Set m} |
| 189 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) | |
| 619 | 190 → (Pre : bt A → List (bt A) → findPR tree stack ) |
| 191 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 → bt-depth tree1 < bt-depth tree → t ) | |
| 192 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 → t) → t | |
| 618 | 193 findPP key leaf st Pre next exit = exit leaf st (Pre leaf st ) |
| 616 | 194 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁ |
| 618 | 195 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st (P n st) |
| 619 | 196 findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c = |
| 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 | |
| 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 ⟪ {!!} , {!!} ⟫ | |
| 618 | 210 findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) |
| 211 findPP1 = {!!} | |
| 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) | |
| 213 findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) | |
| 214 findPP2 = {!!} | |
| 616 | 215 |
| 618 | 216 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree |
| 217 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t | |
| 218 insertTreePP {n} {m} {A} {t} tree key value P exit = | |
| 619 | 219 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!} |
| 618 | 220 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) |
| 221 $ λ t s P → replaceNodeP key value t {!!} | |
| 222 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) | |
| 223 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } | |
| 224 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫ ⟪ {!!} , ⟪ {!!} , R ⟫ ⟫ | |
| 225 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) P1 | |
| 226 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt ) exit | |
| 227 | |
| 616 | 228 -- findP key tree stack = findPP key tree stack {findPR} → record { ti = tree-invariant tree ; si stack-invariant tree stack } → |
| 229 | |
| 617 | 230 record findP-contains {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where |
| 616 | 231 field |
| 617 | 232 key1 : ℕ |
| 233 value1 : A | |
| 616 | 234 tree1 : bt A |
| 617 | 235 ci : replacedTree key1 value1 tree tree1 |
| 616 | 236 |
| 618 | 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 → ⊤ |
| 615 | 238 containsTree {n} {m} {A} {t} tree tree1 key value P RT = |
| 617 | 239 TerminatingLoopS (bt A ∧ List (bt A) ) |
| 619 | 240 {λ p → findPR (proj1 p) (proj2 p) ∧ findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p)) |
| 241 ⟪ tree1 , [] ⟫ ⟪ {!!} , record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { tree0 = {!!} ; ti = P ; si = lift tt } } ⟫ | |
| 242 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt ) | |
| 617 | 243 $ λ t s P → insertTreeSpec0 t value {!!} |
| 615 | 244 |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
245 insertTreeSpec1 : {n : Level} {A : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤ |
|
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
606
diff
changeset
|
246 insertTreeSpec1 {n} {A} tree key value P = |
| 613 | 247 insertTreeP tree key value P (λ (tree₁ repl : bt A) |
| 248 (P1 : treeInvariant tree₁ ∧ replacedTree key value tree₁ repl ) → insertTreeSpec0 tree₁ value (lemma1 {!!} ) ) where | |
| 612 | 249 lemma1 : (tree₁ : bt A) → top-value tree₁ ≡ just value |
| 250 lemma1 = {!!} |