|
4931
|
1 |
<!-- $Id$ -->
|
|
3279
|
2 |
<HTML><HEAD><TITLE>HOL/Lex/README</TITLE></HEAD>
|
|
1344
|
3 |
<BODY>
|
|
|
4 |
|
|
1345
|
5 |
<H1>A Simplified Scanner Generator</H1>
|
|
1344
|
6 |
|
|
4931
|
7 |
This directory contains the theories for the functional scanner generator
|
|
|
8 |
described
|
|
|
9 |
<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols98.html">
|
|
5327
|
10 |
here</A>. In contrast to the paper, the latest version of the theories
|
|
|
11 |
provides a fully executable scanner generator. The non-executable bits
|
|
|
12 |
(transitive closure) have been eliminated by going from regular expressions
|
|
|
13 |
directly to nondeterministic automata, thus bypassing epsilon-moves.
|
|
|
14 |
<br>
|
|
4931
|
15 |
<br>
|
|
|
16 |
Overview:
|
|
|
17 |
<dl>
|
|
|
18 |
<dt>Automata</dt>
|
|
|
19 |
<dd>AutoProj, NA, NAe, DA, Automata</dd>
|
|
|
20 |
<dt>Regular expressions and their conversion to automata</dt>
|
|
5327
|
21 |
<dd>RegSet, RegExp, RegExp2NA, RegExp2NAe</dd>
|
|
4931
|
22 |
<dt>Scanning</dt>
|
|
|
23 |
<dd>Prefix, MaxPrefix, MaxChop, AutoMaxChop, Scanner</dd>
|
|
|
24 |
</dl>
|
|
|
25 |
In addition there are some bits and pieces:
|
|
|
26 |
<ul>
|
|
|
27 |
<li> Regset_of_nat_DA describes the translation of deterministic automata
|
|
|
28 |
into regular sets. Should be completed to translate finite automata
|
|
|
29 |
into regular expressions.
|
|
|
30 |
<li> Chopper, AutoChopper and AutoChopper1 are old versions of the scanner
|
|
|
31 |
(excluding regular expressions). Mainly of historic interest.
|
|
|
32 |
</ul>
|
|
1344
|
33 |
|
|
|
34 |
</BODY>
|
|
|
35 |
</HTML>
|