24 ZERO ("\<^bold>0" 81) and |
24 ZERO ("\<^bold>0" 81) and |
25 ONE ("\<^bold>1" 81) and |
25 ONE ("\<^bold>1" 81) and |
26 CH ("_" [1000] 80) and |
26 CH ("_" [1000] 80) and |
27 ALT ("_ + _" [77,77] 78) and |
27 ALT ("_ + _" [77,77] 78) and |
28 SEQ ("_ \<cdot> _" [77,77] 78) and |
28 SEQ ("_ \<cdot> _" [77,77] 78) and |
29 STAR ("_\<^sup>\<star>" [79] 78) |
29 STAR ("_\<^sup>\<star>" [79] 78) and |
|
30 |
|
31 val.Void ("Empty" 78) and |
|
32 val.Char ("Char _" [1000] 78) and |
|
33 val.Left ("Left _" [79] 78) and |
|
34 val.Right ("Right _" [1000] 78) and |
|
35 val.Seq ("Seq _ _" [79,79] 78) and |
|
36 val.Stars ("Stars _" [79] 78) and |
|
37 |
|
38 Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and |
|
39 |
|
40 flat ("|_|" [75] 74) and |
|
41 flats ("|_|" [72] 74) and |
|
42 injval ("inj _ _ _" [79,77,79] 76) and |
|
43 mkeps ("mkeps _" [79] 76) and |
|
44 length ("len _" [73] 73) and |
|
45 set ("_" [73] 73) and |
|
46 |
|
47 AZERO ("ZERO" 81) and |
|
48 AONE ("ONE _" [79] 81) and |
|
49 ACHAR ("CHAR _ _" [79, 79] 80) and |
|
50 AALTs ("ALTs _ _" [77,77] 78) and |
|
51 ASEQ ("SEQ _ _ _" [79, 77,77] 78) and |
|
52 ASTAR ("STAR _ _" [79, 79] 78) and |
|
53 |
|
54 code ("code _" [79] 74) and |
|
55 intern ("_\<^latex>\<open>\\mbox{$^\\uparrow$}\<close>" [900] 80) and |
|
56 erase ("_\<^latex>\<open>\\mbox{$^\\downarrow$}\<close>" [1000] 74) and |
|
57 bnullable ("nullable\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and |
|
58 bmkeps ("mkeps\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) |
|
59 |
|
60 |
|
61 lemma better_retrieve: |
|
62 shows "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v" |
|
63 and "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v" |
|
64 apply (metis list.exhaust retrieve.simps(4)) |
|
65 by (metis list.exhaust retrieve.simps(5)) |
30 |
66 |
31 (*>*) |
67 (*>*) |
32 |
68 |
33 section {* Introduction *} |
69 section {* Introduction *} |
34 |
70 |
73 left-most symbol and only matches the next symbol in case of a mismatch |
109 left-most symbol and only matches the next symbol in case of a mismatch |
74 (this is greedy in the sense of preferring instant gratification to |
110 (this is greedy in the sense of preferring instant gratification to |
75 delayed repletion). The second case is POSIX matching, which prefers the |
111 delayed repletion). The second case is POSIX matching, which prefers the |
76 longest match. |
112 longest match. |
77 |
113 |
|
114 |
|
115 \begin{center} |
|
116 \begin{tabular}{cc} |
|
117 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
|
118 @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\ |
|
119 @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\ |
|
120 @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\ |
|
121 @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\ |
|
122 @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{text "if"} @{term "nullable(r\<^sub>1)"}\\ |
|
123 & & @{text "then"} @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}\\ |
|
124 & & @{text "else"} @{term "SEQ (der c r\<^sub>1) r\<^sub>2"}\\ |
|
125 % & & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\ |
|
126 @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)} |
|
127 \end{tabular} |
|
128 & |
|
129 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
130 @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\ |
|
131 @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\ |
|
132 @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\ |
|
133 @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
134 @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
135 @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\ |
|
136 \end{tabular} |
|
137 \end{tabular} |
|
138 \end{center} |
78 |
139 |
79 |
140 |
80 \begin{figure}[t] |
141 \begin{figure}[t] |
81 \begin{center} |
142 \begin{center} |
82 \begin{tikzpicture}[scale=2,node distance=1.3cm, |
143 \begin{tikzpicture}[scale=2,node distance=1.3cm, |
149 \end{center} |
210 \end{center} |
150 \caption{Our inductive definition of POSIX values.}\label{POSIXrules} |
211 \caption{Our inductive definition of POSIX values.}\label{POSIXrules} |
151 \end{figure} |
212 \end{figure} |
152 |
213 |
153 |
214 |
154 *} |
215 \begin{center} |
155 |
216 \begin{tabular}{lcl} |
156 section {* Bitcoded Derivatives *} |
217 @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\ |
|
218 @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
219 @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
220 @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\ |
|
221 \end{tabular} |
|
222 \end{center} |
|
223 |
|
224 \begin{center} |
|
225 \begin{tabular}{l@ {\hspace{5mm}}lcl} |
|
226 \textit{(1)} & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ |
|
227 \textit{(2)} & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
|
228 @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
|
229 \textit{(3)} & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
|
230 @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
|
231 \textit{(4)} & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
|
232 & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
|
233 \textit{(5)} & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
|
234 & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
|
235 \textit{(6)} & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ |
|
236 & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
|
237 \textit{(7)} & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ |
|
238 & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\ |
|
239 \end{tabular} |
|
240 \end{center} |
|
241 |
|
242 *} |
|
243 |
|
244 section {* Bitcoded Regular Expressions and Derivatives *} |
157 |
245 |
158 text {* |
246 text {* |
159 bitcoded regexes / decoding / bmkeps |
247 bitcoded regexes / decoding / bmkeps |
160 gets rid of the second phase (only single phase) |
248 gets rid of the second phase (only single phase) |
161 correctness |
249 correctness |
|
250 |
|
251 |
|
252 \begin{center} |
|
253 \begin{tabular}{lcl} |
|
254 @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ |
|
255 @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ |
|
256 @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ |
|
257 @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ |
|
258 @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ |
|
259 @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ |
|
260 @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} |
|
261 \end{tabular} |
|
262 \end{center} |
|
263 |
|
264 |
|
265 The idea of the bitcodes is to annotate them to regular expressions and generate values |
|
266 incrementally. The bitcodes can be read off from the @{text breg} and then decoded into a value. |
|
267 |
|
268 \begin{center} |
|
269 \begin{tabular}{lcl} |
|
270 @{term breg} & $::=$ & @{term "AZERO"}\\ |
|
271 & $\mid$ & @{term "AONE bs"}\\ |
|
272 & $\mid$ & @{term "ACHAR bs c"}\\ |
|
273 & $\mid$ & @{term "AALTs bs rs"}\\ |
|
274 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
|
275 & $\mid$ & @{term "ASTAR bs r"} |
|
276 \end{tabular} |
|
277 \end{center} |
|
278 |
|
279 |
|
280 |
|
281 \begin{center} |
|
282 \begin{tabular}{lcl} |
|
283 @{thm (lhs) retrieve.simps(1)} & $\dn$ & @{thm (rhs) retrieve.simps(1)}\\ |
|
284 @{thm (lhs) retrieve.simps(2)} & $\dn$ & @{thm (rhs) retrieve.simps(2)}\\ |
|
285 @{thm (lhs) retrieve.simps(3)} & $\dn$ & @{thm (rhs) retrieve.simps(3)}\\ |
|
286 @{thm (lhs) better_retrieve(1)} & $\dn$ & @{thm (rhs) better_retrieve(1)}\\ |
|
287 @{thm (lhs) better_retrieve(2)} & $\dn$ & @{thm (rhs) better_retrieve(2)}\\ |
|
288 @{thm (lhs) retrieve.simps(6)[of _ "r\<^sub>1" "r\<^sub>2" "v\<^sub>1" "v\<^sub>2"]} |
|
289 & $\dn$ & @{thm (rhs) retrieve.simps(6)[of _ "r\<^sub>1" "r\<^sub>2" "v\<^sub>1" "v\<^sub>2"]}\\ |
|
290 @{thm (lhs) retrieve.simps(7)} & $\dn$ & @{thm (rhs) retrieve.simps(7)}\\ |
|
291 @{thm (lhs) retrieve.simps(8)} & $\dn$ & @{thm (rhs) retrieve.simps(8)} |
|
292 \end{tabular} |
|
293 \end{center} |
|
294 |
|
295 |
|
296 \begin{theorem} |
|
297 @{thm blexer_correctness} |
|
298 \end{theorem} |
162 *} |
299 *} |
163 |
300 |
164 |
301 |
165 section {* Simplification *} |
302 section {* Simplification *} |
166 |
303 |
167 text {* |
304 text {* |
168 Sulzmann \& Lu apply simplification via a fixpoint operation; also does not use erase to filter out duplicates. |
305 Sulzmann \& Lu apply simplification via a fixpoint operation; also does not use erase to filter out duplicates. |
169 |
306 |
170 not direct correspondence with PDERs, because of example |
307 not direct correspondence with PDERs, because of example |
171 problem with retrieve |
308 problem with retrieve |
172 |
309 |
173 correctness |
310 correctness |
174 |
311 |
|
312 |
|
313 |
|
314 |
175 |
315 |
176 |
316 |
177 \begin{figure}[t] |
317 \begin{figure}[t] |
178 \begin{center} |
318 \begin{center} |
179 \begin{tabular}{c} |
319 \begin{tabular}{c} |
180 @{thm[mode=Axiom] bs1}\qquad |
320 @{thm[mode=Axiom] bs1[of _ "r\<^sub>2"]}\qquad |
181 @{thm[mode=Axiom] bs2}\qquad |
321 @{thm[mode=Axiom] bs2[of _ "r\<^sub>1"]}\qquad |
182 @{thm[mode=Axiom] bs3}\\ |
322 @{thm[mode=Axiom] bs3[of "bs\<^sub>1" "bs\<^sub>2"]}\\ |
183 @{thm[mode=Rule] bs4}\qquad |
323 @{thm[mode=Rule] bs4[of "r\<^sub>1" "r\<^sub>2" _ "r\<^sub>3"]}\qquad |
184 @{thm[mode=Rule] bs5}\\ |
324 @{thm[mode=Rule] bs5[of "r\<^sub>3" "r\<^sub>4" _ "r\<^sub>1"]}\\ |
185 @{thm[mode=Rule] bs6}\qquad |
325 @{thm[mode=Axiom] bs6}\qquad |
186 @{thm[mode=Rule] bs7}\\ |
326 @{thm[mode=Axiom] bs7}\\ |
187 @{thm[mode=Rule] bs8}\\ |
327 @{thm[mode=Rule] bs8[of "rs\<^sub>1" "rs\<^sub>2"]}\\ |
188 @{thm[mode=Axiom] ss1}\qquad |
328 @{thm[mode=Axiom] ss1}\qquad |
189 @{thm[mode=Rule] ss2}\qquad |
329 @{thm[mode=Rule] ss2[of "rs\<^sub>1" "rs\<^sub>2"]}\qquad |
190 @{thm[mode=Rule] ss3}\\ |
330 @{thm[mode=Rule] ss3[of "r\<^sub>1" "r\<^sub>2"]}\\ |
191 @{thm[mode=Axiom] ss4}\qquad |
331 @{thm[mode=Axiom] ss4}\qquad |
192 @{thm[mode=Axiom] ss5}\qquad |
332 @{thm[mode=Axiom] ss5[of "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\ |
193 @{thm[mode=Rule] ss6}\\ |
333 @{thm[mode=Rule] ss6[of "r\<^sub>1" "r\<^sub>2" "rs\<^sub>1" "rs\<^sub>2" "rs\<^sub>3"]}\\ |
194 \end{tabular} |
334 \end{tabular} |
195 \end{center} |
335 \end{center} |
196 \caption{???}\label{SimpRewrites} |
336 \caption{???}\label{SimpRewrites} |
197 \end{figure} |
337 \end{figure} |
198 *} |
338 *} |