• 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

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)