| author | paulson |
| Mon, 02 Feb 1998 12:55:39 +0100 | |
| changeset 4593 | 6fc8f224655f |
| parent 4137 | 2ce2e659c2b1 |
| child 4931 | 2ec84dee7911 |
| permissions | -rw-r--r-- |
| 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 |
||
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
33 |
The auto_chopper is implemented in theory AutoChopper. An alternative (more |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
34 |
efficient) version is defined in AutoChopper1. However, no properties have |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
35 |
been proved for it yet. |
| 1344 | 36 |
|
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
37 |
The top part of the diagram, i.e. the translation of regular expressions into |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
38 |
deterministic finite automata is still missing (although we have some bits |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
39 |
and pieces). |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
40 |
<P> |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
41 |
|
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
42 |
The directory also contains Regset_of_auto, a theory describing the |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
3279
diff
changeset
|
43 |
translation of deterministic automata into regular sets. |
| 1344 | 44 |
</BODY> |
45 |
</HTML> |