|
3279
|
1 |
<HTML><HEAD><TITLE>HOL/Lex/README</TITLE></HEAD>
|
|
1344
|
2 |
<BODY>
|
|
|
3 |
|
|
1345
|
4 |
<H1>A Simplified Scanner Generator</H1>
|
|
1344
|
5 |
|
|
|
6 |
This is half of a simplified functional scanner generator. The overall design
|
|
|
7 |
is like this:
|
|
|
8 |
<PRE>
|
|
|
9 |
regular expression
|
|
|
10 |
|
|
|
|
11 |
v
|
|
|
12 |
-----------
|
|
|
13 |
| mk_auto |
|
|
|
14 |
-----------
|
|
|
15 |
|
|
|
|
16 |
deterministic automaton
|
|
|
17 |
|
|
|
|
18 |
v
|
|
|
19 |
----------------
|
|
|
20 |
string --> | auto_chopper | --> chopped up string
|
|
|
21 |
----------------
|
|
|
22 |
</PRE>
|
|
|
23 |
A chopped up string is a pair of
|
|
|
24 |
<UL>
|
|
|
25 |
<LI>a prefix of the input string, chopped up into words of the language,
|
|
|
26 |
<LI>together with the remaining suffix.
|
|
|
27 |
</UL>
|
|
|
28 |
For example, if the language consists just of the word <KBD>ab</KBD>, the
|
|
|
29 |
input <KBD>ababaab</KBD> is partitioned into a chopped up prefix
|
|
|
30 |
<KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
|
|
|
31 |
<P>
|
|
|
32 |
|
|
|
33 |
The auto_chopper is implemented in theory AutoChopper. The top part of the
|
|
|
34 |
diagram, i.e. the translation of regular expressions into deterministic
|
|
|
35 |
finite automata is still missing. <P>
|
|
|
36 |
|
|
|
37 |
</BODY>
|
|
|
38 |
</HTML>
|