Mercurial > hg > Members > Moririn
annotate hoareBinaryTree.agda @ 604:2075785a124a
new approach
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Nov 2021 10:32:56 +0900 |
| parents | 803c423c2855 |
| children | f8cc98fcc34b |
| 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 | |
| 27 | |
| 590 | 28 -- |
| 29 -- | |
| 30 -- no children , having left node , having right node , having both | |
| 31 -- | |
| 597 | 32 data bt {n : Level} (A : Set n) : Set n where |
| 604 | 33 leaf : bt A |
| 34 node : (key : ℕ) → (value : A) → | |
| 35 (left : bt A ) → (write : bt A ) → bt A | |
| 600 | 36 |
| 604 | 37 find : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → List (bt A) |
| 38 → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t | |
| 39 find key leaf st _ exit = exit leaf st | |
| 40 find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁ | |
| 41 find key n st _ exit | tri≈ ¬a b ¬c = exit n st | |
| 42 find key n@(node key₁ v tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) | |
| 43 find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) | |
| 597 | 44 |
| 604 | 45 {-# TERMINATING #-} |
| 46 find-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t | |
| 47 find-loop {_} {A} {t} key tree st exit = find-loop1 tree st where | |
| 48 find-loop1 : bt A → List (bt A) → t | |
| 49 find-loop1 tree st = find key tree st find-loop1 exit | |
| 600 | 50 |
| 604 | 51 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 |
| 52 replace key value tree [] next exit = exit tree | |
| 53 replace key value tree (leaf ∷ st) next exit = next key value tree st | |
| 54 replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁ | |
| 55 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st | |
| 56 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st | |
| 57 ... | 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
|
58 |
| 604 | 59 {-# TERMINATING #-} |
| 60 replace-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (value : A) → bt A → List (bt A) → (exit : bt A → t) → t | |
| 61 replace-loop {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where | |
| 62 replace-loop1 : (key : ℕ) → (value : A) → bt A → List (bt A) → t | |
| 63 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
|
64 |
| 604 | 65 insertTree : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t |
| 66 insertTree tree key value exit = find-loop key tree [] ( λ t st → replace-loop key value t st exit ) | |
| 587 | 67 |
| 604 | 68 insertTest1 = insertTree leaf 1 1 (λ x → x ) |
| 587 | 69 |