Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 586:0ddfa505d612

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isolate search function problem, and add hoareBinaryTree.agda.
author ryokka
date Wed, 04 Dec 2019 15:42:47 +0900
parents
children f103f07c0552
comparison
equal deleted inserted replaced
585:42e8cf963c5c 586:0ddfa505d612
1 module hoareBinaryTree where
2
3 open import Level renaming (zero to Z ; suc to succ)
4
5 open import Data.Nat hiding (compare)
6 open import Data.Nat.Properties as NatProp
7 open import Data.Maybe
8 open import Data.Maybe.Properties
9 open import Data.Empty
10 open import Data.List
11 open import Data.Product
12
13 open import Function as F hiding (const)
14
15 open import Relation.Binary
16 open import Relation.Binary.PropositionalEquality
17 open import Relation.Nullary
18 open import logic
19
20
21 SingleLinkedStack = List
22
23 emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data
24 emptySingleLinkedStack = []
25
26 clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data → ( SingleLinkedStack Data → t) → t
27 clearSingleLinkedStack [] cg = cg []
28 clearSingleLinkedStack (x ∷ as) cg = cg []
29
30 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
31 pushSingleLinkedStack stack datum next = next ( datum ∷ stack )
32
33 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
34 popSingleLinkedStack [] cs = cs [] nothing
35 popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1)
36
37
38
39 data bt {n : Level} {a : Set n} : ℕ → ℕ → Set n where
40 bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt l u
41 bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) →
42 bt {n} {a} l' d → bt {n} {a} d u' → l ≤ l' → u' ≤ u → bt l u
43
44 lleaf : {n : Level} {a : Set n} → bt {n} {a} 0 3
45 lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
46
47 rleaf : {n : Level} {a : Set n} → bt {n} {a} 3 4
48 rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 4 ⦄ (n≤1+n 3))
49
50 test-node : {n : Level} {a : Set n} → bt {n} {a} 0 4
51 test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )
52
53
54
55 _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
56 d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))
57
58 iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
59 iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }
60
61 -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい
62 -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる
63 bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} l u → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
64 bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing
65 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg with <-cmp key d
66 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
67 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
68 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
69
70
71 -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう
72 bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t
73 bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node
74
75 bt-search-test-bad : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 8 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 7) → ⊥)))) → t) → t
76 bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node
77
78
79 -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ)
80 -- up-some (just (fst , snd)) = just fst
81 -- up-some nothing = nothing
82
83 search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} l u) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata)
84 search-lem {n} {m} {a} {t} key (bt-leaf x) = refl
85 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d
86 search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄ key tree₁
87 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl
88 search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄ key tree₂
89
90
91 -- bt-find
92 find-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → ( (bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
93
94 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing
95 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d
96 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))
97
98 find-support {n} {m} {a} {t} key node@(bt-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c =
99 pushSingleLinkedStack st node
100 (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L {!!} {!!})
101 -- bt が l u の2つの ℕ を受ける、この値はすべてのnodeによって異なるため stack に積むときに型が合わない
102
103 -- find-support ⦃ ll' ⦄ ⦃ d ⦄ key L {!!} {!!})
104
105
106 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = {!!}
107
108
109 bt-find : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → ( (bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
110 bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st (λ cst → find-support key tr cst cg)
111
112
113
114 -- 証明に insert がはいっててほしい
115 -- bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → bt-search d tree (λ pt → ) → t
116 -- bt-insert = ?