• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
      • Acre-internals
      • Parse-and-match-regex
      • Match-regex
      • Parse
      • Matchresult->matchedp
      • Match
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Prime-field-constraint-systems
    • Proof-checker-array
    • Soft
    • Rp-rewriter
    • Farray
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Bigmem
    • Regex
    • ACL2-programming-language
    • Java
    • C
    • Jfkr
    • X86isa
    • Equational
    • Cryptography
    • Where-do-i-place-my-book
    • Json
    • Built-ins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Acre

Parse-and-match-regex

Parse a regular expression from a pattern string and match it against a string x.

Signature

(parse-and-match-regex pat x &key (case-insens 'nil) (legible 't)) 
  → 
(mv parse-err match)

Arguments

pat — String to parse as a regular expression.
    Guard (stringp pat).

x — String to match against.
    Guard (stringp x).

case-insens — Match case-insensitively.
    Guard (booleanp case-insens).

legible — Option to preprocess away non-escaped whitespace and Perl-style # comments.
    Guard (booleanp legible).

Returns

parse-err — Parse error message.
    Type (acl2::maybe-stringp parse-err).

match — Result of matching, including whether it matched, which part matched, and capture group matches.
    Type (matchresult-p match).

Same as parse followed by match-regex.

Definitions and Theorems

Function: parse-and-match-regex-fn

(defun parse-and-match-regex-fn
       (pat x case-insens legible)
       (declare (xargs :guard (and (stringp pat)
                                   (stringp x)
                                   (booleanp case-insens)
                                   (booleanp legible))))
       (let ((__function__ 'parse-and-match-regex))
            (declare (ignorable __function__))
            (b* (((mv err regex)
                  (parse pat :legible legible))
                 ((when err)
                  (mv err
                      (make-matchresult :loc nil
                                        :len 0
                                        :str x
                                        :backrefs nil))))
                (mv nil
                    (match-regex regex x
                                 :case-insens case-insens)))))

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

(defthm maybe-stringp-of-parse-and-match-regex.parse-err
        (b* (((mv ?parse-err ?match)
              (parse-and-match-regex-fn pat x case-insens legible)))
            (acl2::maybe-stringp parse-err))
        :rule-classes :type-prescription)

Theorem: matchresult-p-of-parse-and-match-regex.match

(defthm matchresult-p-of-parse-and-match-regex.match
        (b* (((mv ?parse-err ?match)
              (parse-and-match-regex-fn pat x case-insens legible)))
            (matchresult-p match))
        :rule-classes :rewrite)

Theorem: matchresult-in-bounds-of-parse-and-match-regex

(defthm matchresult-in-bounds-of-parse-and-match-regex
        (b* (((mv ?parse-err ?match)
              (parse-and-match-regex-fn pat x case-insens legible)))
            (matchresult-in-bounds match)))

Theorem: matchresult->str-of-parse-and-match-regex

(defthm matchresult->str-of-parse-and-match-regex
        (b* (((mv ?parse-err ?match)
              (parse-and-match-regex-fn pat x case-insens legible)))
            (equal (matchresult->str match)
                   (lstrfix x))))

Theorem: parse-and-match-regex-fn-of-str-fix-pat

(defthm
     parse-and-match-regex-fn-of-str-fix-pat
     (equal (parse-and-match-regex-fn (acl2::str-fix pat)
                                      x case-insens legible)
            (parse-and-match-regex-fn pat x case-insens legible)))

Theorem: parse-and-match-regex-fn-streqv-congruence-on-pat

(defthm
 parse-and-match-regex-fn-streqv-congruence-on-pat
 (implies
   (acl2::streqv pat pat-equiv)
   (equal
        (parse-and-match-regex-fn pat x case-insens legible)
        (parse-and-match-regex-fn pat-equiv x case-insens legible)))
 :rule-classes :congruence)

Theorem: parse-and-match-regex-fn-of-str-fix-x

(defthm
     parse-and-match-regex-fn-of-str-fix-x
     (equal (parse-and-match-regex-fn pat (acl2::str-fix x)
                                      case-insens legible)
            (parse-and-match-regex-fn pat x case-insens legible)))

Theorem: parse-and-match-regex-fn-streqv-congruence-on-x

(defthm
 parse-and-match-regex-fn-streqv-congruence-on-x
 (implies
   (acl2::streqv x x-equiv)
   (equal
        (parse-and-match-regex-fn pat x case-insens legible)
        (parse-and-match-regex-fn pat x-equiv case-insens legible)))
 :rule-classes :congruence)

Theorem: parse-and-match-regex-fn-of-bool-fix-case-insens

(defthm
 parse-and-match-regex-fn-of-bool-fix-case-insens
 (equal (parse-and-match-regex-fn pat x (acl2::bool-fix case-insens)
                                  legible)
        (parse-and-match-regex-fn pat x case-insens legible)))

Theorem: parse-and-match-regex-fn-iff-congruence-on-case-insens

(defthm
 parse-and-match-regex-fn-iff-congruence-on-case-insens
 (implies
   (iff case-insens case-insens-equiv)
   (equal
        (parse-and-match-regex-fn pat x case-insens legible)
        (parse-and-match-regex-fn pat x case-insens-equiv legible)))
 :rule-classes :congruence)

Theorem: parse-and-match-regex-fn-of-bool-fix-legible

(defthm
 parse-and-match-regex-fn-of-bool-fix-legible
 (equal
   (parse-and-match-regex-fn pat
                             x case-insens (acl2::bool-fix legible))
   (parse-and-match-regex-fn pat x case-insens legible)))

Theorem: parse-and-match-regex-fn-iff-congruence-on-legible

(defthm
 parse-and-match-regex-fn-iff-congruence-on-legible
 (implies
   (iff legible legible-equiv)
   (equal
        (parse-and-match-regex-fn pat x case-insens legible)
        (parse-and-match-regex-fn pat x case-insens legible-equiv)))
 :rule-classes :congruence)