|
598
|
1 module hoareBinaryTree1 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
|
|
599
|
17 open import Relation.Nullary hiding (proof)
|
|
598
|
18 open import logic
|
|
|
19
|
|
|
20
|
|
|
21 data bt {n : Level} (A : Set n) : Set n where
|
|
602
|
22 bt-empty : bt A
|
|
598
|
23 bt-node : (key : ℕ) → A →
|
|
|
24 (ltree : bt A) → (rtree : bt A) → bt A
|
|
|
25
|
|
|
26 bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
|
|
|
27 → ( bt A → List (bt A) → t ) → t
|
|
602
|
28 bt-find {n} {m} {A} {t} key leaf@(bt-empty) stack exit = exit leaf stack
|
|
598
|
29 bt-find {n} {m} {A} {t} key (bt-node key₁ AA tree tree₁) stack next with <-cmp key key₁
|
|
|
30 bt-find {n} {m} {A} {t} key node@(bt-node key₁ AA tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack
|
|
|
31 bt-find {n} {m} {A} {t} key node@(bt-node key₁ AA ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (node ∷ stack) next
|
|
|
32 bt-find {n} {m} {A} {t} key node@(bt-node key₁ AA ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (node ∷ stack) next
|
|
|
33
|
|
|
34 bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → List (bt A) → (bt A → t ) → t
|
|
|
35 bt-replace {n} {m} {A} {t} ikey a otree stack next = bt-replace0 otree where
|
|
|
36 bt-replace1 : bt A → List (bt A) → t
|
|
|
37 bt-replace1 tree [] = next tree
|
|
602
|
38 bt-replace1 node ((bt-empty) ∷ stack) = bt-replace1 node stack
|
|
598
|
39 bt-replace1 node ((bt-node key₁ b x x₁) ∷ stack) = bt-replace1 (bt-node key₁ b node x₁) stack
|
|
|
40 bt-replace0 : (tree : bt A) → t
|
|
|
41 bt-replace0 tree@(bt-node key _ ltr rtr) = bt-replace1 (bt-node ikey a ltr rtr) stack -- find case
|
|
602
|
42 bt-replace0 bt-empty = bt-replace1 (bt-node ikey a bt-empty bt-empty) stack
|
|
598
|
43
|
|
|
44
|
|
602
|
45 bt-Empty : {n : Level} {A : Set n} → bt A
|
|
|
46 bt-Empty = bt-empty
|
|
598
|
47
|
|
|
48 bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → (bt A → t ) → t
|
|
|
49 bt-insert key a tree next = bt-find key tree [] (λ mtree stack → bt-replace key a mtree stack (λ tree → next tree) )
|
|
|
50
|
|
|
51 find-test : bt ℕ
|
|
|
52 find-test = bt-find 5 bt-empty [] (λ x y → x)
|
|
|
53
|
|
|
54
|
|
|
55 insert-test : bt ℕ
|
|
|
56 insert-test = bt-insert 5 7 bt-empty (λ x → x)
|
|
|
57
|
|
|
58 insert-test1 : bt ℕ
|
|
|
59 insert-test1 = bt-insert 5 7 bt-empty (λ x → bt-insert 15 17 x (λ y → y))
|
|
|
60
|
|
602
|
61 insert-test2 : {n : Level} {t : Set n} → ( bt ℕ → t ) → t
|
|
|
62 insert-test2 next = bt-insert 15 17 bt-empty
|
|
|
63 $ λ x1 → bt-insert 5 7 x1
|
|
|
64 $ λ x2 → bt-insert 1 3 x2
|
|
|
65 $ λ x3 → bt-insert 4 2 x3
|
|
|
66 $ λ x4 → bt-insert 1 4 x4
|
|
|
67 $ λ y → next y
|
|
|
68
|
|
|
69 insert-test3 : bt ℕ
|
|
|
70 insert-test3 = bt-insert 15 17 bt-empty
|
|
|
71 $ λ x1 → bt-insert 5 7 x1
|
|
|
72 $ λ x2 → bt-insert 1 3 x2
|
|
|
73 $ λ x3 → bt-insert 4 2 x3
|
|
|
74 $ λ x4 → bt-insert 1 4 x4
|
|
|
75 $ λ y → y
|
|
|
76
|
|
|
77 insert-find0 : bt ℕ
|
|
|
78 insert-find0 = insert-test2 $ λ tree → bt-find 1 tree [] $ λ x y → x
|
|
|
79
|
|
|
80 insert-find1 : List (bt ℕ)
|
|
|
81 insert-find1 = insert-test2 $ λ tree → bt-find 1 tree [] $ λ x y → y
|
|
|
82
|
|
|
83 --
|
|
|
84 -- 1 After insert, all node except inserted node is preserved
|
|
|
85 -- 2 After insert, specified key node is inserted
|
|
|
86 -- 3 tree node order is consistent
|
|
|
87 --
|
|
|
88 -- 4 noes on stack + current node = original top node .... invriant bt-find
|
|
|
89 -- 5 noes on stack + current node = original top node with replaced node .... invriant bt-replace
|
|
598
|
90
|
|
599
|
91 tree+stack0 : {n : Level} {A : Set n} → (tree mtree : bt A) → (stack : List (bt A)) → Set n
|
|
|
92 tree+stack0 {n} {A} tree mtree [] = {!!}
|
|
|
93 tree+stack0 {n} {A} tree mtree (x ∷ stack) = {!!}
|
|
|
94
|
|
598
|
95 tree+stack : {n : Level} {A : Set n} → (tree mtree : bt A) → (stack : List (bt A)) → Set n
|
|
602
|
96 tree+stack {n} {A} bt-empty mtree stack = (mtree ≡ bt-empty) ∧ (stack ≡ [])
|
|
598
|
97 tree+stack {n} {A} (bt-node key x tree tree₁) mtree stack = bt-replace key x mtree stack (λ ntree → ntree ≡ tree)
|
|
|
98
|
|
599
|
99 data _implies_ (A B : Set ) : Set (succ Z) where
|
|
|
100 proof : ( A → B ) → A implies B
|
|
|
101
|
|
|
102 implies2p : {A B : Set } → A implies B → A → B
|
|
|
103 implies2p (proof x) = x
|
|
|
104
|
|
|
105
|
|
|
106 bt-find-hoare1 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (stack : List (bt A))
|
|
|
107 → (tree+stack tree mtree stack)
|
|
|
108 → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t
|
|
602
|
109 bt-find-hoare1 {n} {m} {A} {t} key leaf@(bt-empty) mtree stack t+s exit = exit leaf stack {!!}
|
|
599
|
110 bt-find-hoare1 {n} {m} {A} {t} key (bt-node key₁ AA tree tree₁) mtree stack t+s next with <-cmp key key₁
|
|
|
111 bt-find-hoare1 {n} {m} {A} {t} key node@(bt-node key₁ AA tree tree₁) mtree stack t+s exit | tri≈ ¬a b ¬c = exit node stack {!!}
|
|
|
112 bt-find-hoare1 {n} {m} {A} {t} key node@(bt-node key₁ AA ltree rtree) mtree stack t+s next | tri< a ¬b ¬c = bt-find-hoare1 {n} {m} {A} {t} key ltree {!!} (node ∷ stack) {!!} {!!}
|
|
|
113 bt-find-hoare1 {n} {m} {A} {t} key node@(bt-node key₁ AA ltree rtree) mtree stack t+s next | tri> ¬a ¬b c = bt-find-hoare1 key rtree {!!} (node ∷ stack) {!!} {!!}
|
|
|
114
|
|
|
115
|
|
|
116 bt-find-hoare : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t
|
|
|
117 bt-find-hoare {n} {m} {A} {t} key node exit = bt-find-hoare1 {n} {m} {A} {t} key node bt-empty [] ({!!}) exit
|
