Centaur Lexer Library.
This is a rudimentary library for creating lexers for character data in ACL2. It is an outgrowth and revision of lexer support routines that were originally developed as part of the ACL2::vl library.
These routines are based on ACL2 ACL2::characters. They are, accordingly, suitable for processing text in ASCII or ISO-8859-1 or some other 8-bit character set, but not Unicode or other wide character sets. It would generally be a bad idea to use CLEX to write a lexer for a language like Java or XML that needs Unicode support.
Many lexical analyzers like Flex are rather sophisticated and allow you to declare the syntax of your tokens at a relatively high level (e.g., via regular expressions); this description is then compiled into a full-blown scanner function.
In comparison, CLEX is quite primitive. Really, it is nothing more than some functions that tend to be useful when writing lexers "by hand." Even so, this is not so bad. Here are the things that CLEX provides:
Most users should simply load the top book in the library as follows:
(include-book "centaur/clex/top" :dir :system)
Besides this documentation, you may find it useful to see the example-lexer, located in