annotate rbt_t.agda @ 9:a335a903f87d

add imple
author soto
date Tue, 12 Jan 2021 21:20:16 +0900
parents 5b398e84eae3
children 2521da2c3c9a
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
1 module rbt_t where
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
2
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
3 open import Data.Nat hiding (compare)
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
4 open import Data.Nat.Properties as NatProp -- <-cmp
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
5 open import Relation.Binary
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
6 open import Data.List
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
8 -- → t を適用するために必要だった
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
9 open import Level renaming ( suc to succ ; zero to Zero )
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
10 open import Level
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
11
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
12
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
13 data col : Set where
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
14 black : col
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
15 red : col
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
16
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
17 record node (A B : Set) : Set where
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
18 field
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
19 coler : A
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
20 number : B
9
a335a903f87d add imple
soto
parents: 8
diff changeset
21 open node
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
22
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
23 record tree (A B C : Set) : Set where
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
24 field
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
25 key : A
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
26 ltree : B
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
27 rtree : C
9
a335a903f87d add imple
soto
parents: 8
diff changeset
28 open tree
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
29
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
30 data rbt : Set where
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
31 bt-empty : rbt
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
32 bt-node : (node : tree (node col ℕ) rbt rbt ) → rbt
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
33
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
34 record Env : Set (succ Zero) where
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
35 field
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
36 vart : rbt
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
37 varn : ℕ
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
38 varl : List rbt
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
39 open Env
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
40
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
41 whileTest-next : {l : Level} {t : Set l} → (c10 : rbt) → (n : ℕ) → (list : List rbt) → (next : Env → t) → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
42 whileTest-next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} )
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
43
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
44 merge-tree : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
45
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
46 -- 全てmerge-treeへ
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
47 split : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
48 split node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
49 split node@record { vart = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ; varn = varn ; varl = varl } next exit = exit node
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
50 split node@record { vart = (bt-node record { key = key ; ltree = (bt-node node₁) ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
51 split record { vart = (bt-node record { key = record { coler = coler₁ ; number = number₁ }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
52 ; ltree = (bt-node record { key = record { coler = ly ; number = ln } ; ltree = ll ; rtree = lr })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
53 ; rtree = (bt-node record { key = record { coler = ry ; number = rn } ; ltree = rl ; rtree = rr }) })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
54 ; varn = varn ; varl = varl } next exit
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
55 = next record { vart = (bt-node record { key = record { coler = red ; number = number₁ }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
56 ; ltree = (bt-node record { key = record { coler = black ; number = ln } ; ltree = ll ; rtree = lr })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
57 ; rtree = (bt-node record { key = record { coler = black ; number = rn } ; ltree = rl ; rtree = rr }) })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
58 ; varn = varn ; varl = varl }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
59
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
60
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
61 -- 右回転
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
62 -- 実行時splitへ、それ以外はmerge-treeへ
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
63 merge-rotate-right : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
64 merge-rotate-right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
65 merge-rotate-right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
66 merge-rotate-right record { vart = bt-node record { key = record { coler = y ; number = x }
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
67 ; ltree = (bt-node record { key = record { coler = ly ; number = lx } ; ltree = ll ; rtree = lr })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
68 ; rtree = r }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
69 ; varn = varn ; varl = varl } next exit
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
70 = next record { vart = bt-node record { key = record { coler = y ; number = lx }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
71 ; ltree = ll
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
72 ; rtree = (bt-node record { key = record { coler = red ; number = x } ; ltree = lr; rtree = r }) }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
73 ; varn = varn ; varl = varl }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
74
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
75
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
76 -- split
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
77 split-branch : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
78 split-branch node@record{ vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
79 split-branch node@record{ vart = bt-node record { key = key ; ltree = bt-empty ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
80 split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = lc ; number = number } ; ltree = bt-empty ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
81 split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = (bt-node node₁) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
82 split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = red ; number = number₁ } ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree₁ }) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
83 split-branch node@record{ vart = bt-node record { key = key₁
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
84 ; ltree = (bt-node record { key = record { coler = red ; number = number₁ }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
85 ; ltree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree₁ })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
86 ; rtree = lr })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
87 ; rtree = rtree }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
88 ; varn = varn ; varl = varl } next exit
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
89 = next node
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
90
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
91
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
92 -- 左回転、exitはsplit_branchへ nextもsplit_branchへ
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
93 merge-rotate-left : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
94 merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
95 merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
96 merge-rotate-left record { vart = bt-node record { key = record { coler = y ; number = x } ; ltree = l ; rtree = (bt-node record { key = record { coler = ry ; number = rx } ; ltree = rl ; rtree = rr }) } ; varn = varn ; varl = varl } next exit
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
97 = next record { vart = bt-node record { key = record { coler = y ; number = rx }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
98   ; ltree = (bt-node record { key = record { coler = red ; number = x } ; ltree = l ; rtree = rl })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
99   ; rtree = rr}
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
100   ; varn = varn ; varl = varl }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
101
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
102
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
103 -- skew exitがsplitへ nextが左回転
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
104 skew-bt : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
105 skew-bt node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
106 skew-bt node@record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
107 skew-bt node@record { vart = (bt-node record { key = key₁
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
108 ; ltree = ltree₁
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
109 ; rtree = (bt-node record { key = record { coler = black ; number = number }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
110 ; ltree = ltree ; rtree = rtree }) }) ; varn = varn ; varl = varl } next exit
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
111 = exit node
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
112 skew-bt node@record { vart = (bt-node record { key = key₁
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
113 ; ltree = ltree₁
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
114 ; rtree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree }) })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
115 ; varn = varn ; varl = varl } next exit
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
116 = next node
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
117
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
118
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
119 set-node-coler : Env → Env
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
120 set-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
121 set-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
122 = record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
123
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
124 init-node-coler : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
125 init-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
126 init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
127 = exit record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
128
9
a335a903f87d add imple
soto
parents: 8
diff changeset
129 --修正前
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
130 merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit node
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
131 merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty ∷ varl₁) } next exit = exit node
9
a335a903f87d add imple
soto
parents: 8
diff changeset
132
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
133 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit with <-cmp varn number
9
a335a903f87d add imple
soto
parents: 8
diff changeset
134
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
135 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri≈ ¬a b ¬c
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
136 = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl₁ }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
137
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
138 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri> ¬a ¬b c
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
139 = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = vart }) ; varn = number ; varl = varl₁ }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
140
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
141 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri< a ¬b ¬c
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
142 = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl₁ }
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
143
9
a335a903f87d add imple
soto
parents: 8
diff changeset
144 --修正後
a335a903f87d add imple
soto
parents: 8
diff changeset
145 merge-tree1 : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
a335a903f87d add imple
soto
parents: 8
diff changeset
146 merge-tree1 env next exit with varl env
a335a903f87d add imple
soto
parents: 8
diff changeset
147 ... | [] = exit env
a335a903f87d add imple
soto
parents: 8
diff changeset
148 ... | bt-empty ∷ nl = exit env
a335a903f87d add imple
soto
parents: 8
diff changeset
149 ... | bt-node node₁ ∷ nl with <-cmp (varn env) (number ( key node₁ ))
a335a903f87d add imple
soto
parents: 8
diff changeset
150 ... | tri≈ ¬a b ¬c = next (record env { varn = number (key node₁) ; varl = nl })
a335a903f87d add imple
soto
parents: 8
diff changeset
151 -- next (record{ vart = vart env ; varn = number (key node₁) ; varl = nl })
a335a903f87d add imple
soto
parents: 8
diff changeset
152 ... | tri> ¬a ¬b c = next (record env { vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
a335a903f87d add imple
soto
parents: 8
diff changeset
153 -- next (record{ vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
a335a903f87d add imple
soto
parents: 8
diff changeset
154 ... | tri< a ¬b ¬c = next (record{ vart = (bt-node record { key = key node₁ ; ltree = vart env ; rtree = rtree node₁ }) ; varn = number (key node₁) ; varl = nl })
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
155
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
156 -- insert
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
157 bt-insert : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
158 -- mergeへ遷移する
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
159 bt-insert (record { vart = bt-empty ; varn = varn ; varl = varl }) next exit
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
160 = exit (record { vart = (bt-node (record { key = record { coler = red ; number = varn }; ltree = bt-empty; rtree = bt-empty })) ; varn = varn ; varl = varl })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
161
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
162 -- 場合分けを行う
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
163 bt-insert record {vart = (bt-node record { key = record { coler = y; number = x } ; ltree = ltree ; rtree = rtree }) ; varn = n ; varl = varl } next exit with <-cmp x n
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
164 bt-insert node@(record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } ) next exit | tri≈ ¬a b ¬c
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
165 = exit node
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
166
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
167 bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri> ¬a ¬b c
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
168 = next (record {vart = ltree ; varn = varn ; varl = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ∷ varl })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
169
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
170 bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a ¬b ¬c
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
171 = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ∷ varl })
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
172
9
a335a903f87d add imple
soto
parents: 8
diff changeset
173
a335a903f87d add imple
soto
parents: 8
diff changeset
174
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
175 -- normal loop without termination
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
176 {-# TERMINATING #-}
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
177 insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
178 insert env exit = bt-insert env (λ env → insert env exit ) exit
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
179
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
180
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
181
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
182 init-col : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
183 init-col env exit = init-node-coler env exit exit
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
184
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
185 {-
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
186 {-# TERMINATING #-}
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
187 merge : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
188
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
189 {-# TERMINATING #-}
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
190 split-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
191 split-p env exit = split env (λ env → merge env (λ env → merge env exit ) ) exit
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
192
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
193 {-# TERMINATING #-}
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
194 rotate_right : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
195 rotate_right env exit = merge-rotate-right env (λ env → split-p env (λ env → merge env exit ) ) exit
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
196
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
197 {-# TERMINATING #-}
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
198 split-b : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
199 split-b env exit = split-branch env (λ env → rotate_right env exit ) λ env → merge env exit
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
200
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
201 {-# TERMINATING #-}
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
202 rotate_left : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
203 rotate_left env exit = merge-rotate-left env (λ env → split-b env exit ) exit
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
204
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
205 {-# TERMINATING #-}
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
206 skew : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
207 skew env exit = skew-bt env (λ env → rotate_left env (λ env → split-b env exit ) ) exit
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
208
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
209 merge env exit = merge-tree env (λ env → skew env exit ) exit
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
210 -}
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
211 -- skewはnextがrotate-right。exitはsplitとなる
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
212 -- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
213 -- それはskewのexitと等しいので同時に記述してやる。
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
214 skew' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
215 skew' env exit = skew-bt env (λ env → merge-rotate-left env exit exit ) exit
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
216
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
217 split' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
218 split' env exit = split-branch env (λ env → merge-rotate-right env (λ env → split env exit exit ) (λ env → split env exit exit ) ) exit
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
219
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
220
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
221 {-
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
222 merge' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
223 merge' node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
224 merge' node@record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = merge' (merge-tree node (λ env → skew' env (λ env → split' env (λ env → env) ) ) (λ env → env) ) exit
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
225 -}
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
226
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
227 whileTestP : {l : Level} {t : Set l} → (tree : rbt) → (n : ℕ) → (Code : Env → t) → t
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
228 whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } )
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
229
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
230
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
231
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
232 {-# TERMINATING #-}
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
233 mergeP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
234 mergeP env exit = merge-tree env (λ env → skew' env (λ env → split' env (λ env → mergeP env exit)) ) exit
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
235
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
236 {-
9
a335a903f87d add imple
soto
parents: 8
diff changeset
237 mergeP1 : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
a335a903f87d add imple
soto
parents: 8
diff changeset
238 mergeP1 record { vart = vart ; varn = varn ; varl = [] } exit = {!!}
a335a903f87d add imple
soto
parents: 8
diff changeset
239 mergeP1 record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = {!!}
a335a903f87d add imple
soto
parents: 8
diff changeset
240 -}
a335a903f87d add imple
soto
parents: 8
diff changeset
241
a335a903f87d add imple
soto
parents: 8
diff changeset
242 {-
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
243 merge-tree env
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
244 (λ env → skew-bt env
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
245 (λ env → merge-rotate-left env
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
246 (λ env → split-branch env
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
247 (λ env → merge-rotate-right env
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
248 (λ env → split env (λ env → mergeP env exit ) (λ env → mergeP env exit ) ) exit)
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
249 (λ env → mergeP env exit ) )
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
250 exit )
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
251 exit ) exit
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
252 -}
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
253
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
254 --whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (c11 : ℕ) → (Code : Envc → t) → t
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
255 --whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
256
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
257 --whileTestPCall : (tree : rbt) → (n : ℕ) → Env
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
258 --whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env → init-col env (λ env → env ) ) ) )
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
259
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
260 whileTestPCall' : (tree : rbt) → (n : ℕ) → Env
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
261 whileTestPCall' tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → mergeP env (λ env → init-col env (λ env → env ) ) ) )
7
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
262
06d03fab2668 add continuatioin rbt-insert
soto
parents:
diff changeset
263
8
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
264 -- 以下test部分
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
265 test1 = whileTestPCall' bt-empty 0
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
266 test2 = whileTestPCall' (vart test1) 1
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
267 test3 = whileTestPCall' (vart test2) 2
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
268 test4 = whileTestPCall' (vart test3) 3
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
269 test5 = whileTestPCall' (vart test4) 4
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
270 test6 = whileTestPCall' (vart test5) 5
5b398e84eae3 refactoring
soto
parents: 7
diff changeset
271 test7 = whileTestPCall' (vart test6) 6