• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Prime-field-constraint-systems
    • Proof-checker-array
    • Soft
    • Rp-rewriter
    • Farray
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Bigmem
    • Regex
      • Parse-options
      • Regex-get
      • Do-regex-match
      • Do-regex-match-precomp
      • Patbind-match
    • ACL2-programming-language
    • Java
    • C
    • Jfkr
    • X86isa
    • Equational
    • Cryptography
    • Where-do-i-place-my-book
    • Json
    • Built-ins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Regex

Do-regex-match-precomp

Test whether a given string matches a given regular expression

Signature

(do-regex-match-precomp str regex opts) → (mv whole substrs)

Arguments

str — String to test.
    Guard (stringp str).

regex — Regular expression specifying the pattern to find.
    Guard (regex-p regex).

opts — Options for test.
BOZO: state and explain the possible options. Possible options might include :b/:e/:f for basic/extended/fixed, :i for case-insensitive, :full for something, etc.
    Guard (parse-opts-p opts).

Returns

whole — The portion of str that matches the pattern provided by regex. Nil if there is not a match.
    Type (or (stringp whole) (not whole)).

substrs — List of substrings that match parenthesized subexpressions of the pattern (when applicable). Nil if there is not a match.
    Type (true-listp substrs).

Intended for use during macroexpansion, as occurs in b*.

Definitions and Theorems

Function: do-regex-match-precomp

(defun do-regex-match-precomp (str regex opts)
       (declare (xargs :guard (and (stringp str)
                                   (regex-p regex)
                                   (parse-opts-p opts))))
       (let ((__function__ 'do-regex-match-precomp))
            (declare (ignorable __function__))
            (b* ((str (mbe :logic (if (stringp str) str "")
                           :exec str))
                 (transstr (if (parse-options-case-insensitive opts)
                               (str::downcase-string str)
                               str))
                 ((mv ?matchp whole substrs)
                  (match-regex regex transstr str)))
                (mv whole substrs))))

Theorem: return-type-of-do-regex-match-precomp.whole

(defthm return-type-of-do-regex-match-precomp.whole
        (b* (((mv ?whole ?substrs)
              (do-regex-match-precomp str regex opts)))
            (or (stringp whole) (not whole)))
        :rule-classes :type-prescription)

Theorem: true-listp-of-do-regex-match-precomp.substrs

(defthm true-listp-of-do-regex-match-precomp.substrs
        (b* (((mv ?whole ?substrs)
              (do-regex-match-precomp str regex opts)))
            (true-listp substrs))
        :rule-classes :type-prescription)

Theorem: string-or-nil-listp-of-do-regex-match-precomp-substrs

(defthm string-or-nil-listp-of-do-regex-match-precomp-substrs
        (string-or-nil-listp
             (mv-nth 1
                     (do-regex-match-precomp str regex opts))))