Mercurial > hg > Members > Moririn

comparison hoareBinaryTree1.agda @ 598:40ffa0833d03

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add new BinaryTree
author ryokka
date Wed, 26 Feb 2020 18:27:54 +0900
parents
children 7ae0c25d2b58
comparison
equal deleted inserted replaced
597:89fd7cf09b2a 598:40ffa0833d03
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
17 open import Relation.Nullary
18 open import logic
19
20
21 data bt {n : Level} (A : Set n) : Set n where
22 bt-leaf : bt A
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
28 bt-find {n} {m} {A} {t} key leaf@(bt-leaf) 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₁
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
38 bt-replace1 node ((bt-leaf) ∷ 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
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
42 bt-replace0 bt-leaf = bt-replace1 (bt-node ikey a bt-leaf bt-leaf) stack
43
44
45
46
47 bt-empty : {n : Level} {A : Set n} → bt A
48 bt-empty = bt-leaf
49
50 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) )
52
53 find-test : bt ℕ
54 find-test = bt-find 5 bt-empty [] (λ x y → x)
55
56
57 insert-test : bt ℕ
58 insert-test = bt-insert 5 7 bt-empty (λ x → x)
59
60 insert-test1 : bt ℕ
61 insert-test1 = bt-insert 5 7 bt-empty (λ x → bt-insert 15 17 x (λ y → y))
62
63
64 tree+stack : {n : Level} {A : Set n} → (tree mtree : bt A) → (stack : List (bt A)) → Set n
65 tree+stack {n} {A} bt-leaf mtree stack = (mtree ≡ bt-leaf) ∧ (stack ≡ [])
66 tree+stack {n} {A} (bt-node key x tree tree₁) mtree stack = bt-replace key x mtree stack (λ ntree → ntree ≡ tree)
67