Regular expression library for ACL2
This library is modeled after the regular expression parsing functionality of GNU grep. While the code is mostly considered to be complete enough for now, we invite those who wish to improve the documentation to go ahead and do so. As of March 2013, this library is compliant with 579 of the 646 GNU grep regression suite tests (see book projects/regex/regex-tests for those tests).
To start using the regex library, include book projects/regex/regex-ui.
This library supports "Basic", "Extended", and "Fixed" regular expressions (see parse-options). Although some implementations of GNU Grep support "Perl" regular expressions, we do not yet implement them. If a user is motivated to provide such an extension, they should feel free to do so.
This library does not currently support features like [[:digit:]] and [[:alpha:]]. A workaround for this is specifying the expansion of these named classes, respectively, as in [0-9] and [a-zA-Z].
See GNU Grep Regular Expressions for more information on these regular expressions.