Mercurial > hg > Members > Moririn
annotate hoareBinaryTree.agda @ 606:61a0491a627b
with Hoare condition
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Nov 2021 16:14:09 +0900 |
| parents | f8cc98fcc34b |
| children | 79418701a283 |
| 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) → | |
| 34 (left : bt A ) → (write : bt A ) → bt A | |
| 600 | 35 |
| 606 | 36 bt-length : {n : Level} {A : Set n} → (tree : bt A ) → ℕ |
| 37 bt-length leaf = 0 | |
| 38 bt-length (node key value t t₁) = Data.Nat._⊔_ (bt-length t ) (bt-length t₁ ) | |
| 39 | |
| 604 | 40 find : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → List (bt A) |
| 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 #-} |
| 49 find-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t | |
| 50 find-loop {_} {A} {t} key tree st exit = find-loop1 tree st where | |
| 51 find-loop1 : bt A → List (bt A) → t | |
| 52 find-loop1 tree st = find key tree st find-loop1 exit | |
| 600 | 53 |
| 604 | 54 replace : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t |
| 55 replace key value tree [] next exit = exit tree | |
| 56 replace key value tree (leaf ∷ st) next exit = next key value tree st | |
| 57 replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁ | |
| 58 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st | |
| 59 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st | |
| 60 ... | 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
|
61 |
| 604 | 62 {-# TERMINATING #-} |
| 63 replace-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (value : A) → bt A → List (bt A) → (exit : bt A → t) → t | |
| 64 replace-loop {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where | |
| 65 replace-loop1 : (key : ℕ) → (value : A) → bt A → List (bt A) → t | |
| 66 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
|
67 |
| 604 | 68 insertTree : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t |
| 69 insertTree tree key value exit = find-loop key tree [] ( λ t st → replace-loop key value t st exit ) | |
| 587 | 70 |
| 604 | 71 insertTest1 = insertTree leaf 1 1 (λ x → x ) |
| 587 | 72 |
| 605 | 73 open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) |
| 74 | |
| 75 treeInvariant : {n : Level} {A : Set n} → (tree : bt A) → Set | |
| 76 treeInvariant leaf = ⊤ | |
| 77 treeInvariant (node key value leaf leaf) = ⊤ | |
| 78 treeInvariant (node key value leaf n@(node key₁ value₁ t₁ t₂)) = (key < key₁) ∧ treeInvariant n | |
| 79 treeInvariant (node key value n@(node key₁ value₁ t t₁) leaf) = treeInvariant n ∧ (key < key₁) | |
| 80 treeInvariant (node key value n@(node key₁ value₁ t t₁) m@(node key₂ value₂ t₂ t₃)) = treeInvariant n ∧ (key < key₁) ∧ (key₁ < key₂) ∧ treeInvariant m | |
| 81 | |
| 82 treeInvariantTest1 = treeInvariant (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf))) | |
| 83 | |
| 84 stackInvariant : {n : Level} {A : Set n} → (stack : List (bt A)) → Set n | |
| 85 stackInvariant {_} {A} [] = Lift _ ⊤ | |
| 86 stackInvariant {_} {A} (leaf ∷ stack) = Lift _ ⊤ | |
| 87 stackInvariant {_} {A} (node key value leaf leaf ∷ []) = Lift _ ⊤ | |
| 88 stackInvariant {_} {A} (node key value _ (node _ _ _ _) ∷ []) = Lift _ ⊥ | |
| 89 stackInvariant {_} {A} (node key value (node _ _ _ _) _ ∷ []) = Lift _ ⊥ | |
| 90 stackInvariant {_} {A} (x ∷ node key value leaf leaf ∷ tail ) = Lift _ ⊥ | |
| 91 stackInvariant {_} {A} (x ∷ tail @ (node key value leaf tree ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail | |
| 92 stackInvariant {_} {A} (x ∷ tail @ (node key value tree leaf ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail | |
| 93 stackInvariant {_} {A} (x ∷ tail @ (node key value left right ∷ _ )) = ( (left ≡ x) ∧ stackInvariant tail) ∨ ( (right ≡ x) ∧ stackInvariant tail) | |
| 94 stackInvariant {_} {A} s = Lift _ ⊥ | |
| 606 | 95 |
| 96 findP : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) | |
| 97 → treeInvariant tree → stackInvariant stack | |
| 98 → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-length tree1 < bt-length tree → t ) | |
| 99 → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → t ) → t | |
| 100 findP = {!!} | |
| 101 | |
| 102 replaceP : {n : Level} {A : Set n} {t : Set n} | |
| 103 → (key : ℕ) → (value : A) → (tree : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant stack | |
| 104 → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-length tree1 < bt-length tree → t ) | |
| 105 → (exit : (tree1 : bt A) → treeInvariant tree1 → t) → t | |
| 106 replaceP = {!!} | |
| 107 | |
| 108 | |
| 109 | |
| 110 |