/usr/share/acl2-4.3/books/regex/regex-defs.lisp is in acl2-books-source 4.3-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 | (in-package "ACL2")
;; (local (include-book "defsum-thms"))
;; (include-book "defsum")
(include-book "tools/defsum" :dir :system)
(defmacro range-start (x) `(cadr ,x))
(defmacro range-end (x) `(caddr ,x))
#||
;; Depend on arithmetic since defsum uses it.
(include-book "arithmetic/top-with-meta" :dir :system)
||#
;; Checks whether x is a valid element to include in a charset.
;; either a character or ('range char char).
(defun charset-memberp (x)
(declare (xargs :guard t))
(cond
((characterp x) t)
(t (and (consp x)
(consp (cdr x))
(consp (cddr x))
(equal (car x) 'range)
(characterp (range-start x))
(characterp (range-end x))))))
;; Is x composed of valid charset-members
;; A little bit less restrictive than we'll use because
;; it allows "not" to occur anywhere; a real parsed regex
;; will only have "not" occurring first
(defun charsetp (x)
(declare (xargs :guard t))
(if (atom x)
(equal x nil)
(and (or (equal (car x) 'not)
(charset-memberp (car x)))
(charsetp (cdr x)))))
(defsum regex
; :guard :fast
(r-disjunct (regex-p left) (regex-p right))
(r-concat (regex-p left) (regex-p right))
(r-exact (characterp val))
(r-charset (charsetp set))
(r-any)
(r-empty)
(r-nomatch)
(r-end)
(r-begin)
(r-repeat (regex-p regex) (integerp min) (integerp max))
(r-group (regex-p regex) (natp index))
(r-backref (natp index)))
;;(in-theory (enable regex-executable-counterparts))
;; (defmacro regex-match (input &rest clauses)
;; (make-pattern-match input clauses
;; (append *regex-types-pattern-match-alist*
;; *basic-constructor-alist*)))
(defun parse-type-p (x)
(declare (xargs :guard t))
(and (symbolp x) ;; GNU regular expressions -- see GNU documentation
(or (eq x 'bre) ;; Basic regular expressions
(eq x 'ere) ;; Extended regular expressions
(eq x 'fixed) ;; Fixed (no character is special) string
)))
(set-bogus-defun-hints-ok t) ;; For non-recursive function ignore the (ACL2) hints.
(defsum parse-opts
; :guard :fast
(parse-options
(parse-type-p type)
(booleanp strict-paren)
(booleanp strict-brace)
(booleanp strict-repeat)
(booleanp case-insensitive)))
; Makes parsing options (parse-opts) structure.
(defmacro make-parse-opts
(&key (type 'ere)
strict-paren
strict-brace
strict-repeat
case-insensitive
)
`(parse-options ',type
',strict-paren
',strict-brace
',strict-repeat
',case-insensitive))
(defthm parse-opts-type-possibilities
(implies (and (parse-opts-p x)
(not (equal (parse-options-type x) 'bre))
(not (equal (parse-options-type x) 'ere)))
(equal (parse-options-type x) 'fixed))
:hints (("Goal" :cases ((parse-options-p x)))
("Subgoal 1" :in-theory (disable parse-opts-possibilities))))
(defthm parse-options-parse-opts
(implies (parse-opts-p x)
(parse-options-p x)))
;;(in-theory (enable parse-options-executable-counterparts))
;; (defthm len-cdr (<= (len (cdr x)) (len x))
;; :rule-classes
;; (:rewrite
;; (:forward-chaining :trigger-terms ((len (cdr x))))))
|