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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     1
<HTML><HEAD><TITLE>HOL/Lex/ReadMe</TITLE></HEAD>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     2
<BODY>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     3
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     4
<H2>A Simplified Scanner Generator</H2>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     5
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     6
This is half of a simplified functional scanner generator. The overall design
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     7
is like this:
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     8
<PRE>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     9
         regular expression
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    10
                  |
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    11
                  v
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    12
             -----------
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    13
             | mk_auto |
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    14
             -----------
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    15
                  |
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    16
        deterministic automaton
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    17
                  |
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    18
                  v
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    19
           ----------------
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    20
string --> | auto_chopper | --> chopped up string
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    21
           ----------------
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    22
</PRE>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    23
A chopped up string is a pair of
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    24
<UL>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    25
<LI>a prefix of the input string, chopped up into words of the language,
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    26
<LI>together with the remaining suffix.
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    27
</UL>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    28
For example, if the language consists just of the word <KBD>ab</KBD>, the
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    29
input <KBD>ababaab</KBD> is partitioned into a chopped up prefix
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    30
<KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    31
<P>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    32
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    33
The auto_chopper is implemented in theory AutoChopper. The top part of the
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    34
diagram, i.e. the translation of regular expressions into deterministic
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    35
finite automata is still missing.  <P>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    36
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    37
<B>WANTED:</B> a theoretically inclined student to formalize a bit of
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    38
undergraduate level automata theory. This could be worth a "Diplom" or an
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    39
M.Sc. It could also be undertaken as a two-person "Fopra".
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    40
</BODY>
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    41
</HTML>