• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • 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
      • Parse-options
      • Regex-get
      • Do-regex-match
      • Do-regex-match-precomp
      • Patbind-match
    • 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

• Regex

Parse-options

Generate options for using regular expressions to parse/match strings

General form:

(parse-options parse-type
               strict-paren
               strict-brace
               strict-repeat
               case-insensitive)

Parse-type should be one of 'ere, 'bre, or 'fixed. Basic regular expressions (BRE's) do not support many of the features of traditional regular expressions (e.g., parentheses), so you may wish to consider using extended regular expressions (ERE's). Fixed indicates that the pattern should be interpreted as a list of fixed strings, separated by newlines, any of which is to be matched.

Strict-paren, strict-brace, and strict-repeat, and case-insensitive are booleanp values.

BOZO: document strict-paren, strict-brace, and strict-repeat.

Definitions and Theorems

Function: parse-options-p

(defun parse-options-p (x)
  (declare (xargs :guard t))
  (and (consp x)
       (consp (cdr x))
       (consp (car (cdr x)))
       t t (consp (cdr (cdr x)))
       t (consp (cdr (cdr (cdr x))))
       t t (eq (car x) 'parse-options)))

Function: parse-options

(defun parse-options (type strict-paren strict-brace
                           strict-repeat case-insensitive)
  (declare (xargs :guard t))
  (cons 'parse-options
        (cons (cons type strict-paren)
              (cons strict-brace
                    (cons strict-repeat case-insensitive)))))

Function: parse-options-type

(defun parse-options-type (x)
  (declare (xargs :guard (parse-options-p x)))
  (mbe :logic (and (parse-options-p x)
                   (car (car (cdr x))))
       :exec (car (car (cdr x)))))

Function: parse-options-strict-paren

(defun parse-options-strict-paren (x)
  (declare (xargs :guard (parse-options-p x)))
  (mbe :logic (and (parse-options-p x)
                   (cdr (car (cdr x))))
       :exec (cdr (car (cdr x)))))

Function: parse-options-strict-brace

(defun parse-options-strict-brace (x)
  (declare (xargs :guard (parse-options-p x)))
  (mbe :logic (and (parse-options-p x)
                   (car (cdr (cdr x))))
       :exec (car (cdr (cdr x)))))

Function: parse-options-strict-repeat

(defun parse-options-strict-repeat (x)
  (declare (xargs :guard (parse-options-p x)))
  (mbe :logic (and (parse-options-p x)
                   (car (cdr (cdr (cdr x)))))
       :exec (car (cdr (cdr (cdr x))))))

Function: parse-options-case-insensitive

(defun parse-options-case-insensitive (x)
  (declare (xargs :guard (parse-options-p x)))
  (mbe :logic (and (parse-options-p x)
                   (cdr (cdr (cdr (cdr x)))))
       :exec (cdr (cdr (cdr (cdr x))))))

Theorem: parse-options-p-compound-recognizer

(defthm parse-options-p-compound-recognizer
  (implies (parse-options-p x) (consp x))
  :rule-classes :compound-recognizer)

Theorem: parse-options-acl2-count

(defthm parse-options-acl2-count
  (equal (acl2-count (parse-options type strict-paren strict-brace
                                    strict-repeat case-insensitive))
         (+ 5 (acl2-count type)
            (acl2-count strict-paren)
            (acl2-count strict-brace)
            (acl2-count strict-repeat)
            (acl2-count case-insensitive))))

Theorem: parse-options-type-acl2-count

(defthm parse-options-type-acl2-count
  (implies (parse-options-p x)
           (< (acl2-count (parse-options-type x))
              (acl2-count x)))
  :rule-classes (:rewrite :linear))

Theorem: parse-options-strict-paren-acl2-count

(defthm parse-options-strict-paren-acl2-count
  (implies (parse-options-p x)
           (< (acl2-count (parse-options-strict-paren x))
              (acl2-count x)))
  :rule-classes (:rewrite :linear))

Theorem: parse-options-strict-brace-acl2-count

(defthm parse-options-strict-brace-acl2-count
  (implies (parse-options-p x)
           (< (acl2-count (parse-options-strict-brace x))
              (acl2-count x)))
  :rule-classes (:rewrite :linear))

Theorem: parse-options-strict-repeat-acl2-count

(defthm parse-options-strict-repeat-acl2-count
  (implies (parse-options-p x)
           (< (acl2-count (parse-options-strict-repeat x))
              (acl2-count x)))
  :rule-classes (:rewrite :linear))

Theorem: parse-options-case-insensitive-acl2-count

(defthm parse-options-case-insensitive-acl2-count
  (implies (parse-options-p x)
           (< (acl2-count (parse-options-case-insensitive x))
              (acl2-count x)))
  :rule-classes (:rewrite :linear))

Theorem: not-parse-options-p-parse-options-type

(defthm not-parse-options-p-parse-options-type
  (implies (not (parse-options-p x))
           (equal (parse-options-type x) nil)))

Theorem: not-parse-options-p-parse-options-strict-paren

(defthm not-parse-options-p-parse-options-strict-paren
  (implies (not (parse-options-p x))
           (equal (parse-options-strict-paren x)
                  nil)))

Theorem: not-parse-options-p-parse-options-strict-brace

(defthm not-parse-options-p-parse-options-strict-brace
  (implies (not (parse-options-p x))
           (equal (parse-options-strict-brace x)
                  nil)))

Theorem: not-parse-options-p-parse-options-strict-repeat

(defthm not-parse-options-p-parse-options-strict-repeat
  (implies (not (parse-options-p x))
           (equal (parse-options-strict-repeat x)
                  nil)))

Theorem: not-parse-options-p-parse-options-case-insensitive

(defthm not-parse-options-p-parse-options-case-insensitive
  (implies (not (parse-options-p x))
           (equal (parse-options-case-insensitive x)
                  nil)))

Theorem: parse-options-p-parse-options

(defthm parse-options-p-parse-options
  (parse-options-p (parse-options type strict-paren strict-brace
                                  strict-repeat case-insensitive)))

Theorem: parse-options-elim

(defthm parse-options-elim
  (implies (parse-options-p x)
           (equal (parse-options (parse-options-type x)
                                 (parse-options-strict-paren x)
                                 (parse-options-strict-brace x)
                                 (parse-options-strict-repeat x)
                                 (parse-options-case-insensitive x))
                  x))
  :rule-classes (:rewrite :elim))

Theorem: parse-options-type-parse-options

(defthm parse-options-type-parse-options
  (equal (parse-options-type
              (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive))
         type))

Theorem: parse-options-not-equal-type

(defthm parse-options-not-equal-type
  (not (equal (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive)
              type)))

Theorem: parse-options-not-equal-parse-options-type

(defthm parse-options-not-equal-parse-options-type
  (implies (parse-options-p x)
           (not (equal (parse-options-type x) x))))

Theorem: difference-type-parse-options

(defthm difference-type-parse-options
 (implies (not (equal type (parse-options-type x)))
          (not (equal (parse-options type strict-paren strict-brace
                                     strict-repeat case-insensitive)
                      x))))

Theorem: parse-options-strict-paren-parse-options

(defthm parse-options-strict-paren-parse-options
  (equal (parse-options-strict-paren
              (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive))
         strict-paren))

Theorem: parse-options-not-equal-strict-paren

(defthm parse-options-not-equal-strict-paren
  (not (equal (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive)
              strict-paren)))

Theorem: parse-options-not-equal-parse-options-strict-paren

(defthm parse-options-not-equal-parse-options-strict-paren
  (implies (parse-options-p x)
           (not (equal (parse-options-strict-paren x)
                       x))))

Theorem: difference-strict-paren-parse-options

(defthm difference-strict-paren-parse-options
 (implies (not (equal strict-paren
                      (parse-options-strict-paren x)))
          (not (equal (parse-options type strict-paren strict-brace
                                     strict-repeat case-insensitive)
                      x))))

Theorem: parse-options-strict-brace-parse-options

(defthm parse-options-strict-brace-parse-options
  (equal (parse-options-strict-brace
              (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive))
         strict-brace))

Theorem: parse-options-not-equal-strict-brace

(defthm parse-options-not-equal-strict-brace
  (not (equal (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive)
              strict-brace)))

Theorem: parse-options-not-equal-parse-options-strict-brace

(defthm parse-options-not-equal-parse-options-strict-brace
  (implies (parse-options-p x)
           (not (equal (parse-options-strict-brace x)
                       x))))

Theorem: difference-strict-brace-parse-options

(defthm difference-strict-brace-parse-options
 (implies (not (equal strict-brace
                      (parse-options-strict-brace x)))
          (not (equal (parse-options type strict-paren strict-brace
                                     strict-repeat case-insensitive)
                      x))))

Theorem: parse-options-strict-repeat-parse-options

(defthm parse-options-strict-repeat-parse-options
  (equal (parse-options-strict-repeat
              (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive))
         strict-repeat))

Theorem: parse-options-not-equal-strict-repeat

(defthm parse-options-not-equal-strict-repeat
  (not (equal (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive)
              strict-repeat)))

Theorem: parse-options-not-equal-parse-options-strict-repeat

(defthm parse-options-not-equal-parse-options-strict-repeat
  (implies (parse-options-p x)
           (not (equal (parse-options-strict-repeat x)
                       x))))

Theorem: difference-strict-repeat-parse-options

(defthm difference-strict-repeat-parse-options
 (implies (not (equal strict-repeat
                      (parse-options-strict-repeat x)))
          (not (equal (parse-options type strict-paren strict-brace
                                     strict-repeat case-insensitive)
                      x))))

Theorem: parse-options-case-insensitive-parse-options

(defthm parse-options-case-insensitive-parse-options
  (equal (parse-options-case-insensitive
              (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive))
         case-insensitive))

Theorem: parse-options-not-equal-case-insensitive

(defthm parse-options-not-equal-case-insensitive
  (not (equal (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive)
              case-insensitive)))

Theorem: parse-options-not-equal-parse-options-case-insensitive

(defthm parse-options-not-equal-parse-options-case-insensitive
  (implies (parse-options-p x)
           (not (equal (parse-options-case-insensitive x)
                       x))))

Theorem: difference-case-insensitive-parse-options

(defthm difference-case-insensitive-parse-options
 (implies (not (equal case-insensitive
                      (parse-options-case-insensitive x)))
          (not (equal (parse-options type strict-paren strict-brace
                                     strict-repeat case-insensitive)
                      x))))

Function: parse-opts-p

(defun parse-opts-p (x)
  (declare (xargs :guard t))
  (pattern-match x
                 ((parse-options type strict-paren strict-brace
                                 strict-repeat case-insensitive)
                  (and (parse-type-p type)
                       (booleanp strict-paren)
                       (booleanp strict-brace)
                       (booleanp strict-repeat)
                       (booleanp case-insensitive)))))

Theorem: parse-opts-compound-recognizer

(defthm parse-opts-compound-recognizer
  (implies (parse-opts-p x) (consp x))
  :rule-classes :compound-recognizer)

Theorem: parse-opts-possibilities

(defthm parse-opts-possibilities
  (implies (parse-opts-p x)
           (parse-options-p x))
  :rule-classes :forward-chaining)

Theorem: parse-opts-parse-options-accessor-types

(defthm parse-opts-parse-options-accessor-types
  (implies (and (parse-opts-p x)
                (parse-options-p x))
           (and (parse-type-p (parse-options-type x))
                (booleanp (parse-options-strict-paren x))
                (booleanp (parse-options-strict-brace x))
                (booleanp (parse-options-strict-repeat x))
                (booleanp (parse-options-case-insensitive x)))))

Theorem: parse-options-not-parse-opts

(defthm parse-options-not-parse-opts
 (implies
      (and (parse-options-p x)
           (or (not (parse-type-p (parse-options-type x)))
               (not (booleanp (parse-options-strict-paren x)))
               (not (booleanp (parse-options-strict-brace x)))
               (not (booleanp (parse-options-strict-repeat x)))
               (not (booleanp (parse-options-case-insensitive x)))))
      (not (parse-opts-p x))))

Theorem: parse-opts-p-parse-options

(defthm parse-opts-p-parse-options
  (iff (parse-opts-p (parse-options type strict-paren strict-brace
                                    strict-repeat case-insensitive))
       (and (parse-type-p type)
            (booleanp strict-paren)
            (booleanp strict-brace)
            (booleanp strict-repeat)
            (booleanp case-insensitive))))

Theorem: parse-options-p-product-type

(defthm parse-options-p-product-type
  (implies (parse-options-p x)
           (equal (product-type x)
                  'parse-options)))

Theorem: product-type-parse-options-p

(defthm product-type-parse-options-p
  (implies (not (equal (product-type x) 'parse-options))
           (not (parse-options-p x))))

Theorem: parse-options-product-type

(defthm parse-options-product-type
  (equal
       (product-type (parse-options type strict-paren strict-brace
                                    strict-repeat case-insensitive))
       'parse-options))

Theorem: parse-options-equal-product-type

(defthm parse-options-equal-product-type
 (implies
  (not
   (equal
       (product-type (parse-options type strict-paren strict-brace
                                    strict-repeat case-insensitive))
       (product-type x)))
  (not (equal (parse-options type strict-paren strict-brace
                             strict-repeat case-insensitive)
              x))))

Function: parse-opts-measure

(defun parse-opts-measure (x)
  (declare (xargs :guard t) (ignore x))
  (pattern-match x (& 1)))