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