• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
        • Parse-options
        • Regex-get
        • Do-regex-match
        • Do-regex-match-precomp
        • Patbind-match
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Projects

Regex

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.

Subtopics

Parse-options
Generate options for using regular expressions to parse/match strings
Regex-get
Lookup a string in the regular expression alist.
Do-regex-match
Test whether a given string matches a given regular expression
Do-regex-match-precomp
Test whether a given string matches a given regular expression
Patbind-match
b* binder for regular expression matching.