		Search-engine friendly clone of the ACL2 documentation.

Regex

Do-regex-match

Test whether a given string matches a given regular expression

Signature
(do-regex-match str pat opts) → (mv error-msg whole substrs)
Arguments: str — String to test.
Guard (stringp str).; pat — String representing the pattern to find.
Guard (stringp pat).; 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: error-msg — Error message.
Type (or (stringp error-msg) (not error-msg)).; whole — The portion of str that matches the pattern provided by pat. 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 in the dynamically compiled case.

As examples:

(do-regex-match "cdeAbfdEfDeghIj"
                "cdeabfdefdeghij"
               (parse-options 'fixed ; type
                               nil  ; not strict-paren
                               nil  ; not strict-brace
                               nil  ; not strict-repeat
                               t    ; case-insensitive
                               ))

returns (mv nil "cdeAbfdEfDeghIj" nil),

(do-regex-match "cdeAbfdEfDeghIj"
                "ab([def]*)\1([gh])"
                (parse-options 'fixed nil nil nil t))

returns (mv nil nil nil), and

(do-regex-match "cdeAbfdEfDeghIj"
                "ab([def]*)\1([gh])"
                (parse-options 'ere nil nil nil t))

returns (mv nil "AbfdEfDeg" ("fdE" "g")).

Definitions and Theorems

Function: do-regex-match

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

Theorem: return-type-of-do-regex-match.error-msg

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

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

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

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

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

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

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