|
532
|
1 |
% Chapter Template
|
|
|
2 |
|
|
|
3 |
% Main chapter title
|
|
538
|
4 |
\chapter{Bit-coded Algorithm of Sulzmann and Lu}
|
|
532
|
5 |
|
|
|
6 |
\label{Bitcoded1} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}
|
|
|
7 |
%Then we illustrate how the algorithm without bitcodes falls short for such aggressive
|
|
|
8 |
%simplifications and therefore introduce our version of the bitcoded algorithm and
|
|
|
9 |
%its correctness proof in
|
|
|
10 |
%Chapter 3\ref{Chapter3}.
|
|
564
|
11 |
In this chapter, we are going to describe the bit-coded algorithm
|
|
|
12 |
introduced by Sulzmann and Lu \parencite{Sulzmann2014} to address the growth problem of
|
|
|
13 |
regular expressions.
|
|
579
|
14 |
We have implemented their algorithm in Scala, and found out inefficiencies
|
|
|
15 |
in their algorithm such as de-duplication not working properly and redundant
|
|
|
16 |
fixpoint construction. Their algorithm is improved and verified with the help of
|
|
|
17 |
formal proofs.
|
|
580
|
18 |
\section{The Motivation Behind Using Bitcodes}
|
|
579
|
19 |
We first do a recap of what was going on
|
|
|
20 |
in the lexer algorithm in Chapter \ref{Inj},
|
|
|
21 |
\begin{center}
|
|
|
22 |
\begin{tabular}{lcl}
|
|
|
23 |
$\lexer \; r \; [] $ & $=$ & $\textit{if} \; (\nullable \; r)\; \textit{then}\; \Some(\mkeps \; r) \; \textit{else} \; \None$\\
|
|
|
24 |
$\lexer \; r \;c::s$ & $=$ & $\textit{case}\; (\lexer \; (r\backslash c) \; s) \;\textit{of}\; $\\
|
|
|
25 |
& & $\quad \phantom{\mid}\; \None \implies \None$\\
|
|
|
26 |
& & $\quad \mid \Some(v) \implies \Some(\inj \; r\; c\; v)$
|
|
|
27 |
\end{tabular}
|
|
|
28 |
\end{center}
|
|
|
29 |
\noindent
|
|
|
30 |
The algorithm recursively calls $\lexer$ on
|
|
|
31 |
each new character input,
|
|
|
32 |
and before starting a child call
|
|
|
33 |
it stores information of previous lexing steps
|
|
|
34 |
on a stack, in the form of regular expressions
|
|
|
35 |
and characters: $r_0$, $c_0$, $r_1$, $c_1$, etc.
|
|
|
36 |
Each descent into deeper recursive calls in $\lexer$
|
|
|
37 |
causes a new pair of $r_i, c_i$ to be pushed to the call stack.
|
|
580
|
38 |
\begin{figure}[H]
|
|
579
|
39 |
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
|
40 |
%\draw (-6,-6) grid (6,6);
|
|
|
41 |
\node [ circle ] (r) at (-6, 5) {$r$};
|
|
|
42 |
|
|
|
43 |
%\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
|
44 |
\node [circle, minimum size = 0.1, draw] (c1) at (-4, 5.4) {$c_1$};
|
|
|
45 |
%
|
|
|
46 |
%\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
|
47 |
\node [minimum size = 0.5, circle, draw] (r1) at (-2, 5) {$r_1$};
|
|
|
48 |
|
|
|
49 |
\node [minimum width = 2cm, rectangle, draw] (stack) at (0, 3) {Stack};
|
|
|
50 |
|
|
|
51 |
\path
|
|
|
52 |
(r)
|
|
|
53 |
edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
|
54 |
|
|
|
55 |
\path (r1)
|
|
|
56 |
edge [bend right, dashed] node {saved} (stack);
|
|
|
57 |
\path (c1)
|
|
|
58 |
edge [bend right, dashed] node {} (stack);
|
|
|
59 |
|
|
|
60 |
|
|
|
61 |
\end{tikzpicture}
|
|
|
62 |
\caption{First Derivative Taken}
|
|
|
63 |
\end{figure}
|
|
|
64 |
|
|
|
65 |
|
|
|
66 |
|
|
580
|
67 |
\begin{figure}[H]
|
|
579
|
68 |
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
|
69 |
%\draw (-6,-6) grid (6,6);
|
|
|
70 |
\node [ circle ] (r) at (-6, 5) {$r$};
|
|
|
71 |
|
|
|
72 |
%\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
|
73 |
\node [circle, minimum size = 0.1, ] (c1) at (-4, 5.4) {$c_1$};
|
|
|
74 |
%
|
|
|
75 |
%\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
|
76 |
\node [minimum size = 0.5, circle, ] (r1) at (-2, 5) {$r_1$};
|
|
|
77 |
|
|
|
78 |
|
|
|
79 |
\node [circle, minimum size = 0.1, draw] (c2) at (0, 5.4) {$c_2$};
|
|
|
80 |
%
|
|
|
81 |
%\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
|
82 |
\node [circle, draw] (r2) at (2, 5) {$r_2$};
|
|
|
83 |
\node [minimum width = 3cm, minimum height = 1cm, rectangle, draw] (stack) at (0, 2) {\large Stack};
|
|
|
84 |
|
|
|
85 |
\path
|
|
|
86 |
(r)
|
|
|
87 |
edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
|
88 |
|
|
|
89 |
\path (r2)
|
|
|
90 |
edge [bend right, dashed] node {} (stack);
|
|
|
91 |
\path (c2)
|
|
|
92 |
edge [bend right, dashed] node {} (stack);
|
|
|
93 |
|
|
|
94 |
\path (r1)
|
|
|
95 |
edge [] node {} (r2);
|
|
|
96 |
|
|
|
97 |
\end{tikzpicture}
|
|
|
98 |
\caption{Second Derivative Taken}
|
|
|
99 |
\end{figure}
|
|
|
100 |
\noindent
|
|
|
101 |
As the number of derivative steps increase,
|
|
|
102 |
the stack would increase:
|
|
|
103 |
|
|
580
|
104 |
\begin{figure}[H]
|
|
579
|
105 |
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
|
106 |
%\draw (-6,-6) grid (6,6);
|
|
|
107 |
\node [ circle ] (r) at (-6, 5) {$r$};
|
|
|
108 |
|
|
|
109 |
%\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
|
110 |
\node [circle, minimum size = 0.1, ] (c1) at (-4, 5.4) {$c_1$};
|
|
|
111 |
%
|
|
|
112 |
%\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
|
113 |
\node [minimum size = 0.5, circle, ] (r1) at (-2, 5) {$r_1$};
|
|
|
114 |
|
|
|
115 |
|
|
|
116 |
\node [circle, minimum size = 0.1, ] (c2) at (0, 5.4) {$c_2$};
|
|
|
117 |
%
|
|
|
118 |
%\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
|
119 |
\node [circle, ] (r2) at (2, 5) {$r_2$};
|
|
|
120 |
\node [minimum width = 4cm, minimum height = 2.5cm, rectangle, draw] (stack) at (0, 1) { \large Stack};
|
|
|
121 |
|
|
|
122 |
\node [] (ldots) at (3.5, 5) {};
|
|
|
123 |
%\node (6, 5) (rn) circle [radius = 0.5] {$r_n$};
|
|
|
124 |
|
|
|
125 |
\node [minimum size = 0.5, circle, ] (rn) at (6, 5) {};
|
|
|
126 |
|
|
|
127 |
\node (rldots) at ($(ldots)!.4!(rn)$) {\ldots};
|
|
|
128 |
|
|
|
129 |
\path
|
|
|
130 |
(r)
|
|
|
131 |
edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
|
132 |
|
|
|
133 |
\path (rldots)
|
|
|
134 |
edge [bend left, dashed] node {} (stack);
|
|
|
135 |
|
|
|
136 |
\path (r1)
|
|
|
137 |
edge [] node {} (r2);
|
|
|
138 |
|
|
|
139 |
\path (r2)
|
|
|
140 |
edge [] node {} (ldots);
|
|
|
141 |
\path (ldots)
|
|
|
142 |
edge [bend left, dashed] node {} (stack);
|
|
|
143 |
\path (5.03, 4.9)
|
|
|
144 |
edge [bend left, dashed] node {} (stack);
|
|
|
145 |
\end{tikzpicture}
|
|
|
146 |
\caption{More Derivatives Taken}
|
|
|
147 |
\end{figure}
|
|
580
|
148 |
|
|
579
|
149 |
|
|
580
|
150 |
\begin{figure}[H]
|
|
579
|
151 |
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
|
152 |
%\draw (-6,-6) grid (6,6);
|
|
|
153 |
\node [radius = 0.5, circle, draw] (r) at (-6, 5) {$r$};
|
|
|
154 |
|
|
|
155 |
%\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
|
156 |
\node [circle, minimum size = 0.1, draw] (c1) at (-4, 5.4) {$c_1$};
|
|
|
157 |
%
|
|
|
158 |
%\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
|
159 |
\node [minimum size = 0.5, circle, draw] (r1) at (-2, 5) {$r_1$};
|
|
|
160 |
%
|
|
|
161 |
%\node (0, 6) (c2) circle [radius = 0.3] {$c_2$};
|
|
|
162 |
\node [circle, minimum size = 0.1, draw] (c2) at (0, 5.4) {$c_2$};
|
|
|
163 |
%
|
|
|
164 |
%\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
|
165 |
\node [circle, draw] (r2) at (2, 5) {$r_2$};
|
|
|
166 |
%
|
|
|
167 |
%
|
|
|
168 |
\node [] (ldots) at (4.5, 5) {};
|
|
|
169 |
%\node (6, 5) (rn) circle [radius = 0.5] {$r_n$};
|
|
|
170 |
|
|
|
171 |
\node [minimum size = 0.5, circle, draw] (rn) at (6, 5) {$r_n$};
|
|
|
172 |
|
|
|
173 |
\node at ($(ldots)!.4!(rn)$) {\ldots};
|
|
|
174 |
|
|
|
175 |
|
|
|
176 |
|
|
|
177 |
|
|
|
178 |
\node [minimum size = 6cm, rectangle, draw] (stack) at (0, 0) {\Huge Stack};
|
|
|
179 |
|
|
|
180 |
\path
|
|
|
181 |
(r)
|
|
|
182 |
edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
|
183 |
\path
|
|
|
184 |
(r1)
|
|
|
185 |
edge [] node {} (r2);
|
|
|
186 |
\path (r2)
|
|
|
187 |
edge [] node {} (ldots);
|
|
|
188 |
\path (r)
|
|
|
189 |
edge [dashed, bend right] node {} (stack);
|
|
|
190 |
|
|
|
191 |
\path (r1)
|
|
|
192 |
edge [dashed, ] node {} (stack);
|
|
|
193 |
|
|
|
194 |
\path (c1)
|
|
|
195 |
edge [dashed, bend right] node {} (stack);
|
|
|
196 |
|
|
|
197 |
\path (c2)
|
|
|
198 |
edge [dashed] node {} (stack);
|
|
|
199 |
\path (4.5, 5)
|
|
|
200 |
edge [dashed, bend left] node {} (stack);
|
|
|
201 |
\path (4.9, 5)
|
|
|
202 |
edge [dashed, bend left] node {} (stack);
|
|
|
203 |
\path (5.3, 5)
|
|
|
204 |
edge [dashed, bend left] node {} (stack);
|
|
|
205 |
\path (r2)
|
|
|
206 |
edge [dashed, ] node {} (stack);
|
|
|
207 |
\path (rn)
|
|
|
208 |
edge [dashed, bend left] node {} (stack);
|
|
|
209 |
\end{tikzpicture}
|
|
580
|
210 |
\caption{Before Injection Phase Starts}
|
|
|
211 |
\end{figure}
|
|
|
212 |
|
|
|
213 |
|
|
|
214 |
\noindent
|
|
|
215 |
After all derivatives have been taken, the stack grows to a maximum size
|
|
|
216 |
and the pair of regular expressions and characters $r_i, c_{i+1}$
|
|
|
217 |
are then popped out and used in the injection phase.
|
|
|
218 |
|
|
|
219 |
|
|
|
220 |
|
|
|
221 |
\begin{figure}[H]
|
|
|
222 |
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
|
223 |
%\draw (-6,-6) grid (6,6);
|
|
|
224 |
\node [radius = 0.5, circle, ] (r) at (-6, 5) {$r$};
|
|
|
225 |
|
|
|
226 |
%\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
|
227 |
\node [circle, minimum size = 0.1, ] (c1) at (-4, 5.4) {$c_1$};
|
|
579
|
228 |
%
|
|
580
|
229 |
%\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
|
230 |
\node [minimum size = 0.5, circle, ] (r1) at (-2, 5) {$r_1$};
|
|
579
|
231 |
%
|
|
580
|
232 |
%\node (0, 6) (c2) circle [radius = 0.3] {$c_2$};
|
|
|
233 |
\node [circle, minimum size = 0.1, ] (c2) at (0, 5.4) {$c_2$};
|
|
579
|
234 |
%
|
|
580
|
235 |
%\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
|
236 |
\node [circle, ] (r2) at (2, 5) {$r_2$};
|
|
579
|
237 |
%
|
|
|
238 |
%
|
|
580
|
239 |
\node [] (ldots) at (4.5, 5) {};
|
|
|
240 |
%\node (6, 5) (rn) circle [radius = 0.5] {$r_n$};
|
|
|
241 |
|
|
|
242 |
\node [minimum size = 0.5, circle, ] (rn) at (6, 5) {$r_n$};
|
|
|
243 |
|
|
|
244 |
\node at ($(ldots)!.4!(rn)$) {\ldots};
|
|
|
245 |
|
|
|
246 |
\node [minimum size = 0.5, circle, ] (vn) at (6, -5) {$v_n$};
|
|
|
247 |
|
|
|
248 |
\node [] (ldots2) at (3.5, -5) {};
|
|
|
249 |
|
|
|
250 |
\node [minimum size = 0.5, circle, ] (v2) at (2, -5) {$v_2$};
|
|
|
251 |
|
|
|
252 |
\node at ($(ldots2)!.4!(v2)$) {\ldots};
|
|
|
253 |
|
|
|
254 |
|
|
|
255 |
\node [circle, ] (v1) at (-2, -5) {$v_1$};
|
|
|
256 |
|
|
|
257 |
\node [radius = 0.5, circle, ] (v) at (-6, -5) {$v$};
|
|
|
258 |
|
|
|
259 |
\node [minimum size = 6cm, rectangle, draw] (stack) at (0, 0) {\Huge Stack};
|
|
|
260 |
|
|
|
261 |
\path
|
|
|
262 |
(r)
|
|
|
263 |
edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
|
264 |
\path
|
|
|
265 |
(r1)
|
|
|
266 |
edge [] node {} (r2);
|
|
|
267 |
\path (r2)
|
|
|
268 |
edge [] node {} (ldots);
|
|
|
269 |
\path (rn)
|
|
|
270 |
edge [] node {$\mkeps$} (vn);
|
|
|
271 |
\path (vn)
|
|
|
272 |
edge [] node {} (ldots2);
|
|
|
273 |
\path (v2)
|
|
|
274 |
edge [] node {$\inj \; r_1 \; c_2\;v_2$} (v1);
|
|
|
275 |
|
|
|
276 |
\path (v1)
|
|
|
277 |
edge [] node {$\inj \; r \; c_1 \; v_1$} (v);
|
|
|
278 |
|
|
|
279 |
\path (stack)
|
|
|
280 |
edge [dashed] node {} (-4.2, -5.2);
|
|
|
281 |
\path (stack)
|
|
|
282 |
edge [dashed] node {} (-4, -5.2);
|
|
|
283 |
\path (stack)
|
|
|
284 |
edge [dashed] node {} (-0.1, -5.2);
|
|
|
285 |
\path (stack)
|
|
|
286 |
edge [dashed] node {} (0.2, -5.26);
|
|
|
287 |
\path (stack)
|
|
|
288 |
edge [dashed] node {} (3.2, -5);
|
|
|
289 |
\path (stack)
|
|
|
290 |
edge [dashed] node {} (2.7, -5);
|
|
|
291 |
\path (stack)
|
|
|
292 |
edge [dashed] node {} (3.7, -5);
|
|
|
293 |
\end{tikzpicture}
|
|
|
294 |
\caption{Stored $r_i, c_{i+1}$ Used by $\inj$}
|
|
|
295 |
\end{figure}
|
|
|
296 |
\noindent
|
|
|
297 |
Storing all $r_i, c_{i+1}$ pairs recursively
|
|
|
298 |
allows the algorithm to work in an elegant way, at the expense of
|
|
|
299 |
storing quite a bit of verbose information.
|
|
|
300 |
The stack seems to grow at least quadratically fast with respect
|
|
|
301 |
to the input (not taking into account the size bloat of $r_i$),
|
|
|
302 |
which can be inefficient and prone to stack overflow.
|
|
|
303 |
\section{Bitcoded Algorithm}
|
|
|
304 |
To address this,
|
|
|
305 |
Sulzmann and Lu chose to define a new datatype
|
|
|
306 |
called \emph{annotated regular expression},
|
|
|
307 |
which condenses all the partial lexing information
|
|
|
308 |
(that was originally stored in $r_i, c_{i+1}$ pairs)
|
|
|
309 |
into bitcodes.
|
|
|
310 |
Annotated regular expressions
|
|
|
311 |
are defined as the following
|
|
|
312 |
Isabelle datatype \footnote{ We use subscript notation to indicate
|
|
|
313 |
that the bitcodes are auxiliary information that do not
|
|
|
314 |
interfere with the structure of the regular expressions }:
|
|
|
315 |
\begin{center}
|
|
|
316 |
\begin{tabular}{lcl}
|
|
|
317 |
$\textit{a}$ & $::=$ & $\ZERO$\\
|
|
|
318 |
& $\mid$ & $_{bs}\ONE$\\
|
|
|
319 |
& $\mid$ & $_{bs}{\bf c}$\\
|
|
|
320 |
& $\mid$ & $_{bs}\sum\,as$\\
|
|
|
321 |
& $\mid$ & $_{bs}a_1\cdot a_2$\\
|
|
|
322 |
& $\mid$ & $_{bs}a^*$
|
|
|
323 |
\end{tabular}
|
|
|
324 |
\end{center}
|
|
|
325 |
\noindent
|
|
|
326 |
where $bs$ stands for bit-codes, $a$ for $\mathbf{a}$nnotated regular
|
|
|
327 |
expressions and $as$ for lists of annotated regular expressions.
|
|
|
328 |
The alternative constructor, written, $\sum$, has been generalised to
|
|
|
329 |
accept a list of annotated regular expressions rather than just two.
|
|
|
330 |
Why is it generalised? This is because when we open up nested
|
|
|
331 |
alternatives, there could be more than two elements at the same level
|
|
|
332 |
after de-duplication, which can no longer be stored in a binary
|
|
|
333 |
constructor.
|
|
|
334 |
Bits and bitcodes (lists of bits) are defined as:
|
|
|
335 |
\begin{center}
|
|
|
336 |
$b ::= S \mid Z \qquad
|
|
|
337 |
bs ::= [] \mid b::bs
|
|
|
338 |
$
|
|
|
339 |
\end{center}
|
|
|
340 |
\noindent
|
|
|
341 |
We use $S$ and $Z$ rather than $1$ and $0$ is to avoid
|
|
|
342 |
confusion with the regular expressions $\ZERO$ and $\ONE$.
|
|
|
343 |
The idea is to use the attached bitcodes
|
|
|
344 |
to indicate which choice was made at a certain point
|
|
|
345 |
during lexing.
|
|
|
346 |
For example,
|
|
|
347 |
$(_{Z}a+_{S}b) \backslash a$ gives us
|
|
|
348 |
$_{Z}\ONE + \ZERO$, this $Z$ bitcode will
|
|
|
349 |
later be used to decode that a left branch was
|
|
|
350 |
selected at the time when the part $a+b$ is being taken
|
|
|
351 |
derivative of.
|
|
|
352 |
\subsection{A Bird's Eye View of the Bit-coded Lexer}
|
|
|
353 |
Before we give out the rest of the functions and definitions
|
|
|
354 |
related to our
|
|
|
355 |
$\blexer$ (\emph{b}-itcoded lexer), we first provide a high-level
|
|
|
356 |
view of the algorithm, so the reader does not get lost in
|
|
|
357 |
the details.
|
|
|
358 |
\begin{figure}[H]
|
|
|
359 |
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
|
360 |
%\draw (-6,-6) grid (6,6);
|
|
|
361 |
|
|
|
362 |
\node [circle, draw] (r0) at (-6, 2) {$r$};
|
|
|
363 |
|
|
|
364 |
\node [radius = 0.5, circle, draw] (r) at (-6, 5) {$_{bs}a$};
|
|
|
365 |
\path (r0)
|
|
|
366 |
edge [] node {$\internalise$} (r);
|
|
|
367 |
%\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
|
368 |
\node [circle, minimum size = 0.1, draw] (c1) at (-4, 5.4) {$c_1$};
|
|
579
|
369 |
%
|
|
580
|
370 |
%\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
|
371 |
\node [minimum size = 1.0cm, circle, draw] (r1) at (-2, 5) {$_{bs_1}a_1$};
|
|
|
372 |
%
|
|
|
373 |
%\node (0, 6) (c2) circle [radius = 0.3] {$c_2$};
|
|
|
374 |
\node [circle, minimum size = 0.1, draw] (c2) at (0, 5.4) {$c_2$};
|
|
|
375 |
%
|
|
|
376 |
%\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
|
377 |
\node [circle, draw, minimum size = 1.4cm] (r2) at (2, 5) {$_{bs_2}a_2$};
|
|
|
378 |
%
|
|
|
379 |
%
|
|
|
380 |
\node [] (ldots) at (4.5, 5) {};
|
|
|
381 |
%\node (6, 5) (rn) circle [radius = 0.5] {$r_n$};
|
|
|
382 |
|
|
|
383 |
\node [minimum size = 2.2cm, circle, draw] (rn) at (6, 5) {$_{bs_n}a_n$};
|
|
|
384 |
|
|
|
385 |
\node at ($(ldots)!.1!(rn)$) {\ldots};
|
|
|
386 |
|
|
|
387 |
\node [minimum size = 0.5, circle, ] (v) at (6, 2) {$v$};
|
|
|
388 |
|
|
|
389 |
%\node [] (v2) at (4, -5) {};
|
|
|
390 |
%
|
|
|
391 |
%\node [draw, cross out] (ldots2) at (5, -5) {};
|
|
579
|
392 |
%
|
|
580
|
393 |
%\node at ($(ldots2)!.4!(v2)$) {\ldots};
|
|
|
394 |
|
|
|
395 |
|
|
|
396 |
\node [align = center] (decode) at (6.6, 3.2) {$\bmkeps$\\$\decode$};
|
|
|
397 |
|
|
|
398 |
\path (c1)
|
|
|
399 |
edge [dashed, bend left] node {} (r0);
|
|
|
400 |
|
|
|
401 |
\path (c2)
|
|
|
402 |
edge [dashed, bend left] node {} (r0);
|
|
|
403 |
|
|
|
404 |
\path (r1)
|
|
|
405 |
edge [dashed, bend right] node {} (r2);
|
|
|
406 |
|
|
|
407 |
|
|
|
408 |
\path
|
|
|
409 |
(r)
|
|
|
410 |
edge [dashed, bend right] node[left] {} (r1);
|
|
|
411 |
|
|
|
412 |
\path
|
|
|
413 |
(r)
|
|
|
414 |
edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
|
415 |
|
|
|
416 |
\path
|
|
|
417 |
(r1)
|
|
|
418 |
edge [] node {} (r2);
|
|
|
419 |
\path (r2)
|
|
|
420 |
edge [] node {} (ldots);
|
|
|
421 |
\path (rn)
|
|
|
422 |
edge [] node {} (v);
|
|
|
423 |
|
|
|
424 |
\path (r0)
|
|
|
425 |
edge [dashed, bend right] node {} (decode);
|
|
|
426 |
%\path (v)
|
|
|
427 |
%edge [] node {} (ldots2);
|
|
579
|
428 |
|
|
|
429 |
|
|
|
430 |
|
|
580
|
431 |
\end{tikzpicture}
|
|
|
432 |
\caption{Bird's Eye View of $\blexer$}
|
|
|
433 |
\end{figure}
|
|
|
434 |
\noindent
|
|
|
435 |
The plain regular expressions
|
|
|
436 |
are first ``lifted'' to an annotated regular expression,
|
|
|
437 |
with the function called \emph{internalise}.
|
|
|
438 |
Then the annotated regular expression $_{bs}a$ will
|
|
|
439 |
go through successive derivatives with respect
|
|
|
440 |
to the input stream of characters $c_1, c_2$ etc.
|
|
|
441 |
Each time a derivative is taken, the bitcodes
|
|
|
442 |
are moved around, discarded or augmented together
|
|
|
443 |
with the regular expression they are attached to.
|
|
|
444 |
After all input has been consumed, the
|
|
|
445 |
bitcodes are collected by $\bmkeps$,
|
|
|
446 |
which traverses the nullable part of the regular expression
|
|
|
447 |
and collect the bitcodes along the way.
|
|
|
448 |
The collected bitcodes are then $\decode$d with the guidance
|
|
|
449 |
of the input regular expression $r$.
|
|
|
450 |
The most notable improvements of $\blexer$
|
|
|
451 |
over $\lexer$ are
|
|
|
452 |
\begin{itemize}
|
|
|
453 |
\item
|
|
|
454 |
|
|
|
455 |
An absence of the second injection phase.
|
|
|
456 |
\item
|
|
|
457 |
One need not store each pair of the
|
|
|
458 |
intermediate regular expressions $_{bs_i}a_i$ and $c_{i+1}$.
|
|
|
459 |
The previous annotated regular expression $_{bs_i}a_i$'s information is passed
|
|
|
460 |
on without loss to its successor $_{bs_{i+1}}a_{i+1}$,
|
|
|
461 |
and $c_{i+1}$'s already contained in the strings in $L\;r$ \footnote{
|
|
|
462 |
which can be easily recovered if we decode in the correct order}.
|
|
|
463 |
\item
|
|
|
464 |
The simplification works much better--one can maintain correctness
|
|
|
465 |
while applying quite strong simplifications, as we shall wee.
|
|
|
466 |
\end{itemize}
|
|
|
467 |
\noindent
|
|
|
468 |
In the next section we will
|
|
|
469 |
give the operations needed in $\blexer$,
|
|
|
470 |
with some remarks on the idea behind their definitions.
|
|
|
471 |
\subsection{Operations in $\textit{Blexer}$}
|
|
|
472 |
The first operation we define related to bit-coded regular expressions
|
|
|
473 |
is how we move bits to the inside of regular expressions.
|
|
|
474 |
Called $\fuse$, this operation attaches bit-codes
|
|
|
475 |
to the front of an annotated regular expression:
|
|
|
476 |
\begin{center}
|
|
|
477 |
\begin{tabular}{lcl}
|
|
|
478 |
$\textit{fuse}\;bs \; \ZERO$ & $\dn$ & $\ZERO$\\
|
|
|
479 |
$\textit{fuse}\;bs\; _{bs'}\ONE$ & $\dn$ &
|
|
|
480 |
$_{bs @ bs'}\ONE$\\
|
|
|
481 |
$\textit{fuse}\;bs\;_{bs'}{\bf c}$ & $\dn$ &
|
|
|
482 |
$_{bs@bs'}{\bf c}$\\
|
|
|
483 |
$\textit{fuse}\;bs\,_{bs'}\sum\textit{as}$ & $\dn$ &
|
|
|
484 |
$_{bs@bs'}\sum\textit{as}$\\
|
|
|
485 |
$\textit{fuse}\;bs\; _{bs'}a_1\cdot a_2$ & $\dn$ &
|
|
|
486 |
$_{bs@bs'}a_1 \cdot a_2$\\
|
|
|
487 |
$\textit{fuse}\;bs\,_{bs'}a^*$ & $\dn$ &
|
|
|
488 |
$_{bs @ bs'}a^*$
|
|
|
489 |
\end{tabular}
|
|
|
490 |
\end{center}
|
|
|
491 |
|
|
|
492 |
\noindent
|
|
|
493 |
With \emph{fuse} we are able to define the $\internalise$ function
|
|
|
494 |
that translates a ``standard'' regular expression into an
|
|
|
495 |
annotated regular expression.
|
|
|
496 |
This function will be applied before we start
|
|
|
497 |
with the derivative phase of the algorithm.
|
|
|
498 |
|
|
|
499 |
\begin{center}
|
|
|
500 |
\begin{tabular}{lcl}
|
|
|
501 |
$(\ZERO)^\uparrow$ & $\dn$ & $\ZERO$\\
|
|
|
502 |
$(\ONE)^\uparrow$ & $\dn$ & $_{[]}\ONE$\\
|
|
|
503 |
$(c)^\uparrow$ & $\dn$ & $_{[]}{\bf c}$\\
|
|
|
504 |
$(r_1 + r_2)^\uparrow$ & $\dn$ &
|
|
|
505 |
$_{[]}\sum[\textit{fuse}\,[Z]\,r_1^\uparrow,\,
|
|
|
506 |
\textit{fuse}\,[S]\,r_2^\uparrow]$\\
|
|
|
507 |
$(r_1\cdot r_2)^\uparrow$ & $\dn$ &
|
|
|
508 |
$_{[]}r_1^\uparrow \cdot r_2^\uparrow$\\
|
|
|
509 |
$(r^*)^\uparrow$ & $\dn$ &
|
|
|
510 |
$_{[]}(r^\uparrow)^*$\\
|
|
|
511 |
\end{tabular}
|
|
|
512 |
\end{center}
|
|
|
513 |
\noindent
|
|
|
514 |
We use an up arrow with postfix notation
|
|
|
515 |
to denote this operation
|
|
|
516 |
for convenience.
|
|
|
517 |
The opposite of $\textit{internalise}$ is
|
|
|
518 |
$\erase$, where all the bit-codes are removed,
|
|
|
519 |
and the alternative operator $\sum$ for annotated
|
|
|
520 |
regular expressions is transformed to the binary version
|
|
|
521 |
in plain regular expressions.
|
|
|
522 |
\begin{center}
|
|
|
523 |
\begin{tabular}{lcl}
|
|
|
524 |
$\ZERO_\downarrow$ & $\dn$ & $\ZERO$\\
|
|
|
525 |
$( _{bs}\ONE )_\downarrow$ & $\dn$ & $\ONE$\\
|
|
|
526 |
$( _{bs}\mathbf{c} )_\downarrow$ & $\dn$ & $\mathbf{c}$\\
|
|
|
527 |
$( _{bs} a_1 \cdot a_2 )_\downarrow$ & $\dn$ &
|
|
|
528 |
$ (a_1) _\downarrow \cdot (a_2) _\downarrow$\\
|
|
|
529 |
$( _{bs} [])_\downarrow $ & $\dn$ & $\ZERO $\\
|
|
|
530 |
$( _{bs} [a] )_\downarrow$ & $\dn$ & $a_\downarrow$\\
|
|
|
531 |
$_{bs} \sum [a_1, \; a_2]$ & $\dn$ & $ (a_1) _\downarrow + ( a_2 ) _\downarrow $\\
|
|
|
532 |
$(_{bs} \sum (a :: as))_\downarrow$ & $\dn$ & $ a_\downarrow + \; (_{[]} \sum as)_\downarrow$\\
|
|
|
533 |
$( _{bs} a^* )_\downarrow$ & $\dn$ & $(a_\downarrow)^*$
|
|
|
534 |
\end{tabular}
|
|
|
535 |
\end{center}
|
|
|
536 |
\noindent
|
|
|
537 |
We also abbreviate the $\erase\; a$ operation
|
|
|
538 |
as $a_\downarrow$, for conciseness.
|
|
|
539 |
|
|
|
540 |
Testing whether an annotated regular expression
|
|
|
541 |
contains the empty string in its lauguage requires
|
|
|
542 |
a dedicated function $\bnullable$.
|
|
|
543 |
$\bnullable$ simply calls $\erase$ before $\nullable$.
|
|
|
544 |
\begin{definition}
|
|
|
545 |
$\bnullable \; a \dn \nullable \; (a_\downarrow)$
|
|
|
546 |
\end{definition}
|
|
|
547 |
The function for collecting
|
|
|
548 |
bitcodes from a
|
|
|
549 |
(b)nullable regular expression is called $\bmkeps$.
|
|
|
550 |
$\bmkeps$ is a variation of the $\textit{mkeps}$ function,
|
|
|
551 |
which follows the path $\mkeps$ takes to traverse the
|
|
|
552 |
$\nullable$ branches when visiting a regular expression,
|
|
|
553 |
but gives back bitcodes instead of a value.
|
|
|
554 |
\begin{center}
|
|
|
555 |
\begin{tabular}{lcl}
|
|
|
556 |
$\textit{bmkeps}\,(_{bs}\ONE)$ & $\dn$ & $bs$\\
|
|
|
557 |
$\textit{bmkeps}\,(_{bs}\sum a::\textit{as})$ & $\dn$ &
|
|
|
558 |
$\textit{if}\;\textit{bnullable}\,a$\\
|
|
|
559 |
& &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\
|
|
|
560 |
& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{[]}\sum \textit{as})$\\
|
|
|
561 |
$\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ &
|
|
|
562 |
$bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
|
|
|
563 |
$\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ &
|
|
|
564 |
$bs \,@\, [Z]$
|
|
|
565 |
\end{tabular}
|
|
|
566 |
\end{center}
|
|
|
567 |
\noindent
|
|
|
568 |
$\bmkeps$ retrieves the value $v$'s
|
|
|
569 |
information in the format
|
|
|
570 |
of bitcodes, by travelling along the
|
|
|
571 |
path of the regular expression that corresponds to a POSIX match,
|
|
|
572 |
collecting all the bitcodes, and attaching $S$ to indicate the end of star
|
|
|
573 |
iterations. \\
|
|
|
574 |
The bitcodes extracted by $\bmkeps$ need to be
|
|
|
575 |
$\decode$d (with the guidance of a plain regular expression):
|
|
|
576 |
%\begin{definition}[Bitdecoding of Values]\mbox{}
|
|
|
577 |
\begin{center}
|
|
|
578 |
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
|
|
|
579 |
$\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
|
|
|
580 |
$\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
|
|
|
581 |
$\textit{decode}'\,(Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
|
|
|
582 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
|
|
|
583 |
(\Left\,v, bs_1)$\\
|
|
|
584 |
$\textit{decode}'\,(S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
|
|
|
585 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
|
|
|
586 |
(\Right\,v, bs_1)$\\
|
|
|
587 |
$\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
|
|
|
588 |
$\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
|
|
|
589 |
& & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
|
|
|
590 |
& & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
|
|
|
591 |
$\textit{decode}'\,(Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
|
|
|
592 |
$\textit{decode}'\,(S\!::\!bs)\,(r^*)$ & $\dn$ &
|
|
|
593 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
|
|
|
594 |
& & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
|
|
|
595 |
& & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
|
|
|
596 |
|
|
|
597 |
$\textit{decode}\,bs\,r$ & $\dn$ &
|
|
|
598 |
$\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
|
|
|
599 |
& & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
|
|
|
600 |
\textit{else}\;\textit{None}$
|
|
|
601 |
\end{tabular}
|
|
|
602 |
\end{center}
|
|
537
|
603 |
\noindent
|
|
580
|
604 |
The function $\decode'$ returns a pair consisting of
|
|
|
605 |
a partially decoded value and some leftover bit list that cannot
|
|
|
606 |
be decide yet.
|
|
|
607 |
The function $\decode'$ succeeds if the left-over
|
|
|
608 |
bit-sequence is empty.
|
|
|
609 |
$\decode$ is terminating as $\decode'$ is terminating.
|
|
|
610 |
$\decode'$ is terminating
|
|
|
611 |
because at least one of $\decode'$'s parameters will go down in terms
|
|
|
612 |
of size.\\
|
|
|
613 |
The reverse operation of $\decode$ is $\code$.
|
|
|
614 |
$\textit{code}$ encodes a value into a bitcode by converting
|
|
|
615 |
$\Left$ into $Z$, $\Right$ into $S$, and marks the start of any non-empty
|
|
|
616 |
star iteration by $S$. The border where a star iteration
|
|
|
617 |
terminates is marked by $Z$.
|
|
|
618 |
This coding is lossy, as it throws away the information about
|
|
|
619 |
characters, and does not encode the ``boundary'' between two
|
|
|
620 |
sequence values. Moreover, with only the bitcode we cannot even tell
|
|
|
621 |
whether the $S$s and $Z$s are for $\Left/\Right$ or $\Stars$.
|
|
|
622 |
\begin{center}
|
|
|
623 |
\begin{tabular}{lcl}
|
|
|
624 |
$\textit{code}(\Empty)$ & $\dn$ & $[]$\\
|
|
|
625 |
$\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
|
|
|
626 |
$\textit{code}(\Left\,v)$ & $\dn$ & $Z :: code(v)$\\
|
|
|
627 |
$\textit{code}(\Right\,v)$ & $\dn$ & $S :: code(v)$\\
|
|
|
628 |
$\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
|
|
|
629 |
$\textit{code}(\Stars\,[])$ & $\dn$ & $[Z]$\\
|
|
|
630 |
$\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $S :: code(v) \;@\;
|
|
|
631 |
code(\Stars\,vs)$
|
|
|
632 |
\end{tabular}
|
|
|
633 |
\end{center}
|
|
|
634 |
\noindent
|
|
|
635 |
Assume we have a value $v$ and regular expression $r$
|
|
|
636 |
with $\vdash v:r$,
|
|
|
637 |
then we have the property that $\decode$ and $\code$ are
|
|
|
638 |
reverse operations of one another:
|
|
|
639 |
\begin{lemma}
|
|
|
640 |
\[If \vdash v : r \; then \;\decode \; (\code \; v) \; r = \textit{Some}(v) \]
|
|
|
641 |
\end{lemma}
|
|
|
642 |
\begin{proof}
|
|
|
643 |
By proving a more general version of the lemma, on $\decode'$:
|
|
|
644 |
\[\vdash v : r \implies \decode' \; ((\code \; v) @ ds) \; r = (v, ds) \]
|
|
|
645 |
Then setting $ds$ to be $[]$ and unfolding $\decode$ definition,
|
|
|
646 |
we obtain the property.
|
|
|
647 |
\end{proof}
|
|
|
648 |
\noindent
|
|
|
649 |
Now we give out the central part of this lexing algorithm,
|
|
|
650 |
the $\bder$ function (stands for \emph{b}itcoded-derivative):
|
|
|
651 |
\begin{center}
|
|
|
652 |
\begin{tabular}{@{}lcl@{}}
|
|
|
653 |
$(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
654 |
$(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
655 |
$(_{bs}{\bf d})\,\backslash c$ & $\dn$ &
|
|
|
656 |
$\textit{if}\;c=d\; \;\textit{then}\;
|
|
|
657 |
_{bs}\ONE\;\textit{else}\;\ZERO$\\
|
|
|
658 |
$(_{bs}\sum \;\textit{as})\,\backslash c$ & $\dn$ &
|
|
|
659 |
$_{bs}\sum\;(\textit{map} \; (\_\backslash c) \; as )$\\
|
|
|
660 |
$(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ &
|
|
|
661 |
$\textit{if}\;\textit{bnullable}\,a_1$\\
|
|
|
662 |
& &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\
|
|
|
663 |
& &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\
|
|
|
664 |
& &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\
|
|
|
665 |
$(_{bs}a^*)\,\backslash c$ & $\dn$ &
|
|
|
666 |
$_{bs}(\textit{fuse}\, [Z] \; r\,\backslash c)\cdot
|
|
|
667 |
(_{[]}r^*))$
|
|
|
668 |
\end{tabular}
|
|
|
669 |
\end{center}
|
|
|
670 |
\noindent
|
|
|
671 |
For most time we use the infix notation $(\_\backslash\_)$
|
|
|
672 |
to mean $\bder$ for brevity when
|
|
|
673 |
there is no danger of confusion with derivatives on plain regular expressions.
|
|
|
674 |
For example, we write $( _{[]}r^* ) \backslash c$ instead of $\bder \;c \; _{[]}r^*$,
|
|
|
675 |
as the bitcodes at the front of $r^*$ indicates that it is
|
|
|
676 |
a bit-coded regular expression, not a plain one.\\
|
|
|
677 |
$\bder$ tells us how regular expressions can be recursively traversed,
|
|
|
678 |
where the bitcodes are augmented and carried around
|
|
|
679 |
when a derivative is taken.
|
|
|
680 |
We give the intuition behind some of the more involved cases in
|
|
|
681 |
$\bder$. \\
|
|
|
682 |
For example,
|
|
|
683 |
in the \emph{star} case,
|
|
|
684 |
a derivative on $_{bs}a^*$ means
|
|
|
685 |
that one more star iteratoin needs to be taken.
|
|
|
686 |
we need to unfold it into a sequence,
|
|
|
687 |
and attach an additional bit $Z$ to the front of $r \backslash c$
|
|
|
688 |
as a record to indicate one new star iteration is unfolded.
|
|
|
689 |
|
|
|
690 |
\noindent
|
|
|
691 |
\begin{center}
|
|
|
692 |
\begin{tabular}{@{}lcl@{}}
|
|
|
693 |
$(_{bs}a^*)\,\backslash c$ & $\dn$ &
|
|
|
694 |
$_{bs}(\underbrace{\textit{fuse}\, [Z] \; a\,\backslash c}_{\text{One more iteration}})\cdot
|
|
|
695 |
(_{[]}a^*))$
|
|
|
696 |
\end{tabular}
|
|
|
697 |
\end{center}
|
|
|
698 |
|
|
|
699 |
\noindent
|
|
|
700 |
This information will be recovered later by the $\decode$ function.
|
|
|
701 |
The intuition is that the bit $Z$ will be decoded at the right location,
|
|
|
702 |
because we accumulate bits from left to right (a rigorous proof will be given
|
|
|
703 |
later).
|
|
|
704 |
|
|
|
705 |
%\begin{tikzpicture}[ > = stealth, % arrow head style
|
|
|
706 |
% shorten > = 1pt, % don't touch arrow head to node
|
|
|
707 |
% semithick % line style
|
|
|
708 |
% ]
|
|
|
709 |
%
|
|
|
710 |
% \tikzstyle{every state}=[
|
|
|
711 |
% draw = black,
|
|
|
712 |
% thin,
|
|
|
713 |
% fill = cyan!29,
|
|
|
714 |
% minimum size = 7mm
|
|
|
715 |
% ]
|
|
|
716 |
% \begin{scope}[node distance=1cm and 0cm, every node/.style=state]
|
|
|
717 |
% \node (k) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
|
718 |
% {$bs$
|
|
|
719 |
% \nodepart{two} $a^*$ };
|
|
|
720 |
% \node (l) [below =of k, rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
|
721 |
% { $bs$ + [Z]
|
|
|
722 |
% \nodepart{two} $(a\backslash c )\cdot a^*$ };
|
|
|
723 |
% \end{scope}
|
|
|
724 |
% \path[->]
|
|
|
725 |
% (k) edge (l);
|
|
|
726 |
%\end{tikzpicture}
|
|
|
727 |
%
|
|
|
728 |
%Pictorially the process looks like below.
|
|
|
729 |
%Like before, the red region denotes
|
|
|
730 |
%previous lexing information (stored as bitcodes in $bs$).
|
|
|
731 |
|
|
|
732 |
%\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
|
733 |
% \begin{scope}[node distance=1cm]
|
|
|
734 |
% \node (a) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
|
735 |
% {$bs$
|
|
|
736 |
% \nodepart{two} $a^*$ };
|
|
|
737 |
% \node (b) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
|
738 |
% { $bs$ + [Z]
|
|
|
739 |
% \nodepart{two} $(a\backslash c )\cdot a^*$ };
|
|
|
740 |
%%\caption{term 1 \ref{term:1}'s matching configuration}
|
|
|
741 |
% \end{scope}
|
|
|
742 |
%\end{tikzpicture}
|
|
|
743 |
|
|
|
744 |
\noindent
|
|
|
745 |
Another place the $\bder$ function differs
|
|
|
746 |
from derivatives on plain regular expressions
|
|
|
747 |
is the sequence case:
|
|
|
748 |
\begin{center}
|
|
|
749 |
\begin{tabular}{@{}lcl@{}}
|
|
|
750 |
|
|
|
751 |
$(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ &
|
|
|
752 |
$\textit{if}\;\textit{bnullable}\,a_1$\\
|
|
|
753 |
& &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\
|
|
|
754 |
& &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\
|
|
|
755 |
& &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$
|
|
|
756 |
\end{tabular}
|
|
|
757 |
\end{center}
|
|
|
758 |
\noindent
|
|
|
759 |
The difference is that (when $a_1$ is $\bnullable$)
|
|
|
760 |
we use $\bmkeps$ to store the lexing information
|
|
|
761 |
in $a_1$ before collapsing
|
|
|
762 |
it (as it has been fully matched by string prior to $c$),
|
|
|
763 |
and attach the collected bit-codes to the front of $a_2$
|
|
|
764 |
before throwing away $a_1$. We assume that $\bmkeps$
|
|
|
765 |
correctly extracts the bitcode for how $a_1$
|
|
|
766 |
matches the string prior to $c$ (more on this later).
|
|
|
767 |
The bitsequence $\textit{bs}$ which was initially
|
|
|
768 |
attached to the first element of the sequence
|
|
|
769 |
$a_1 \cdot a_2$, has now been
|
|
|
770 |
elevated to the top level of the $\sum$ constructor.
|
|
|
771 |
This is because this piece of information will be needed
|
|
|
772 |
whichever way the sequence is matched,
|
|
|
773 |
regardless of whether $c$ belongs to $a_1$ or $a_2$.
|
|
|
774 |
|
|
|
775 |
In the injection-based lexer, $r_1$ is immediately thrown away in
|
|
|
776 |
subsequent derivatives on the right branch (when $r_1$ is $\nullable$),
|
|
|
777 |
depite $r_1$ potentially storing information of previous matches:
|
|
|
778 |
\begin{center}
|
|
|
779 |
$(r_1 \cdot r_2 )\backslash c = (r_1 \backslash c) \cdot r_2 + r_2 \backslash c$
|
|
|
780 |
\end{center}
|
|
|
781 |
\noindent
|
|
|
782 |
this loss of information makes it necessary
|
|
|
783 |
to store on stack all the regular expressions'
|
|
|
784 |
``snapshots'' before they were
|
|
|
785 |
taken derivative of.
|
|
|
786 |
So that the related information will be available
|
|
|
787 |
once the child recursive
|
|
|
788 |
call finishes.\\
|
|
|
789 |
The rest of the clauses of $\bder$ is rather similar to
|
|
|
790 |
$\der$. \\
|
|
|
791 |
Generalising the derivative operation with bitcodes to strings, we have
|
|
|
792 |
\begin{center}
|
|
|
793 |
\begin{tabular}{@{}lcl@{}}
|
|
|
794 |
$a\backslash_s [] $ & $\dn$ & $a$\\
|
|
|
795 |
$a\backslash (c :: s) $ & $\dn$ & $(a \backslash c) \backslash_s s$
|
|
|
796 |
\end{tabular}
|
|
|
797 |
\end{center}
|
|
|
798 |
\noindent
|
|
|
799 |
As we did earlier, we omit the $s$ subscript at $\backslash_s$ when there is no danger
|
|
|
800 |
of confusion.
|
|
|
801 |
\subsection{Putting Things Together}
|
|
|
802 |
Putting these operations altogether, we obtain a lexer with bit-coded regular expressions
|
|
|
803 |
as its internal data structures, which we call $\blexer$:
|
|
|
804 |
|
|
|
805 |
\begin{center}
|
|
|
806 |
\begin{tabular}{lcl}
|
|
|
807 |
$\textit{blexer}\;r\,s$ & $\dn$ &
|
|
|
808 |
$\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\
|
|
|
809 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
|
|
|
810 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
|
811 |
& & $\;\;\textit{else}\;\textit{None}$
|
|
|
812 |
\end{tabular}
|
|
|
813 |
\end{center}
|
|
|
814 |
|
|
|
815 |
\noindent
|
|
|
816 |
Ausaf and Urban formally proved the correctness of the $\blexer$, namely
|
|
|
817 |
\begin{property}
|
|
|
818 |
$\blexer \;r \; s = \lexer \; r \; s$.
|
|
|
819 |
\end{property}
|
|
|
820 |
This was claimed but not formalised in Sulzmann and Lu's work.
|
|
|
821 |
We introduce the proof later, after we give all
|
|
|
822 |
the needed auxiliary functions and definitions.
|
|
|
823 |
But before this we shall first walk the reader
|
|
|
824 |
through a concrete example of our $\blexer$ calculating the right
|
|
|
825 |
lexical information through bit-coded regular expressions.\\
|
|
564
|
826 |
Consider the regular expression $(aa)^* \cdot bc$ matching the string $aabc$
|
|
580
|
827 |
and assume we have just read the first character $a$:
|
|
532
|
828 |
\begin{center}
|
|
537
|
829 |
\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
|
830 |
\node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
580
|
831 |
{$\ONE \cdot a \cdot (aa)^* \cdot bc$
|
|
|
832 |
\nodepart{two} $[] \iff \Seq \; (\Stars \; [\Seq\; a \; ??, \;]), ??$};
|
|
537
|
833 |
\end{tikzpicture}
|
|
|
834 |
\end{center}
|
|
564
|
835 |
\noindent
|
|
580
|
836 |
We use the red area for (annotated) regular expressions and the blue
|
|
|
837 |
area the (partial) bitcodes and (partial) values.
|
|
564
|
838 |
In the injection-based lexing algorithm, we ``neglect" the red area
|
|
|
839 |
by putting all the characters we have consumed and
|
|
|
840 |
intermediate regular expressions on the stack when
|
|
|
841 |
we go from left to right in the derivative phase.
|
|
|
842 |
The red area grows till the string is exhausted.
|
|
|
843 |
During the injection phase, the value in the blue area
|
|
|
844 |
is built up incrementally, while the red area shrinks.
|
|
|
845 |
Before we have recovered all characters and intermediate
|
|
|
846 |
derivative regular expressions from the stack,
|
|
|
847 |
what values these characters and regular expressions correspond
|
|
|
848 |
to are unknown:
|
|
537
|
849 |
\begin{center}
|
|
|
850 |
\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
|
851 |
\node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={white!30,blue!20},]
|
|
564
|
852 |
{$(\ONE \cdot \ONE) \cdot (aa)^* \cdot bc $ correspond to:$???$
|
|
|
853 |
\nodepart{two} $b c$ corresponds to $\Seq(\ldots, \Seq(\Char(b), \Char(c)))$};
|
|
537
|
854 |
%\caption{term 1 \ref{term:1}'s matching configuration}
|
|
|
855 |
\end{tikzpicture}
|
|
|
856 |
\end{center}
|
|
|
857 |
\noindent
|
|
564
|
858 |
However, they should be calculable,
|
|
|
859 |
as characters and regular expression shapes
|
|
|
860 |
after taking derivative w.r.t those characters
|
|
|
861 |
have already been known, therefore in our example,
|
|
|
862 |
we know that the value starts with two $a$s,
|
|
|
863 |
and makes up to an iteration in a Kleene star:
|
|
|
864 |
(We have put the injection-based lexing's partial
|
|
|
865 |
result in the right part of the split rectangle
|
|
|
866 |
to contrast it with the partial valued produced
|
|
|
867 |
in a forward manner)
|
|
537
|
868 |
\begin{center}
|
|
|
869 |
\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
|
870 |
\node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
564
|
871 |
{$\stackrel{Bitcoded}{\longrightarrow} \Seq(\Stars[\Char(a), \Char(a)], ???)$
|
|
|
872 |
\nodepart{two} $\Seq(\ldots, \Seq(\Char(b), \Char(c)))$ $\stackrel{Inj}{\longleftarrow}$};
|
|
537
|
873 |
%\caption{term 1 \ref{term:1}'s matching configuration}
|
|
|
874 |
\end{tikzpicture}
|
|
|
875 |
\end{center}
|
|
|
876 |
\noindent
|
|
|
877 |
If we do this kind of "attachment"
|
|
|
878 |
and each time augment the attached partially
|
|
|
879 |
constructed value when taking off a
|
|
|
880 |
character:
|
|
|
881 |
\begin{center}
|
|
564
|
882 |
\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
|
883 |
\node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] (spPoint)
|
|
|
884 |
{$\Seq(\Stars[\Char(a), \Char(a)], \ldots)$
|
|
|
885 |
\nodepart{two} Remaining: $b c$};
|
|
|
886 |
\end{tikzpicture}\\
|
|
|
887 |
$\downarrow$\\
|
|
537
|
888 |
\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
|
889 |
\node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
|
890 |
{$\Seq(\Stars[\Char(a), \Char(a)], \Seq(\Char(b), \ldots))$
|
|
564
|
891 |
\nodepart{two} Remaining: $c$};
|
|
537
|
892 |
\end{tikzpicture}\\
|
|
564
|
893 |
$\downarrow$\\
|
|
537
|
894 |
\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
|
895 |
\node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
|
896 |
{$\Seq(\Stars[\Char(a), \Char(a)], \Seq(\Char(b), \Char(c)))$
|
|
|
897 |
\nodepart{two} EOF};
|
|
|
898 |
\end{tikzpicture}
|
|
|
899 |
\end{center}
|
|
|
900 |
\noindent
|
|
|
901 |
In the end we could recover the value without a backward phase.
|
|
|
902 |
But (partial) values are a bit clumsy to stick together with a regular expression, so
|
|
|
903 |
we instead use bit-codes to encode them.
|
|
|
904 |
|
|
|
905 |
Bits and bitcodes (lists of bits) are defined as:
|
|
|
906 |
\begin{center}
|
|
|
907 |
$b ::= S \mid Z \qquad
|
|
532
|
908 |
bs ::= [] \mid b::bs
|
|
|
909 |
$
|
|
|
910 |
\end{center}
|
|
|
911 |
|
|
|
912 |
\noindent
|
|
|
913 |
|
|
|
914 |
%-----------------------------------
|
|
|
915 |
% SUBSECTION 1
|
|
|
916 |
%-----------------------------------
|
|
|
917 |
\section{Specifications of Some Helper Functions}
|
|
542
|
918 |
The functions we introduce will give a more detailed glimpse into
|
|
|
919 |
the lexing process, which might not be possible
|
|
|
920 |
using $\lexer$ or $\blexer$ themselves.
|
|
|
921 |
The first function we shall look at is $\retrieve$.
|
|
543
|
922 |
\subsection{$\textit{Retrieve}$}
|
|
542
|
923 |
Our bit-coded lexer "retrieve"s the bitcodes using $\bmkeps$
|
|
|
924 |
after we finished doing all the derivatives:
|
|
532
|
925 |
\begin{center}
|
|
542
|
926 |
\begin{tabular}{lcl}
|
|
|
927 |
& & $\ldots$\\
|
|
|
928 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
|
|
|
929 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
|
930 |
& & $\ldots$
|
|
532
|
931 |
\end{tabular}
|
|
|
932 |
\end{center}
|
|
542
|
933 |
\noindent
|
|
|
934 |
Recall that $\bmkeps$ looks for the leftmost branch of an alternative
|
|
|
935 |
and completes a star's iterations by attaching a $Z$ at the end of the bitcodes
|
|
|
936 |
extracted. It "retrieves" a sequence by visiting both children and then stitch together
|
|
|
937 |
two bitcodes using concatenation. After the entire tree structure of the regular
|
|
|
938 |
expression has been traversed using the above manner, we get a bitcode encoding the
|
|
|
939 |
lexing result.
|
|
|
940 |
We know that this "retrieved" bitcode leads to the correct value after decoding,
|
|
|
941 |
which is $v_0$ in the bird's eye view of the injection-based lexing diagram.
|
|
|
942 |
Now assume we keep every other data structure in the diagram \ref{InjFigure},
|
|
|
943 |
and only replace all the plain regular expression by their annotated counterparts,
|
|
|
944 |
computed during a $\blexer$ run.
|
|
|
945 |
Then we obtain a diagram for the annotated regular expression derivatives and
|
|
|
946 |
their corresponding values, though the values are never calculated in $\blexer$.
|
|
|
947 |
We have that $a_n$ contains all the lexing result information.
|
|
|
948 |
\vspace{20mm}
|
|
|
949 |
\begin{center}%\label{graph:injLexer}
|
|
|
950 |
\begin{tikzcd}[
|
|
|
951 |
every matrix/.append style = {name=p},
|
|
|
952 |
remember picture, overlay,
|
|
|
953 |
]
|
|
|
954 |
a_0 \arrow[r, "\backslash c_0"] \arrow[d] & a_1 \arrow[r, "\backslash c_1"] \arrow[d] & a_2 \arrow[r, dashed] \arrow[d] & a_n \arrow[d] \\
|
|
|
955 |
v_0 & v_1 \arrow[l,"inj_{r_0} c_0"] & v_2 \arrow[l, "inj_{r_1} c_1"] & v_n \arrow[l, dashed]
|
|
|
956 |
\end{tikzcd}
|
|
|
957 |
\begin{tikzpicture}[
|
|
|
958 |
remember picture, overlay,
|
|
|
959 |
E/.style = {ellipse, draw=blue, dashed,
|
|
|
960 |
inner xsep=4mm,inner ysep=-4mm, rotate=90, fit=#1}
|
|
|
961 |
]
|
|
|
962 |
\node[E = (p-1-1) (p-2-1)] {};
|
|
|
963 |
\node[E = (p-1-4) (p-2-4)] {};
|
|
|
964 |
\end{tikzpicture}
|
|
|
965 |
|
|
|
966 |
\end{center}
|
|
|
967 |
\vspace{20mm}
|
|
|
968 |
\noindent
|
|
|
969 |
On the other hand, $v_0$ also encodes the correct lexing result, as we have proven for $\lexer$.
|
|
|
970 |
Encircled in the diagram are the two pairs $v_0, a_0$ and $v_n, a_n$, which both
|
|
|
971 |
encode the correct lexical result. Though for the leftmost pair, we have
|
|
|
972 |
the information condensed in $v_0$ the value part, whereas for the rightmost pair,
|
|
|
973 |
the information is concentrated on $a_n$.
|
|
|
974 |
We know that in the intermediate steps the pairs $v_i, a_i$, must in some way encode the complete
|
|
|
975 |
lexing information as well. Therefore, we need a unified approach to extract such lexing result
|
|
|
976 |
from a value $v_i$ and its annotated regular expression $a_i$.
|
|
|
977 |
And the function $f$ must satisfy these requirements:
|
|
|
978 |
\begin{itemize}
|
|
|
979 |
\item
|
|
|
980 |
$f \; a_i\;v_i = f \; a_n \; v_n = \decode \; (\bmkeps \; a_n) \; (\erase \; a_0)$
|
|
|
981 |
\item
|
|
|
982 |
$f \; a_i\;v_i = f \; a_0 \; v_0 = v_0 = \decode \;(\code \; v_0) \; (\erase \; a_0)$
|
|
|
983 |
\end{itemize}
|
|
|
984 |
\noindent
|
|
|
985 |
If we factor out the common part $\decode \; \_ \; (\erase \; a_0)$,
|
|
|
986 |
The core of the function $f$ is something that produces the bitcodes
|
|
|
987 |
$\code \; v_0$.
|
|
|
988 |
It is unclear how, but Sulzmann and Lu came up with a function satisfying all the above
|
|
|
989 |
requirements, named \emph{retrieve}:
|
|
532
|
990 |
|
|
|
991 |
|
|
|
992 |
|
|
542
|
993 |
\begin{center}
|
|
|
994 |
\begin{tabular}{lcr}
|
|
|
995 |
$\retrieve \; \, (_{bs} \ONE) \; \, (\Empty)$ & $\dn$ & $\textit{bs}$\\
|
|
|
996 |
$\retrieve \; \, (_{bs} \mathbf{c} ) \; \Char(c)$ & $\dn$ & $ \textit{bs}$\\
|
|
|
997 |
$\retrieve \; \, (_{bs} a_1 \cdot a_2) \; \Seq(v_1, v_2)$ & $\dn$ & $\textit{bs} @ (\retrieve \; a_1\; v_1) @ (\retrieve \; a_2 \; v_2)$\\
|
|
|
998 |
$\retrieve \; \, (_{bs} \Sigma (a :: \textit{as}) \; \,\Left(v)$ & $\dn$ & $\textit{bs} @ (\retrieve \; a \; v)$\\
|
|
|
999 |
$\retrieve \; \, (_{bs} \Sigma (a :: \textit{as} \; \, \Right(v)$ & $\dn$ & $\textit{bs} @ (\retrieve \; (_{[]}\Sigma \textit{as}) \; v)$\\
|
|
|
1000 |
$\retrieve \; \, (_{bs} a^*) \; \, (\Stars(v :: vs)) $ & $\dn$ & $\textit{bs} @ (\retrieve \; a \; v) @ (\retrieve \; (_{[]} a^*) \; (\Stars(vs)))$\\
|
|
|
1001 |
$\retrieve \; \, (_{bs} a^*) \; \, (\Stars([]) $ & $\dn$ & $\textit{bs} @ [Z]$
|
|
|
1002 |
\end{tabular}
|
|
|
1003 |
\end{center}
|
|
|
1004 |
\noindent
|
|
|
1005 |
As promised, $\retrieve$ collects the right bit-codes from the
|
|
|
1006 |
final derivative $a_n$:
|
|
|
1007 |
\begin{lemma}
|
|
|
1008 |
$\bnullable \; a \implies \bmkeps \; a = \retrieve \; a \; (\mkeps \; (\erase \; a))$
|
|
|
1009 |
\end{lemma}
|
|
|
1010 |
\begin{proof}
|
|
|
1011 |
By a routine induction on $a$.
|
|
|
1012 |
\end{proof}
|
|
|
1013 |
The design of $\retrieve$ enables extraction of bit-codes
|
|
|
1014 |
from not only $\bnullable$ (annotated) regular expressions,
|
|
|
1015 |
but also those that are not $\bnullable$.
|
|
|
1016 |
For example, if we have the regular expression just internalised
|
|
|
1017 |
and the lexing result value, we could $\retrieve$ the bitcdoes
|
|
|
1018 |
that look as if we have en$\code$-ed the value:
|
|
|
1019 |
\begin{lemma}
|
|
|
1020 |
$\vdash v : r \implies \retrieve \; (r)^\uparrow \; v = \code \; v$
|
|
|
1021 |
\end{lemma}
|
|
|
1022 |
\begin{proof}
|
|
|
1023 |
By induction on $r$.
|
|
|
1024 |
\end{proof}
|
|
|
1025 |
\noindent
|
|
|
1026 |
The following property is more interesting, as
|
|
|
1027 |
it provides a "bridge" between $a_0, v_0$ and $a_n, v_n$ in the
|
|
|
1028 |
lexing diagram.
|
|
|
1029 |
If you take derivative of an annotated regular expression,
|
|
|
1030 |
you can $\retrieve$ the same bit-codes as before the derivative took place,
|
|
|
1031 |
provided that you use the corresponding value:
|
|
|
1032 |
|
|
|
1033 |
\begin{lemma}\label{retrieveStepwise}
|
|
|
1034 |
$\vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c) \; v= \retrieve \; r \; (\inj \; r\; c\; v)$
|
|
|
1035 |
\end{lemma}
|
|
|
1036 |
\begin{proof}
|
|
|
1037 |
By induction on $r$, where $v$ is allowed to be arbitrary.
|
|
|
1038 |
The induction principle is function $\erase$'s cases.
|
|
|
1039 |
\end{proof}
|
|
|
1040 |
\noindent
|
|
|
1041 |
$\retrieve$ is connected to the $\blexer$ in the following way:
|
|
|
1042 |
\begin{lemma}\label{blexer_retrieve}
|
|
|
1043 |
$\blexer \; r \; s = \decode \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$
|
|
|
1044 |
\end{lemma}
|
|
|
1045 |
\noindent
|
|
564
|
1046 |
$\retrieve$ allows free navigation on the diagram \ref{InjFigure} for annotated regular expressiones of $\blexer$.
|
|
542
|
1047 |
For plain regular expressions something similar is required as well.
|
|
|
1048 |
|
|
|
1049 |
\subsection{$\flex$}
|
|
|
1050 |
Ausaf and Urban cleverly defined an auxiliary function called $\flex$ for $\lexer$,
|
|
532
|
1051 |
defined as
|
|
536
|
1052 |
\begin{center}
|
|
|
1053 |
\begin{tabular}{lcr}
|
|
|
1054 |
$\flex \; r \; f \; [] \; v$ & $=$ & $f\; v$\\
|
|
|
1055 |
$\flex \; r \; f \; c :: s \; v$ & $=$ & $\flex \; r \; \lambda v. \, f (\inj \; r\; c\; v)\; s \; v$
|
|
|
1056 |
\end{tabular}
|
|
|
1057 |
\end{center}
|
|
532
|
1058 |
which accumulates the characters that needs to be injected back,
|
|
|
1059 |
and does the injection in a stack-like manner (last taken derivative first injected).
|
|
|
1060 |
$\flex$ is connected to the $\lexer$:
|
|
|
1061 |
\begin{lemma}
|
|
|
1062 |
$\flex \; r \; \textit{id}\; s \; \mkeps (r\backslash s) = \lexer \; r \; s$
|
|
|
1063 |
\end{lemma}
|
|
542
|
1064 |
\begin{proof}
|
|
|
1065 |
By reverse induction on $s$.
|
|
|
1066 |
\end{proof}
|
|
|
1067 |
$\flex$ provides us a bridge between $\lexer$'s intermediate steps.
|
|
532
|
1068 |
What is even better about $\flex$ is that it allows us to
|
|
|
1069 |
directly operate on the value $\mkeps (r\backslash v)$,
|
|
|
1070 |
which is pivotal in the definition of $\lexer $ and $\blexer$, but not visible as an argument.
|
|
|
1071 |
When the value created by $\mkeps$ becomes available, one can
|
|
|
1072 |
prove some stepwise properties of lexing nicely:
|
|
|
1073 |
\begin{lemma}\label{flexStepwise}
|
|
|
1074 |
$\textit{flex} \; r \; f \; s@[c] \; v= \flex \; r \; f\; s \; (\inj \; (r\backslash s) \; c \; v) $
|
|
|
1075 |
\end{lemma}
|
|
542
|
1076 |
\begin{proof}
|
|
|
1077 |
By induction on the shape of $r\backslash s$
|
|
|
1078 |
\end{proof}
|
|
|
1079 |
\noindent
|
|
|
1080 |
With $\flex$ and $\retrieve$ ready, we are ready to connect $\lexer$ and $\blexer$ .
|
|
532
|
1081 |
|
|
542
|
1082 |
\subsection{Correctness Proof of Bit-coded Algorithm}
|
|
532
|
1083 |
\begin{lemma}\label{flex_retrieve}
|
|
|
1084 |
$\flex \; r \; \textit{id}\; s\; v = \decode \; (\retrieve \; (r\backslash s )\; v) \; r$
|
|
|
1085 |
\end{lemma}
|
|
|
1086 |
\begin{proof}
|
|
|
1087 |
By induction on $s$. The induction tactic is reverse induction on strings.
|
|
|
1088 |
$v$ is allowed to be arbitrary.
|
|
|
1089 |
The crucial point is to rewrite
|
|
|
1090 |
\[
|
|
|
1091 |
\retrieve \; (r \backslash s@[c]) \; \mkeps (r \backslash s@[c])
|
|
|
1092 |
\]
|
|
|
1093 |
as
|
|
|
1094 |
\[
|
|
|
1095 |
\retrieve \; (r \backslash s) \; (\inj \; (r \backslash s) \; c\; \mkeps (r \backslash s@[c]))
|
|
|
1096 |
\].
|
|
|
1097 |
This enables us to equate
|
|
|
1098 |
\[
|
|
|
1099 |
\retrieve \; (r \backslash s@[c]) \; \mkeps (r \backslash s@[c])
|
|
|
1100 |
\]
|
|
|
1101 |
with
|
|
|
1102 |
\[
|
|
|
1103 |
\flex \; r \; \textit{id} \; s \; (\inj \; (r\backslash s) \; c\; (\mkeps (r\backslash s@[c])))
|
|
|
1104 |
\],
|
|
|
1105 |
which in turn can be rewritten as
|
|
|
1106 |
\[
|
|
|
1107 |
\flex \; r \; \textit{id} \; s@[c] \; (\mkeps (r\backslash s@[c]))
|
|
|
1108 |
\].
|
|
|
1109 |
\end{proof}
|
|
|
1110 |
|
|
|
1111 |
With the above lemma we can now link $\flex$ and $\blexer$.
|
|
|
1112 |
|
|
542
|
1113 |
%----------------------------------------------------------------------------------------
|
|
|
1114 |
% SECTION correctness proof
|
|
|
1115 |
%----------------------------------------------------------------------------------------
|
|
|
1116 |
\section{Correctness of Bit-coded Algorithm (Without Simplification)}
|
|
|
1117 |
We now give the proof the correctness of the algorithm with bit-codes.
|
|
|
1118 |
|
|
532
|
1119 |
\begin{lemma}\label{flex_blexer}
|
|
|
1120 |
$\textit{flex} \; r \; \textit{id} \; s \; \mkeps(r \backslash s) = \blexer \; r \; s$
|
|
|
1121 |
\end{lemma}
|
|
|
1122 |
\begin{proof}
|
|
|
1123 |
Using two of the above lemmas: \ref{flex_retrieve} and \ref{blexer_retrieve}.
|
|
|
1124 |
\end{proof}
|
|
542
|
1125 |
Finally the correctness of $\blexer$ is given as it outputs the same result as $\lexer$:
|
|
|
1126 |
\begin{theorem}
|
|
|
1127 |
$\blexer\; r \; s = \lexer \; r \; s$
|
|
|
1128 |
\end{theorem}
|
|
|
1129 |
\begin{proof}
|
|
|
1130 |
Straightforward corollary of \ref{flex_blexer}.
|
|
|
1131 |
\end{proof}
|
|
|
1132 |
\noindent
|
|
576
|
1133 |
To piece things together and spell out the exact correctness
|
|
|
1134 |
of the bitcoded lexer
|
|
|
1135 |
in terms of producing POSIX values,
|
|
|
1136 |
we use the fact from the previous chapter that
|
|
|
1137 |
\[
|
|
|
1138 |
If \; (r, s) \rightarrow v \; then \; \lexer \; r \; s = v
|
|
|
1139 |
\]
|
|
|
1140 |
to obtain this corollary:
|
|
|
1141 |
\begin{corollary}\label{blexerPOSIX}
|
|
|
1142 |
$If \; (r, s) \rightarrow v \; then \blexer \; r \; s = v$
|
|
|
1143 |
\end{corollary}
|
|
542
|
1144 |
Our main reason for wanting a bit-coded algorithm over
|
|
|
1145 |
the injection-based one is for its capabilities of allowing
|
|
|
1146 |
more aggressive simplifications.
|
|
|
1147 |
We will elaborate on this in the next chapter.
|
|
532
|
1148 |
|
|
|
1149 |
|