Mercurial > hg > Members > Moririn

comparison hoareBinaryTree1.agda @ 602:0dbbcab02864

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jun 2020 15:44:39 +0900
parents 7ae0c25d2b58
children
comparison
equal deleted inserted replaced
601:803c423c2855 602:0dbbcab02864
17 open import Relation.Nullary hiding (proof) 17 open import Relation.Nullary hiding (proof)
18 open import logic 18 open import logic
19 19
20 20
21 data bt {n : Level} (A : Set n) : Set n where 21 data bt {n : Level} (A : Set n) : Set n where
22 bt-leaf : bt A 22 bt-empty : bt A
23 bt-node : (key : ℕ) → A → 23 bt-node : (key : ℕ) → A →
24 (ltree : bt A) → (rtree : bt A) → bt A 24 (ltree : bt A) → (rtree : bt A) → bt A
25 25
26 bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A) 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 27 → ( bt A → List (bt A) → t ) → t
28 bt-find {n} {m} {A} {t} key leaf@(bt-leaf) stack exit = exit leaf stack 28 bt-find {n} {m} {A} {t} key leaf@(bt-empty) stack exit = exit leaf stack
29 bt-find {n} {m} {A} {t} key (bt-node key₁ AA tree tree₁) stack next with <-cmp key key₁ 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 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 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 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 33
34 bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → List (bt A) → (bt A → t ) → t 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 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 36 bt-replace1 : bt A → List (bt A) → t
37 bt-replace1 tree [] = next tree 37 bt-replace1 tree [] = next tree
38 bt-replace1 node ((bt-leaf) ∷ stack) = bt-replace1 node stack 38 bt-replace1 node ((bt-empty) ∷ stack) = bt-replace1 node stack
39 bt-replace1 node ((bt-node key₁ b x x₁) ∷ stack) = bt-replace1 (bt-node key₁ b node x₁) stack 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 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 41 bt-replace0 tree@(bt-node key _ ltr rtr) = bt-replace1 (bt-node ikey a ltr rtr) stack -- find case
42 bt-replace0 bt-leaf = bt-replace1 (bt-node ikey a bt-leaf bt-leaf) stack 42 bt-replace0 bt-empty = bt-replace1 (bt-node ikey a bt-empty bt-empty) stack
43 43
44 44
45 45 bt-Empty : {n : Level} {A : Set n} → bt A
46 46 bt-Empty = bt-empty
47 bt-empty : {n : Level} {A : Set n} → bt A
48 bt-empty = bt-leaf
49 47
50 bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → (bt A → t ) → t 48 bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → (bt A → t ) → t
51 bt-insert key a tree next = bt-find key tree [] (λ mtree stack → bt-replace key a mtree stack (λ tree → next tree) ) 49 bt-insert key a tree next = bt-find key tree [] (λ mtree stack → bt-replace key a mtree stack (λ tree → next tree) )
52 50
53 find-test : bt ℕ 51 find-test : bt ℕ
58 insert-test = bt-insert 5 7 bt-empty (λ x → x) 56 insert-test = bt-insert 5 7 bt-empty (λ x → x)
59 57
60 insert-test1 : bt ℕ 58 insert-test1 : bt ℕ
61 insert-test1 = bt-insert 5 7 bt-empty (λ x → bt-insert 15 17 x (λ y → y)) 59 insert-test1 = bt-insert 5 7 bt-empty (λ x → bt-insert 15 17 x (λ y → y))
62 60
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
63 90
64 tree+stack0 : {n : Level} {A : Set n} → (tree mtree : bt A) → (stack : List (bt A)) → Set n 91 tree+stack0 : {n : Level} {A : Set n} → (tree mtree : bt A) → (stack : List (bt A)) → Set n
65 tree+stack0 {n} {A} tree mtree [] = {!!} 92 tree+stack0 {n} {A} tree mtree [] = {!!}
66 tree+stack0 {n} {A} tree mtree (x ∷ stack) = {!!} 93 tree+stack0 {n} {A} tree mtree (x ∷ stack) = {!!}
67 94
68 tree+stack : {n : Level} {A : Set n} → (tree mtree : bt A) → (stack : List (bt A)) → Set n 95 tree+stack : {n : Level} {A : Set n} → (tree mtree : bt A) → (stack : List (bt A)) → Set n
69 tree+stack {n} {A} bt-leaf mtree stack = (mtree ≡ bt-leaf) ∧ (stack ≡ []) 96 tree+stack {n} {A} bt-empty mtree stack = (mtree ≡ bt-empty) ∧ (stack ≡ [])
70 tree+stack {n} {A} (bt-node key x tree tree₁) mtree stack = bt-replace key x mtree stack (λ ntree → ntree ≡ tree) 97 tree+stack {n} {A} (bt-node key x tree tree₁) mtree stack = bt-replace key x mtree stack (λ ntree → ntree ≡ tree)
71 98
72 data _implies_ (A B : Set ) : Set (succ Z) where 99 data _implies_ (A B : Set ) : Set (succ Z) where
73 proof : ( A → B ) → A implies B 100 proof : ( A → B ) → A implies B
74 101
77 104
78 105
79 bt-find-hoare1 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (stack : List (bt A)) 106 bt-find-hoare1 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (stack : List (bt A))
80 → (tree+stack tree mtree stack) 107 → (tree+stack tree mtree stack)
81 → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t 108 → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t
82 bt-find-hoare1 {n} {m} {A} {t} key leaf@(bt-leaf) mtree stack t+s exit = exit leaf stack {!!} 109 bt-find-hoare1 {n} {m} {A} {t} key leaf@(bt-empty) mtree stack t+s exit = exit leaf stack {!!}
83 bt-find-hoare1 {n} {m} {A} {t} key (bt-node key₁ AA tree tree₁) mtree stack t+s next with <-cmp key key₁ 110 bt-find-hoare1 {n} {m} {A} {t} key (bt-node key₁ AA tree tree₁) mtree stack t+s next with <-cmp key key₁
84 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 {!!} 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 {!!}
85 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) {!!} {!!} 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) {!!} {!!}
86 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) {!!} {!!} 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) {!!} {!!}
87 114