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

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