src/HOL/Lex/README.html
author nipkow
Sat, 18 Nov 1995 14:55:44 +0100
changeset 1344 f172a7f14e49
child 1345 d4e26f632bca
permissions -rw-r--r--
Half a lexical analyzer generator.

<HTML><HEAD><TITLE>HOL/Lex/ReadMe</TITLE></HEAD>
<BODY>

<H2>A Simplified Scanner Generator</H2>

This is half of a simplified functional scanner generator. The overall design
is like this:
<PRE>
         regular expression
                  |
                  v
             -----------
             | mk_auto |
             -----------
                  |
        deterministic automaton
                  |
                  v
           ----------------
string --> | auto_chopper | --> chopped up string
           ----------------
</PRE>
A chopped up string is a pair of
<UL>
<LI>a prefix of the input string, chopped up into words of the language,
<LI>together with the remaining suffix.
</UL>
For example, if the language consists just of the word <KBD>ab</KBD>, the
input <KBD>ababaab</KBD> is partitioned into a chopped up prefix
<KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
<P>

The auto_chopper is implemented in theory AutoChopper. The top part of the
diagram, i.e. the translation of regular expressions into deterministic
finite automata is still missing.  <P>

<B>WANTED:</B> a theoretically inclined student to formalize a bit of
undergraduate level automata theory. This could be worth a "Diplom" or an
M.Sc. It could also be undertaken as a two-person "Fopra".
</BODY>
</HTML>