A Simplified Scanner Generator

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

The auto_chopper is implemented in theory AutoChopper. An alternative (more efficient) version is defined in AutoChopper1. However, no properties have been proved for it yet. The top part of the diagram, i.e. the translation of regular expressions into deterministic finite automata is still missing (although we have some bits and pieces).

The directory also contains Regset_of_auto, a theory describing the translation of deterministic automata into regular sets.