		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Parse-primitive

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

Definitions and Theorems

Function: parse-primitive

(defun parse-primitive (x index)
 (declare (xargs :guard (and (stringp x) (natp index))))
 (declare (xargs :guard (<= index (strlen x))))
 (let ((__function__ 'parse-primitive))
  (declare (ignorable __function__))
  (b* ((index (lnfix index))
       ((when (<= (strlen x) (lnfix index)))
        (mv "EOS parsing primitive" nil index))
       (char (char x index))
       (index (+ 1 index)))
   (case char
    (#\. (mv nil (regex-charset "" t) index))
    (#\^ (mv nil (regex-start) index))
    (#\$ (mv nil (regex-end) index))
    (#\[ (parse-charset x index))
    (#\\
      (b*
        (((when (<= (strlen x) (lnfix index)))
          (mv "EOS after backslash" nil index))
         (char (char x index))
         (charset (charset-char-regex char))
         ((when charset)
          (mv nil charset (+ 1 index)))
         ((when (str::dec-digit-char-p char))
          (b* (((mv val len)
                (str::parse-nat-from-string x 0 0 index (strlen x)))
               (index (+ index len)))
            (mv nil (regex-backref val) index)))
         (index (+ 1 index)))
        (case char
          (#\n (mv nil
                   (regex-exact (coerce '(#\Newline) 'string))
                   index))
          (#\t (mv nil
                   (regex-exact (coerce '(#\Tab) 'string))
                   index))
          (#\r (mv nil
                   (regex-exact (coerce '(#\Return) 'string))
                   index))
          (#\f (mv nil
                   (regex-exact (coerce '(#\Page) 'string))
                   index))
          (#\o (b* (((mv err char index)
                     (parse-octal-charcode x index))
                    ((when err) (mv err nil index)))
                 (mv nil
                     (regex-exact (coerce (list char) 'string))
                     index)))
          (#\x (b* (((mv err char index)
                     (parse-hex-charcode x index))
                    ((when err) (mv err nil index)))
                 (mv nil
                     (regex-exact (coerce (list char) 'string))
                     index)))
          ((#\\ #\^ #\. #\$
                #\| #\( #\) #\[ #\] #\* #\+ #\? #\{ #\})
           (mv nil
               (regex-exact (coerce (list char) 'string))
               index))
          (#\g (parse-g-backref x index))
          (#\k (parse-k-backref x index))
          (t (mv (str::cat "Unrecognized escape: \\"
                           (coerce (list char) 'string))
                 nil index)))))
    ((#\| #\( #\) #\] #\* #\+ #\? #\{ #\})
     (mv "Found metacharacter while parsing primitive"
         nil index))
    (t (mv nil
           (regex-exact (coerce (list char) 'string))
           index))))))

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

(defthm maybe-stringp-of-parse-primitive.err
  (b* (((mv ?err ?pat ?new-index)
        (parse-primitive x index)))
    (acl2::maybe-stringp err))
  :rule-classes :type-prescription)

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

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

Theorem: natp-of-parse-primitive.new-index

(defthm natp-of-parse-primitive.new-index
  (b* (((mv ?err ?pat ?new-index)
        (parse-primitive x index)))
    (natp new-index))
  :rule-classes :type-prescription)

Theorem: new-index-of-parse-primitive

(defthm new-index-of-parse-primitive
  (b* (((mv ?err ?pat ?new-index)
        (parse-primitive x index)))
    (<= (nfix index) new-index))
  :rule-classes :linear)

Theorem: new-index-of-parse-primitive-strong

(defthm new-index-of-parse-primitive-strong
  (b* (((mv ?err ?pat ?new-index)
        (parse-primitive x index)))
    (implies (not err)
             (< (nfix index) new-index)))
  :rule-classes :linear)

Theorem: new-index-of-parse-primitive-less-than-length

(defthm new-index-of-parse-primitive-less-than-length
  (b* (((mv ?err ?pat ?new-index)
        (parse-primitive x index)))
    (implies (<= (nfix index)
                 (len (acl2::explode x)))
             (<= new-index (len (acl2::explode x)))))
  :rule-classes :linear)

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

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

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

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

Theorem: parse-primitive-of-nfix-index

(defthm parse-primitive-of-nfix-index
  (equal (parse-primitive x (nfix index))
         (parse-primitive x index)))

Theorem: parse-primitive-nat-equiv-congruence-on-index

(defthm parse-primitive-nat-equiv-congruence-on-index
  (implies (acl2::nat-equiv index index-equiv)
           (equal (parse-primitive x index)
                  (parse-primitive x index-equiv)))
  :rule-classes :congruence)