• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Aleobft
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Bigmem-asymmetric
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • Bigmem
    • Sha-2
    • Yul
    • X86isa
    • 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
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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))))