• 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

Parse a pattern string into a regular expression object.

Signature

(parse pat &key (legible 't)) → (mv err regex)

Arguments

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

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

Returns

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

regex — Regular expression object, if no error.
    Type (implies (not err) (regex-p regex)).

Definitions and Theorems

Function: parse-fn

(defun
     parse-fn (pat legible)
     (declare (xargs :guard (and (stringp pat) (booleanp legible))))
     (let ((__function__ 'parse))
          (declare (ignorable __function__))
          (b* ((preproc-pat (if legible (preproc-legible pat)
                                (lstrfix pat))))
              (parse-regex preproc-pat))))

Theorem: maybe-stringp-of-parse.err

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

Theorem: return-type-of-parse.regex

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

Theorem: parse-fn-of-str-fix-pat

(defthm parse-fn-of-str-fix-pat
        (equal (parse-fn (acl2::str-fix pat) legible)
               (parse-fn pat legible)))

Theorem: parse-fn-streqv-congruence-on-pat

(defthm parse-fn-streqv-congruence-on-pat
        (implies (acl2::streqv pat pat-equiv)
                 (equal (parse-fn pat legible)
                        (parse-fn pat-equiv legible)))
        :rule-classes :congruence)

Theorem: parse-fn-of-bool-fix-legible

(defthm parse-fn-of-bool-fix-legible
        (equal (parse-fn pat (acl2::bool-fix legible))
               (parse-fn pat legible)))

Theorem: parse-fn-iff-congruence-on-legible

(defthm parse-fn-iff-congruence-on-legible
        (implies (iff legible legible-equiv)
                 (equal (parse-fn pat legible)
                        (parse-fn pat legible-equiv)))
        :rule-classes :congruence)