/usr/share/acl2-6.3/books/regex/regex-defs.cert is in acl2-books-certs 6.3-5.
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 121 122 123 124 125 126 127 128 129 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
(DEFPKG "ACL2-CRG" (SET-DIFFERENCE-EQUAL (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (ZERO))) NIL ((:SYSTEM . "arithmetic/equalities.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "arithmetic/top-with-meta.lisp")) T)
(DEFPKG "ACL2-AGP" (SET-DIFFERENCE-EQUAL (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (ZERO))) NIL ((:SYSTEM . "arithmetic/equalities.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "arithmetic/top-with-meta.lisp")) T)
(DEFPKG "ACL2-ASG" (SET-DIFFERENCE-EQUAL (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (ZERO))) NIL ((:SYSTEM . "arithmetic/equalities.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "arithmetic/top-with-meta.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((10 RECORD-EXPANSION (DEFSECTION PARSE-OPTIONS :PARENTS (REGEX) :SHORT "Generate options for using regular expressions to parse/match
strings" :LONG "<p>General form:</p>
@({
(parse-options parse-type
strict-paren
strict-brace
strict-repeat
case-insensitive)
})
<p><tt>Parse-type</tt> should be one of <tt>'ere</tt>, <tt>'bre</tt>, or
<tt>'fixed</tt>. 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.</p>
<p><tt>Strict-paren</tt>, <tt>strict-brace</tt>, and <tt>strict-repeat</tt>,
and <tt>case-insensitive</tt> are @('booleanp') values.</p>
<p>BOZO: document strict-paren, strict-brace, and strict-repeat.</p>" (DEFSUM PARSE-OPTS (PARSE-OPTIONS (PARSE-TYPE-P TYPE) (BOOLEANP STRICT-PAREN) (BOOLEANP STRICT-BRACE) (BOOLEANP STRICT-REPEAT) (BOOLEANP CASE-INSENSITIVE)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE PARSE-OPTIONS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFSUM PARSE-OPTS (PARSE-OPTIONS (PARSE-TYPE-P TYPE) (BOOLEANP STRICT-PAREN) (BOOLEANP STRICT-BRACE) (BOOLEANP STRICT-REPEAT) (BOOLEANP CASE-INSENSITIVE))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE PARSE-OPTIONS)) (XDOC::PARENTS (QUOTE (REGEX))) (XDOC::SHORT (QUOTE "Generate options for using regular expressions to parse/match
strings")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE PARSE-OPTIONS))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>General form:</p>
@({
(parse-options parse-type
strict-paren
strict-brace
strict-repeat
case-insensitive)
})
<p><tt>Parse-type</tt> should be one of <tt>'ere</tt>, <tt>'bre</tt>, or
<tt>'fixed</tt>. 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.</p>
<p><tt>Strict-paren</tt>, <tt>strict-brace</tt>, and <tt>strict-repeat</tt>,
and <tt>case-insensitive</tt> are @('booleanp') values.</p>
<p>BOZO: document strict-paren, strict-brace, and strict-repeat.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . PARSE-OPTIONS) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS REGEX) (:SHORT . "Generate options for using regular expressions to parse/match
strings") (:LONG . "<p>General form:</p>
@({
(parse-options parse-type
strict-paren
strict-brace
strict-repeat
case-insensitive)
})
<p><tt>Parse-type</tt> should be one of <tt>'ere</tt>, <tt>'bre</tt>, or
<tt>'fixed</tt>. 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.</p>
<p><tt>Strict-paren</tt>, <tt>strict-brace</tt>, and <tt>strict-repeat</tt>,
and <tt>case-insensitive</tt> are @('booleanp') values.</p>
<p>BOZO: document strict-paren, strict-brace, and strict-repeat.</p>
<h3>Definitions and Theorems</h3>@(def |ACL2|::|PARSE-OPTIONS-P|)
@(def |ACL2|::|PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-TYPE|)
@(def |ACL2|::|PARSE-OPTIONS-STRICT-PAREN|)
@(def |ACL2|::|PARSE-OPTIONS-STRICT-BRACE|)
@(def |ACL2|::|PARSE-OPTIONS-STRICT-REPEAT|)
@(def |ACL2|::|PARSE-OPTIONS-CASE-INSENSITIVE|)
@(def |ACL2|::|PARSE-OPTIONS-P-COMPOUND-RECOGNIZER|)
@(def |ACL2|::|PARSE-OPTIONS-ACL2-COUNT|)
@(def |ACL2|::|PARSE-OPTIONS-TYPE-ACL2-COUNT|)
@(def |ACL2|::|PARSE-OPTIONS-STRICT-PAREN-ACL2-COUNT|)
@(def |ACL2|::|PARSE-OPTIONS-STRICT-BRACE-ACL2-COUNT|)
@(def |ACL2|::|PARSE-OPTIONS-STRICT-REPEAT-ACL2-COUNT|)
@(def |ACL2|::|PARSE-OPTIONS-CASE-INSENSITIVE-ACL2-COUNT|)
@(def |ACL2|::|NOT-PARSE-OPTIONS-P-PARSE-OPTIONS-TYPE|)
@(def |ACL2|::|NOT-PARSE-OPTIONS-P-PARSE-OPTIONS-STRICT-PAREN|)
@(def |ACL2|::|NOT-PARSE-OPTIONS-P-PARSE-OPTIONS-STRICT-BRACE|)
@(def |ACL2|::|NOT-PARSE-OPTIONS-P-PARSE-OPTIONS-STRICT-REPEAT|)
@(def |ACL2|::|NOT-PARSE-OPTIONS-P-PARSE-OPTIONS-CASE-INSENSITIVE|)
@(def |ACL2|::|PARSE-OPTIONS-P-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-ELIM|)
@(def |ACL2|::|PARSE-OPTIONS-TYPE-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-TYPE|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-PARSE-OPTIONS-TYPE|)
@(def |ACL2|::|DIFFERENCE-TYPE-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-STRICT-PAREN-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-STRICT-PAREN|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-PARSE-OPTIONS-STRICT-PAREN|)
@(def |ACL2|::|DIFFERENCE-STRICT-PAREN-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-STRICT-BRACE-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-STRICT-BRACE|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-PARSE-OPTIONS-STRICT-BRACE|)
@(def |ACL2|::|DIFFERENCE-STRICT-BRACE-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-STRICT-REPEAT-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-STRICT-REPEAT|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-PARSE-OPTIONS-STRICT-REPEAT|)
@(def |ACL2|::|DIFFERENCE-STRICT-REPEAT-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-CASE-INSENSITIVE-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-CASE-INSENSITIVE|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-EQUAL-PARSE-OPTIONS-CASE-INSENSITIVE|)
@(def |ACL2|::|DIFFERENCE-CASE-INSENSITIVE-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTS-P|)
@(def |ACL2|::|PARSE-OPTS-COMPOUND-RECOGNIZER|)
@(def |ACL2|::|PARSE-OPTS-POSSIBILITIES|)
@(def |ACL2|::|PARSE-OPTS-PARSE-OPTIONS-ACCESSOR-TYPES|)
@(def |ACL2|::|PARSE-OPTIONS-NOT-PARSE-OPTS|)
@(def |ACL2|::|PARSE-OPTS-P-PARSE-OPTIONS|)
@(def |ACL2|::|PARSE-OPTIONS-P-PRODUCT-TYPE|)
@(def |ACL2|::|PRODUCT-TYPE-PARSE-OPTIONS-P|)
@(def |ACL2|::|PARSE-OPTIONS-PRODUCT-TYPE|)
@(def |ACL2|::|PARSE-OPTIONS-EQUAL-PRODUCT-TYPE|)
@(def |ACL2|::|PARSE-OPTS-MEASURE|)") (:FROM . "[books]/regex/regex-defs.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC PARSE-OPTIONS)))))) (VALUE-TRIPLE (QUOTE PARSE-OPTIONS))))))
(("/usr/share/acl2-6.3/books/regex/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 390361791) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
(("/usr/share/acl2-6.3/books/regex/regex-defs.lisp" "regex-defs" "regex-defs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1054214948) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-equal.lisp" "meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948431900)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-lemmas.lisp" "term-lemmas" "term-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 304413851)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1403689963)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/mod-gcd.lisp" "mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1629957550)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2140150970)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/nat-listp.lisp" "nat-listp" "nat-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1767896370)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1775556314)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761519866)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2007324914)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1939433116)) ("/usr/share/acl2-6.3/books/tools/defsum.lisp" "tools/defsum" "defsum" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1829289372) ("/usr/share/acl2-6.3/books/tools/types-misc.lisp" "types-misc" "types-misc" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 741554513) ("/usr/share/acl2-6.3/books/tools/theory-tools.lisp" "theory-tools" "theory-tools" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1192579963) ("/usr/share/acl2-6.3/books/tools/pattern-match.lisp" "pattern-match" "pattern-match" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1646398624) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/regex/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 390361791) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
264439742
|