		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Parse-regex

Signature
(parse-regex x) → (mv err pat)
Arguments: x — Guard (stringp x).
Returns: err — Type (acl2::maybe-stringp err).; pat — Type (implies (not err) (regex-p pat)).

Definitions and Theorems

Function: parse-regex

(defun parse-regex (x)
 (declare (xargs :guard (stringp x)))
 (let ((__function__ 'parse-regex))
  (declare (ignorable __function__))
  (b*
   (((mv err regex index ?br-index)
     (parse-regex-rec x 0 1))
    ((when err) (mv err nil))
    ((when (< index (strlen x)))
     (mv
      (str::cat
        "Regex parsing didn't consume the whole string: Remaining: "
        (subseq x index nil))
      nil)))
   (mv nil regex))))

Theorem: maybe-stringp-of-parse-regex.err

(defthm maybe-stringp-of-parse-regex.err
  (b* (((mv ?err ?pat) (parse-regex x)))
    (acl2::maybe-stringp err))
  :rule-classes :rewrite)

Theorem: return-type-of-parse-regex.pat

(defthm return-type-of-parse-regex.pat
  (b* (((mv ?err ?pat) (parse-regex x)))
    (implies (not err) (regex-p pat)))
  :rule-classes :rewrite)

Theorem: parse-regex-of-str-fix-x

(defthm parse-regex-of-str-fix-x
  (equal (parse-regex (acl2::str-fix x))
         (parse-regex x)))

Theorem: parse-regex-streqv-congruence-on-x

(defthm parse-regex-streqv-congruence-on-x
  (implies (acl2::streqv x x-equiv)
           (equal (parse-regex x)
                  (parse-regex x-equiv)))
  :rule-classes :congruence)