acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / regex / regex-ui.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((7 RECORD-EXPANSION (DEFXDOC REGEX :SHORT "Regular expression library for ACL2" :LONG "<p>This library is modeled after the regular expression parsing
         functionality of GNU grep.  While the code is mostly considered to be
         complete enough for now, we invite those who wish to improve the
         documentation to go ahead and do so.  As of March 2013, this library
         is compliant with 579 of the 646 GNU grep regression suite tests (see
         book regex/regex-tests for those tests).</p>

         <p>To start using the regex library, include book
         <tt>regex/regex-ui</tt>.</p>

         <p>This library supports \"Basic\", \"Extended\", and \"Fixed\"
         regular expressions (see @(see parse-options)).  Although some
         implementations of GNU Grep support \"Perl\" regular expressions, we
         do not yet implement them.  If a user is motivated to provide such an
         extension, they should feel free to do so.</p>

         <p>This library does not currently support features like [[:digit:]] and
         [[:alpha:]].  A workaround for this is specifying the expansion of
         these named classes, respectively, as in [0-9] and [a-zA-Z].</p>

         <p>See <a
         href=\"http://www.gnu.org/software/grep/manual/grep.html#Regular-Expressions\">
         GNU Grep Regular Expressions</a> for more information on these regular
         expressions.</p>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . REGEX) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS) (:SHORT . "Regular expression library for ACL2") (:LONG . "<p>This library is modeled after the regular expression parsing
         functionality of GNU grep.  While the code is mostly considered to be
         complete enough for now, we invite those who wish to improve the
         documentation to go ahead and do so.  As of March 2013, this library
         is compliant with 579 of the 646 GNU grep regression suite tests (see
         book regex/regex-tests for those tests).</p>

         <p>To start using the regex library, include book
         <tt>regex/regex-ui</tt>.</p>

         <p>This library supports \"Basic\", \"Extended\", and \"Fixed\"
         regular expressions (see @(see parse-options)).  Although some
         implementations of GNU Grep support \"Perl\" regular expressions, we
         do not yet implement them.  If a user is motivated to provide such an
         extension, they should feel free to do so.</p>

         <p>This library does not currently support features like [[:digit:]] and
         [[:alpha:]].  A workaround for this is specifying the expansion of
         these named classes, respectively, as in [0-9] and [a-zA-Z].</p>

         <p>See <a
         href=\"http://www.gnu.org/software/grep/manual/grep.html#Regular-Expressions\">
         GNU Grep Regular Expressions</a> for more information on these regular
         expressions.</p>") (:FROM . "[books]/regex/regex-ui.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC REGEX)))))) (14 RECORD-EXPANSION (DEFINE DO-REGEX-MATCH-PRECOMP ((STR STRINGP "String to test") (REGEX REGEX-P "Regular expression specifying the pattern to find") (OPTS PARSE-OPTS-P "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.")) :SHORT "Test whether a given string matches a given regular expression" :LONG "Intended for use during macroexpansion, as occurs in @(see B*)." :PARENTS (REGEX) :RETURNS (MV (WHOLE (OR (STRINGP WHOLE) (NOT WHOLE)) "The portion of <tt>str</tt> that matches the pattern
                       provided by <tt>regex</tt>.  <tt>Nil</tt> if there is
                       not a match." :RULE-CLASSES :TYPE-PRESCRIPTION) (SUBSTRS TRUE-LISTP "List of substrings that match parenthesized
                         subexpressions of the pattern (when applicable).
                         <tt>Nil</tt> if there is not a match." :RULE-CLASSES :TYPE-PRESCRIPTION)) (B* ((STR (MBE :LOGIC (IF (STRINGP STR) STR "") :EXEC STR)) (TRANSSTR (IF (PARSE-OPTIONS-CASE-INSENSITIVE OPTS) (STR::DOWNCASE-STRING STR) STR)) ((MV ?MATCHP WHOLE SUBSTRS) (MATCH-REGEX REGEX TRANSSTR STR))) (MV WHOLE SUBSTRS))) (PROGN (RECORD-EXPANSION (DEFSECTION DO-REGEX-MATCH-PRECOMP :PARENTS (REGEX) :SHORT "Test whether a given string matches a given regular expression" :LONG "Intended for use during macroexpansion, as occurs in @(see B*)." (DEFUND DO-REGEX-MATCH-PRECOMP (STR REGEX OPTS) (DECLARE (XARGS :GUARD (AND (STRINGP STR) (REGEX-P REGEX) (PARSE-OPTS-P OPTS)))) (LET ((__FUNCTION__ (QUOTE DO-REGEX-MATCH-PRECOMP))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((STR (MBE :LOGIC (IF (STRINGP STR) STR "") :EXEC STR)) (TRANSSTR (IF (PARSE-OPTIONS-CASE-INSENSITIVE OPTS) (STR::DOWNCASE-STRING STR) STR)) ((MV ?MATCHP WHOLE SUBSTRS) (MATCH-REGEX REGEX TRANSSTR STR))) (MV WHOLE SUBSTRS)))) (CUTIL::EXTEND-DEFINE-TABLE DO-REGEX-MATCH-PRECOMP :FN (QUOTE DO-REGEX-MATCH-PRECOMP) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                       provided by <tt>regex</tt>.  <tt>Nil</tt> if there is
                       not a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                         subexpressions of the pattern (when applicable).
                         <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to test") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . REGEX) (GUARD REGEX-P REGEX) (DOC . "Regular expression specifying the pattern to find") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OPTS) (GUARD PARSE-OPTS-P OPTS) (DOC . "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE DO-REGEX-MATCH-PRECOMP) (W STATE)) (QUOTE (IN-THEORY (ENABLE DO-REGEX-MATCH-PRECOMP))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE DO-REGEX-MATCH-PRECOMP) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                       provided by <tt>regex</tt>.  <tt>Nil</tt> if there is
                       not a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                         subexpressions of the pattern (when applicable).
                         <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE DO-REGEX-MATCH-PRECOMP)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND DO-REGEX-MATCH-PRECOMP (STR REGEX OPTS) (DECLARE (XARGS :GUARD (AND (STRINGP STR) (REGEX-P REGEX) (PARSE-OPTS-P OPTS)))) (LET ((__FUNCTION__ (QUOTE DO-REGEX-MATCH-PRECOMP))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((STR (MBE :LOGIC (IF (STRINGP STR) STR "") :EXEC STR)) (TRANSSTR (IF (PARSE-OPTIONS-CASE-INSENSITIVE OPTS) (STR::DOWNCASE-STRING STR) STR)) ((MV ?MATCHP WHOLE SUBSTRS) (MATCH-REGEX REGEX TRANSSTR STR))) (MV WHOLE SUBSTRS)))) (CUTIL::EXTEND-DEFINE-TABLE DO-REGEX-MATCH-PRECOMP :FN (QUOTE DO-REGEX-MATCH-PRECOMP) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                       provided by <tt>regex</tt>.  <tt>Nil</tt> if there is
                       not a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                         subexpressions of the pattern (when applicable).
                         <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to test") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . REGEX) (GUARD REGEX-P REGEX) (DOC . "Regular expression specifying the pattern to find") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OPTS) (GUARD PARSE-OPTS-P OPTS) (DOC . "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE DO-REGEX-MATCH-PRECOMP) (W STATE)) (QUOTE (IN-THEORY (ENABLE DO-REGEX-MATCH-PRECOMP))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE DO-REGEX-MATCH-PRECOMP) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                       provided by <tt>regex</tt>.  <tt>Nil</tt> if there is
                       not a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                         subexpressions of the pattern (when applicable).
                         <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND DO-REGEX-MATCH-PRECOMP (STR REGEX OPTS) (DECLARE (XARGS :GUARD (AND (STRINGP STR) (REGEX-P REGEX) (PARSE-OPTS-P OPTS)))) (LET ((__FUNCTION__ (QUOTE DO-REGEX-MATCH-PRECOMP))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((STR (MBE :LOGIC (IF (STRINGP STR) STR "") :EXEC STR)) (TRANSSTR (IF (PARSE-OPTIONS-CASE-INSENSITIVE OPTS) (STR::DOWNCASE-STRING STR) STR)) ((MV ?MATCHP WHOLE SUBSTRS) (MATCH-REGEX REGEX TRANSSTR STR))) (MV WHOLE SUBSTRS)))) (CUTIL::EXTEND-DEFINE-TABLE DO-REGEX-MATCH-PRECOMP :FN (QUOTE DO-REGEX-MATCH-PRECOMP) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                       provided by <tt>regex</tt>.  <tt>Nil</tt> if there is
                       not a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                         subexpressions of the pattern (when applicable).
                         <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to test") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . REGEX) (GUARD REGEX-P REGEX) (DOC . "Regular expression specifying the pattern to find") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OPTS) (GUARD PARSE-OPTS-P OPTS) (DOC . "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE DO-REGEX-MATCH-PRECOMP) (W STATE)) (QUOTE (IN-THEORY (ENABLE DO-REGEX-MATCH-PRECOMP))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE DO-REGEX-MATCH-PRECOMP) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                       provided by <tt>regex</tt>.  <tt>Nil</tt> if there is
                       not a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                         subexpressions of the pattern (when applicable).
                         <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM RETURN-TYPE-OF-DO-REGEX-MATCH-PRECOMP.WHOLE (B* (((MV ?WHOLE ?SUBSTRS) (DO-REGEX-MATCH-PRECOMP STR REGEX OPTS))) (OR (STRINGP WHOLE) (NOT WHOLE))) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM RETURN-TYPE-OF-DO-REGEX-MATCH-PRECOMP.SUBSTRS (B* (((MV ?WHOLE ?SUBSTRS) (DO-REGEX-MATCH-PRECOMP STR REGEX OPTS))) (TRUE-LISTP SUBSTRS)) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE DO-REGEX-MATCH-PRECOMP)) (XDOC::PARENTS (QUOTE (REGEX))) (XDOC::SHORT (QUOTE "Test whether a given string matches a given regular expression")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE DO-REGEX-MATCH-PRECOMP))) 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 "Intended for use during macroexpansion, as occurs in @(see B*).") (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 . DO-REGEX-MATCH-PRECOMP) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS REGEX) (:SHORT . "Test whether a given string matches a given regular expression") (:LONG . "Intended for use during macroexpansion, as occurs in @(see B*).

<h3>Definitions and Theorems</h3>@(def |ACL2|::|DO-REGEX-MATCH-PRECOMP|)
@(def |ACL2|::|RETURN-TYPE-OF-DO-REGEX-MATCH-PRECOMP.WHOLE|)
@(def |ACL2|::|RETURN-TYPE-OF-DO-REGEX-MATCH-PRECOMP.SUBSTRS|)") (:FROM . "[books]/regex/regex-ui.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC DO-REGEX-MATCH-PRECOMP)))))) (VALUE-TRIPLE (QUOTE DO-REGEX-MATCH-PRECOMP))))) (RECORD-EXPANSION (MAKE-EVENT (B* ((CUTIL::CURRENT-PKG (F-GET-GLOBAL (QUOTE CURRENT-PACKAGE) STATE)) (CUTIL::BASE-PKG (PKG-WITNESS CUTIL::CURRENT-PKG)) (CUTIL::FNNAME (QUOTE DO-REGEX-MATCH-PRECOMP)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE DO-REGEX-MATCH-PRECOMP) (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to test") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . REGEX) (GUARD REGEX-P REGEX) (DOC . "Regular expression specifying the pattern to find") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OPTS) (GUARD PARSE-OPTS-P OPTS) (DOC . "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                       provided by <tt>regex</tt>.  <tt>Nil</tt> if there is
                       not a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                         subexpressions of the pattern (when applicable).
                         <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) CUTIL::BASE-PKG STATE)) (EVENT (LIST (QUOTE XDOC::XDOC-PREPEND) CUTIL::FNNAME CUTIL::STR))) (VALUE EVENT))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE DO-REGEX-MATCH-PRECOMP) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING:  Ignoring attempt to prepend to topic ~x0, ~
                         because no such topic is currently defined.~%" (QUOTE DO-REGEX-MATCH-PRECOMP)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) "<box><dl>
<dt>Signature</dt><dt><code>(do-regex-match-precomp str regex opts) &rarr; (mv whole substrs)</code></dt><dt>Arguments</dt><dd><tt>str</tt> &mdash; String to test.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp str)').</color></dd>
<dd><tt>regex</tt> &mdash; Regular expression specifying the pattern to find.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(regex-p regex)').</color></dd>
<dd><tt>opts</tt> &mdash; Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(parse-opts-p opts)').</color></dd>
<dt>Returns</dt><dd><tt>whole</tt> &mdash; The portion of <tt>str</tt> that matches the pattern
                       provided by <tt>regex</tt>.  <tt>Nil</tt> if there is
                       not a match.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(or (stringp whole) (not whole))').</color></dd>
<dd><tt>substrs</tt> &mdash; List of substrings that match parenthesized
                         subexpressions of the pattern (when applicable).
                         <tt>Nil</tt> if there is not a match.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(true-listp substrs)').</color></dd>
</dl></box>
" XDOC::OLD-LONG)) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))))) (15 RECORD-EXPANSION (DEFINE DO-REGEX-MATCH ((STR STRINGP "String to test") (PAT STRINGP "String representing the pattern to find") (OPTS PARSE-OPTS-P "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.")) :SHORT "Test whether a given string matches a given regular expression" :LONG "<p>Intended for use in the dynamically compiled case.</p>



<p>As examples:</p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"cdeabfdefdeghij\"
                (parse-options 'fixed ; type
                                nil  ; not strict-paren
                                nil  ; not strict-brace
                                nil  ; not strict-repeat
                                t    ; case-insensitive
                                ))
})

<p>returns <tt>(mv nil \"cdeAbfdEfDeghIj\" nil)</tt>, </p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"ab([def]*)\\1([gh])\"
                 (parse-options 'fixed nil nil nil t))
}) 

<p>returns <tt>(mv nil nil nil)</tt>, and </p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"ab([def]*)\\1([gh])\"
                 (parse-options 'ere nil nil nil t))
})

<p>returns <tt>(mv nil \"AbfdEfDeg\" (\"fdE\" \"g\"))</tt>.</p>" :PARENTS (REGEX) :RETURNS (MV (ERROR-MSG (OR (STRINGP ERROR-MSG) (NOT ERROR-MSG)) "Error message" :RULE-CLASSES :TYPE-PRESCRIPTION) (WHOLE (OR (STRINGP WHOLE) (NOT WHOLE)) "The portion of <tt>str</tt> that matches the pattern
                        provided by <tt>pat</tt>.  <tt>Nil</tt> if there is not
                        a match." :RULE-CLASSES :TYPE-PRESCRIPTION) (SUBSTRS TRUE-LISTP "List of substrings that match parenthesized
                          subexpressions of the pattern (when applicable).
                          <tt>Nil</tt> if there is not a match." :RULE-CLASSES :TYPE-PRESCRIPTION)) (B* ((STR (MBE :LOGIC (IF (STRINGP STR) STR "") :EXEC STR)) (PAT (MBE :LOGIC (IF (STRINGP PAT) PAT "") :EXEC PAT)) (PAT (IF (PARSE-OPTIONS-CASE-INSENSITIVE OPTS) (STR::DOWNCASE-STRING PAT) PAT)) (REGEX (REGEX-DO-PARSE PAT OPTS)) ((WHEN (STRINGP REGEX)) (MV REGEX NIL NIL)) ((MV WHOLE SUBSTRS) (DO-REGEX-MATCH-PRECOMP STR REGEX OPTS))) (MV NIL WHOLE SUBSTRS))) (PROGN (RECORD-EXPANSION (DEFSECTION DO-REGEX-MATCH :PARENTS (REGEX) :SHORT "Test whether a given string matches a given regular expression" :LONG "<p>Intended for use in the dynamically compiled case.</p>



<p>As examples:</p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"cdeabfdefdeghij\"
                (parse-options 'fixed ; type
                                nil  ; not strict-paren
                                nil  ; not strict-brace
                                nil  ; not strict-repeat
                                t    ; case-insensitive
                                ))
})

<p>returns <tt>(mv nil \"cdeAbfdEfDeghIj\" nil)</tt>, </p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"ab([def]*)\\1([gh])\"
                 (parse-options 'fixed nil nil nil t))
}) 

<p>returns <tt>(mv nil nil nil)</tt>, and </p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"ab([def]*)\\1([gh])\"
                 (parse-options 'ere nil nil nil t))
})

<p>returns <tt>(mv nil \"AbfdEfDeg\" (\"fdE\" \"g\"))</tt>.</p>" (DEFUND DO-REGEX-MATCH (STR PAT OPTS) (DECLARE (XARGS :GUARD (AND (STRINGP STR) (STRINGP PAT) (PARSE-OPTS-P OPTS)))) (LET ((__FUNCTION__ (QUOTE DO-REGEX-MATCH))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((STR (MBE :LOGIC (IF (STRINGP STR) STR "") :EXEC STR)) (PAT (MBE :LOGIC (IF (STRINGP PAT) PAT "") :EXEC PAT)) (PAT (IF (PARSE-OPTIONS-CASE-INSENSITIVE OPTS) (STR::DOWNCASE-STRING PAT) PAT)) (REGEX (REGEX-DO-PARSE PAT OPTS)) ((WHEN (STRINGP REGEX)) (MV REGEX NIL NIL)) ((MV WHOLE SUBSTRS) (DO-REGEX-MATCH-PRECOMP STR REGEX OPTS))) (MV NIL WHOLE SUBSTRS)))) (CUTIL::EXTEND-DEFINE-TABLE DO-REGEX-MATCH :FN (QUOTE DO-REGEX-MATCH) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR-MSG) (DOC . "Error message") (CUTIL::RETURN-TYPE OR (STRINGP ERROR-MSG) (NOT ERROR-MSG)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                        provided by <tt>pat</tt>.  <tt>Nil</tt> if there is not
                        a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                          subexpressions of the pattern (when applicable).
                          <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to test") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . PAT) (GUARD STRINGP PAT) (DOC . "String representing the pattern to find") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OPTS) (GUARD PARSE-OPTS-P OPTS) (DOC . "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE DO-REGEX-MATCH) (W STATE)) (QUOTE (IN-THEORY (ENABLE DO-REGEX-MATCH))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE DO-REGEX-MATCH) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR-MSG) (DOC . "Error message") (CUTIL::RETURN-TYPE OR (STRINGP ERROR-MSG) (NOT ERROR-MSG)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                        provided by <tt>pat</tt>.  <tt>Nil</tt> if there is not
                        a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                          subexpressions of the pattern (when applicable).
                          <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE DO-REGEX-MATCH)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND DO-REGEX-MATCH (STR PAT OPTS) (DECLARE (XARGS :GUARD (AND (STRINGP STR) (STRINGP PAT) (PARSE-OPTS-P OPTS)))) (LET ((__FUNCTION__ (QUOTE DO-REGEX-MATCH))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((STR (MBE :LOGIC (IF (STRINGP STR) STR "") :EXEC STR)) (PAT (MBE :LOGIC (IF (STRINGP PAT) PAT "") :EXEC PAT)) (PAT (IF (PARSE-OPTIONS-CASE-INSENSITIVE OPTS) (STR::DOWNCASE-STRING PAT) PAT)) (REGEX (REGEX-DO-PARSE PAT OPTS)) ((WHEN (STRINGP REGEX)) (MV REGEX NIL NIL)) ((MV WHOLE SUBSTRS) (DO-REGEX-MATCH-PRECOMP STR REGEX OPTS))) (MV NIL WHOLE SUBSTRS)))) (CUTIL::EXTEND-DEFINE-TABLE DO-REGEX-MATCH :FN (QUOTE DO-REGEX-MATCH) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR-MSG) (DOC . "Error message") (CUTIL::RETURN-TYPE OR (STRINGP ERROR-MSG) (NOT ERROR-MSG)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                        provided by <tt>pat</tt>.  <tt>Nil</tt> if there is not
                        a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                          subexpressions of the pattern (when applicable).
                          <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to test") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . PAT) (GUARD STRINGP PAT) (DOC . "String representing the pattern to find") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OPTS) (GUARD PARSE-OPTS-P OPTS) (DOC . "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE DO-REGEX-MATCH) (W STATE)) (QUOTE (IN-THEORY (ENABLE DO-REGEX-MATCH))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE DO-REGEX-MATCH) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR-MSG) (DOC . "Error message") (CUTIL::RETURN-TYPE OR (STRINGP ERROR-MSG) (NOT ERROR-MSG)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                        provided by <tt>pat</tt>.  <tt>Nil</tt> if there is not
                        a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                          subexpressions of the pattern (when applicable).
                          <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND DO-REGEX-MATCH (STR PAT OPTS) (DECLARE (XARGS :GUARD (AND (STRINGP STR) (STRINGP PAT) (PARSE-OPTS-P OPTS)))) (LET ((__FUNCTION__ (QUOTE DO-REGEX-MATCH))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((STR (MBE :LOGIC (IF (STRINGP STR) STR "") :EXEC STR)) (PAT (MBE :LOGIC (IF (STRINGP PAT) PAT "") :EXEC PAT)) (PAT (IF (PARSE-OPTIONS-CASE-INSENSITIVE OPTS) (STR::DOWNCASE-STRING PAT) PAT)) (REGEX (REGEX-DO-PARSE PAT OPTS)) ((WHEN (STRINGP REGEX)) (MV REGEX NIL NIL)) ((MV WHOLE SUBSTRS) (DO-REGEX-MATCH-PRECOMP STR REGEX OPTS))) (MV NIL WHOLE SUBSTRS)))) (CUTIL::EXTEND-DEFINE-TABLE DO-REGEX-MATCH :FN (QUOTE DO-REGEX-MATCH) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR-MSG) (DOC . "Error message") (CUTIL::RETURN-TYPE OR (STRINGP ERROR-MSG) (NOT ERROR-MSG)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                        provided by <tt>pat</tt>.  <tt>Nil</tt> if there is not
                        a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                          subexpressions of the pattern (when applicable).
                          <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to test") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . PAT) (GUARD STRINGP PAT) (DOC . "String representing the pattern to find") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OPTS) (GUARD PARSE-OPTS-P OPTS) (DOC . "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE DO-REGEX-MATCH) (W STATE)) (QUOTE (IN-THEORY (ENABLE DO-REGEX-MATCH))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE DO-REGEX-MATCH) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR-MSG) (DOC . "Error message") (CUTIL::RETURN-TYPE OR (STRINGP ERROR-MSG) (NOT ERROR-MSG)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                        provided by <tt>pat</tt>.  <tt>Nil</tt> if there is not
                        a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                          subexpressions of the pattern (when applicable).
                          <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM RETURN-TYPE-OF-DO-REGEX-MATCH.ERROR-MSG (B* (((MV ?ERROR-MSG ?WHOLE ?SUBSTRS) (DO-REGEX-MATCH STR PAT OPTS))) (OR (STRINGP ERROR-MSG) (NOT ERROR-MSG))) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM RETURN-TYPE-OF-DO-REGEX-MATCH.WHOLE (B* (((MV ?ERROR-MSG ?WHOLE ?SUBSTRS) (DO-REGEX-MATCH STR PAT OPTS))) (OR (STRINGP WHOLE) (NOT WHOLE))) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM RETURN-TYPE-OF-DO-REGEX-MATCH.SUBSTRS (B* (((MV ?ERROR-MSG ?WHOLE ?SUBSTRS) (DO-REGEX-MATCH STR PAT OPTS))) (TRUE-LISTP SUBSTRS)) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE DO-REGEX-MATCH)) (XDOC::PARENTS (QUOTE (REGEX))) (XDOC::SHORT (QUOTE "Test whether a given string matches a given regular expression")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE DO-REGEX-MATCH))) 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>Intended for use in the dynamically compiled case.</p>



<p>As examples:</p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"cdeabfdefdeghij\"
                (parse-options 'fixed ; type
                                nil  ; not strict-paren
                                nil  ; not strict-brace
                                nil  ; not strict-repeat
                                t    ; case-insensitive
                                ))
})

<p>returns <tt>(mv nil \"cdeAbfdEfDeghIj\" nil)</tt>, </p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"ab([def]*)\\1([gh])\"
                 (parse-options 'fixed nil nil nil t))
}) 

<p>returns <tt>(mv nil nil nil)</tt>, and </p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"ab([def]*)\\1([gh])\"
                 (parse-options 'ere nil nil nil t))
})

<p>returns <tt>(mv nil \"AbfdEfDeg\" (\"fdE\" \"g\"))</tt>.</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 . DO-REGEX-MATCH) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS REGEX) (:SHORT . "Test whether a given string matches a given regular expression") (:LONG . "<p>Intended for use in the dynamically compiled case.</p>



<p>As examples:</p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"cdeabfdefdeghij\"
                (parse-options 'fixed ; type
                                nil  ; not strict-paren
                                nil  ; not strict-brace
                                nil  ; not strict-repeat
                                t    ; case-insensitive
                                ))
})

<p>returns <tt>(mv nil \"cdeAbfdEfDeghIj\" nil)</tt>, </p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"ab([def]*)\\1([gh])\"
                 (parse-options 'fixed nil nil nil t))
}) 

<p>returns <tt>(mv nil nil nil)</tt>, and </p>

@({
 (do-regex-match \"cdeAbfdEfDeghIj\"
                 \"ab([def]*)\\1([gh])\"
                 (parse-options 'ere nil nil nil t))
})

<p>returns <tt>(mv nil \"AbfdEfDeg\" (\"fdE\" \"g\"))</tt>.</p>

<h3>Definitions and Theorems</h3>@(def |ACL2|::|DO-REGEX-MATCH|)
@(def |ACL2|::|RETURN-TYPE-OF-DO-REGEX-MATCH.ERROR-MSG|)
@(def |ACL2|::|RETURN-TYPE-OF-DO-REGEX-MATCH.WHOLE|)
@(def |ACL2|::|RETURN-TYPE-OF-DO-REGEX-MATCH.SUBSTRS|)") (:FROM . "[books]/regex/regex-ui.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC DO-REGEX-MATCH)))))) (VALUE-TRIPLE (QUOTE DO-REGEX-MATCH))))) (RECORD-EXPANSION (MAKE-EVENT (B* ((CUTIL::CURRENT-PKG (F-GET-GLOBAL (QUOTE CURRENT-PACKAGE) STATE)) (CUTIL::BASE-PKG (PKG-WITNESS CUTIL::CURRENT-PKG)) (CUTIL::FNNAME (QUOTE DO-REGEX-MATCH)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE DO-REGEX-MATCH) (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to test") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . PAT) (GUARD STRINGP PAT) (DOC . "String representing the pattern to find") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OPTS) (GUARD PARSE-OPTS-P OPTS) (DOC . "Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR-MSG) (DOC . "Error message") (CUTIL::RETURN-TYPE OR (STRINGP ERROR-MSG) (NOT ERROR-MSG)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . WHOLE) (DOC . "The portion of <tt>str</tt> that matches the pattern
                        provided by <tt>pat</tt>.  <tt>Nil</tt> if there is not
                        a match.") (CUTIL::RETURN-TYPE OR (STRINGP WHOLE) (NOT WHOLE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . SUBSTRS) (DOC . "List of substrings that match parenthesized
                          subexpressions of the pattern (when applicable).
                          <tt>Nil</tt> if there is not a match.") (CUTIL::RETURN-TYPE TRUE-LISTP SUBSTRS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)))) CUTIL::BASE-PKG STATE)) (EVENT (LIST (QUOTE XDOC::XDOC-PREPEND) CUTIL::FNNAME CUTIL::STR))) (VALUE EVENT))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE DO-REGEX-MATCH) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING:  Ignoring attempt to prepend to topic ~x0, ~
                         because no such topic is currently defined.~%" (QUOTE DO-REGEX-MATCH)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) "<box><dl>
<dt>Signature</dt><dt><code>(do-regex-match str pat opts) &rarr; (mv error-msg whole substrs)</code></dt><dt>Arguments</dt><dd><tt>str</tt> &mdash; String to test.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp str)').</color></dd>
<dd><tt>pat</tt> &mdash; String representing the pattern to find.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp pat)').</color></dd>
<dd><tt>opts</tt> &mdash; Options for test.  <br />

                       BOZO: state and explain the possible options.  Possible
                       options might include
                       <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                       basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                       <tt>:full</tt> for something, etc.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(parse-opts-p opts)').</color></dd>
<dt>Returns</dt><dd><tt>error-msg</tt> &mdash; Error message.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(or (stringp error-msg) (not error-msg))').</color></dd>
<dd><tt>whole</tt> &mdash; The portion of <tt>str</tt> that matches the pattern
                        provided by <tt>pat</tt>.  <tt>Nil</tt> if there is not
                        a match.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(or (stringp whole) (not whole))').</color></dd>
<dd><tt>substrs</tt> &mdash; List of substrings that match parenthesized
                          subexpressions of the pattern (when applicable).
                          <tt>Nil</tt> if there is not a match.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(true-listp substrs)').</color></dd>
</dl></box>
" XDOC::OLD-LONG)) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))))) (24 RECORD-EXPANSION (LOCAL (ASSERT! (MV-LET (ERROR-MSG WHOLE SUBSTRS) (DO-REGEX-MATCH "cdeAbfdEfDeghIj" "ab([def]*)\\1([gh])" (PARSE-OPTIONS (QUOTE ERE) NIL NIL NIL T)) (AND (NOT ERROR-MSG) (EQUAL WHOLE "AbfdEfDeg") (EQUAL SUBSTRS (QUOTE ("fdE" "g"))))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (25 RECORD-EXPANSION (LOCAL (ASSERT! (MV-LET (ERROR-MSG WHOLE SUBSTRS) (DO-REGEX-MATCH "cdeAbfdEfDeghIj" "ab([def]*)\\1([gh])" (PARSE-OPTIONS (QUOTE FIXED) NIL NIL NIL T)) (AND (NOT ERROR-MSG) (NOT WHOLE) (NOT SUBSTRS))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (26 RECORD-EXPANSION (LOCAL (ASSERT! (MV-LET (ERROR-MSG WHOLE SUBSTRS) (DO-REGEX-MATCH "cdeAbfdEfDeghIj" "cdeabfdefdeghij" (PARSE-OPTIONS (QUOTE FIXED) NIL NIL NIL T)) (AND (NOT ERROR-MSG) (EQUAL WHOLE "cdeAbfdEfDeghIj") (NOT SUBSTRS))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (28 RECORD-EXPANSION (LOCAL (MAKE-EVENT (B* ((RES1-OK (EQUAL (B* (((MATCH "ab([def]*)\\1([gh])" :I :FULL F :SUBSTRS (A B)) "cdeAbfdEfDeghIj")) (LIST A B F)) (QUOTE ("fdE" "g" "AbfdEfDeg")))) (RES2-OK (EQUAL (B* ((PATTERN "ab([def]*)\\1([gh])") (STRING "cdeAbfdEfDeghIj") ((MATCH PATTERN :I :FULL F :SUBSTRS (A B) :ERROR-MSG E) STRING)) (LIST E A B F)) (QUOTE (NIL "fdE" "g" "AbfdEfDeg")))) (RES3-OK (EQUAL (B* ((PATTERN "ab([def]*)\\1([gh])") (STRING "cdeAbfdEfDeghIj") ((MATCH PATTERN :I :FULL ?F :SUBSTRS ((THE STRING A) &)) STRING)) (LIST A F)) (QUOTE ("fdE" "AbfdEfDeg"))))) (IF (AND RES1-OK RES2-OK RES3-OK) (QUOTE (VALUE-TRIPLE :OK)) (ER HARD? (QUOTE REGEX-UI) "One of the tests failed~%"))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (33 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (F "FOO_37") (LIST "FOO_37" "FOO" "37")))) (LOCAL (VALUE-TRIPLE :ELIDED))) (34 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (F "FOO_37_abc") (LIST "FOO_37" "FOO" "37")))) (LOCAL (VALUE-TRIPLE :ELIDED))) (35 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (F "abc_FOO_37_abc") (LIST "FOO_37" "FOO" "37")))) (LOCAL (VALUE-TRIPLE :ELIDED))) (36 RECORD-EXPANSION (DEFINE STRING-KEYED-ALIST-P (X) :PARENTS (UNDOCUMENTED) :SHORT "Recognizer for alists whose keys are strings.  Used to implement and
          extend @(see regex-get)." :GUARD T (COND ((ATOM X) (NULL X)) (T (AND (CONSP (CAR X)) (STRINGP (CAAR X)) (STRING-KEYED-ALIST-P (CDR X)))))) (PROGN (RECORD-EXPANSION (DEFSECTION STRING-KEYED-ALIST-P :PARENTS (UNDOCUMENTED) :SHORT "Recognizer for alists whose keys are strings.  Used to implement and
          extend @(see regex-get)." (DEFUND STRING-KEYED-ALIST-P (X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE STRING-KEYED-ALIST-P))) (DECLARE (IGNORABLE __FUNCTION__)) (COND ((ATOM X) (NULL X)) (T (AND (CONSP (CAR X)) (STRINGP (CAAR X)) (STRING-KEYED-ALIST-P (CDR X))))))) (CUTIL::EXTEND-DEFINE-TABLE STRING-KEYED-ALIST-P :FN (QUOTE STRING-KEYED-ALIST-P) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE STRING-KEYED-ALIST-P) (W STATE)) (QUOTE (IN-THEORY (ENABLE STRING-KEYED-ALIST-P))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE STRING-KEYED-ALIST-P) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STRING-KEYED-ALIST-P)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STRING-KEYED-ALIST-P (X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE STRING-KEYED-ALIST-P))) (DECLARE (IGNORABLE __FUNCTION__)) (COND ((ATOM X) (NULL X)) (T (AND (CONSP (CAR X)) (STRINGP (CAAR X)) (STRING-KEYED-ALIST-P (CDR X))))))) (CUTIL::EXTEND-DEFINE-TABLE STRING-KEYED-ALIST-P :FN (QUOTE STRING-KEYED-ALIST-P) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE STRING-KEYED-ALIST-P) (W STATE)) (QUOTE (IN-THEORY (ENABLE STRING-KEYED-ALIST-P))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE STRING-KEYED-ALIST-P) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STRING-KEYED-ALIST-P (X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE STRING-KEYED-ALIST-P))) (DECLARE (IGNORABLE __FUNCTION__)) (COND ((ATOM X) (NULL X)) (T (AND (CONSP (CAR X)) (STRINGP (CAAR X)) (STRING-KEYED-ALIST-P (CDR X))))))) (CUTIL::EXTEND-DEFINE-TABLE STRING-KEYED-ALIST-P :FN (QUOTE STRING-KEYED-ALIST-P) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE STRING-KEYED-ALIST-P) (W STATE)) (QUOTE (IN-THEORY (ENABLE STRING-KEYED-ALIST-P))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE STRING-KEYED-ALIST-P) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STRING-KEYED-ALIST-P)) (XDOC::PARENTS (QUOTE (UNDOCUMENTED))) (XDOC::SHORT (QUOTE "Recognizer for alists whose keys are strings.  Used to implement and
          extend @(see regex-get).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STRING-KEYED-ALIST-P))) 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 "") (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 . STRING-KEYED-ALIST-P) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS UNDOCUMENTED) (:SHORT . "Recognizer for alists whose keys are strings.  Used to implement and
          extend @(see regex-get).") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |ACL2|::|STRING-KEYED-ALIST-P|)") (:FROM . "[books]/regex/regex-ui.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STRING-KEYED-ALIST-P)))))) (VALUE-TRIPLE (QUOTE STRING-KEYED-ALIST-P))))) (RECORD-EXPANSION (MAKE-EVENT (B* ((CUTIL::CURRENT-PKG (F-GET-GLOBAL (QUOTE CURRENT-PACKAGE) STATE)) (CUTIL::BASE-PKG (PKG-WITNESS CUTIL::CURRENT-PKG)) (CUTIL::FNNAME (QUOTE STRING-KEYED-ALIST-P)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE STRING-KEYED-ALIST-P) (QUOTE ((:FORMAL (CUTIL::NAME . X) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE NIL) CUTIL::BASE-PKG STATE)) (EVENT (LIST (QUOTE XDOC::XDOC-PREPEND) CUTIL::FNNAME CUTIL::STR))) (VALUE EVENT))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE STRING-KEYED-ALIST-P) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING:  Ignoring attempt to prepend to topic ~x0, ~
                         because no such topic is currently defined.~%" (QUOTE STRING-KEYED-ALIST-P)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) "<box><dl>
<dt>Signature</dt><dt><code>(string-keyed-alist-p x) &rarr; *</code></dt></dl></box>
" XDOC::OLD-LONG)) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))))) (38 RECORD-EXPANSION (DEFINE REGEX-GET ((STR STRINGP "String to lookup") (ALIST STRING-KEYED-ALIST-P "Alistp where keys are regular expressions in
                                string form and the values are of an
                                unspecified type")) :RETURNS (KEY-VALUE-PAIR (EQUAL (CONSP KEY-VALUE-PAIR) (IF KEY-VALUE-PAIR T NIL)) "Matching regular expression paired with its value.
                            Nil if no entry is found.  Note that this is an
                            exact match, which is different from the
                            functionality of grep, which returns substrings
                            that match." :HYP :FGUARD) :PARENTS (REGEX) :SHORT "Lookup a string in the regular expression alist." :LONG "<p>Warning: this is likely to be a pretty slow way of doing things --
         but we currently have no experimental evidence that indicates whether
         this performance is unacceptable.  If you're looking for a place to
         suspect of bad performance, this could be a good place to start.</p>

         <p>It is likely that the user will want to use <tt>regex-get</tt> to
         implement a function that returns a value of a specific type.  Here,
         we show a couple events that we needed to provide to prove that our
         wrapper for <tt>regex-get</tt> returns an <tt>acl2-number-listp</tt>.
         We expect that users in similar situations will need comparable
         lemmas.

         Such composability is similar to the approach available and documented
         in the book <tt>defexec/other-apps/records/records</tt>.</p>

         <p>We now begin our approach.  First we setup an alist to serve as our
         regex dictionary:</p>

@({
 (include-book \"cutil/defalist\" :dir :system)

 (cutil::defalist dictionary-p (x)
   :key (stringp x)
   :val (acl2-number-listp x)
   :true-listp t)
})

        <p>Next we establish two lemmas that help us specify the return type
        for what will be our use of regex-get:</p>

@({
 (include-book \"regex/regex-ui\" :dir :system)

 (defthm dictionary-p-is-string-keyed-alist-p
   (implies (dictionary-p x)
            (string-keyed-alist-p x))
   :hints ((\"Goal\" :in-theory (enable string-keyed-alist-p))))

 (defthm regex-get-of-dictionary-p-returns-terminal-list-p
   (implies (and (stringp x)
                 (dictionary-p dict))
            (acl2-number-listp (cdr (regex-get x dict))))
   :hints ((\"Goal\" :in-theory (enable regex-get))))
})

        <p>Which enables ACL2 to admit our lookup function:</p>

@({
 (include-book \"cutil/define\" :dir :system)

 (define dictionary-lookup ((key stringp)
                            (dictionary dictionary-p))
   :returns (ans (acl2-number-listp ans)
                 \"The list of integers associated with the given key\"
                 :hyp :fguard)
   (let ((val (regex-get key dictionary)))
     (if (consp val) 
         (cdr val) 
       nil))) ; return value in the atom case is chosen by user
})
" (IF (ATOM ALIST) NIL (MV-LET (ERR WHOLE SUBSTRS) (DO-REGEX-MATCH STR (CAAR ALIST) (PARSE-OPTIONS (QUOTE ERE) NIL NIL NIL NIL)) (DECLARE (IGNORE SUBSTRS)) (COND (ERR (ER HARD? (QUOTE REGEX-GET) ERR)) ((EQUAL STR WHOLE) (CAR ALIST)) (T (REGEX-GET STR (CDR ALIST))))))) (PROGN (RECORD-EXPANSION (DEFSECTION REGEX-GET :PARENTS (REGEX) :SHORT "Lookup a string in the regular expression alist." :LONG "<p>Warning: this is likely to be a pretty slow way of doing things --
         but we currently have no experimental evidence that indicates whether
         this performance is unacceptable.  If you're looking for a place to
         suspect of bad performance, this could be a good place to start.</p>

         <p>It is likely that the user will want to use <tt>regex-get</tt> to
         implement a function that returns a value of a specific type.  Here,
         we show a couple events that we needed to provide to prove that our
         wrapper for <tt>regex-get</tt> returns an <tt>acl2-number-listp</tt>.
         We expect that users in similar situations will need comparable
         lemmas.

         Such composability is similar to the approach available and documented
         in the book <tt>defexec/other-apps/records/records</tt>.</p>

         <p>We now begin our approach.  First we setup an alist to serve as our
         regex dictionary:</p>

@({
 (include-book \"cutil/defalist\" :dir :system)

 (cutil::defalist dictionary-p (x)
   :key (stringp x)
   :val (acl2-number-listp x)
   :true-listp t)
})

        <p>Next we establish two lemmas that help us specify the return type
        for what will be our use of regex-get:</p>

@({
 (include-book \"regex/regex-ui\" :dir :system)

 (defthm dictionary-p-is-string-keyed-alist-p
   (implies (dictionary-p x)
            (string-keyed-alist-p x))
   :hints ((\"Goal\" :in-theory (enable string-keyed-alist-p))))

 (defthm regex-get-of-dictionary-p-returns-terminal-list-p
   (implies (and (stringp x)
                 (dictionary-p dict))
            (acl2-number-listp (cdr (regex-get x dict))))
   :hints ((\"Goal\" :in-theory (enable regex-get))))
})

        <p>Which enables ACL2 to admit our lookup function:</p>

@({
 (include-book \"cutil/define\" :dir :system)

 (define dictionary-lookup ((key stringp)
                            (dictionary dictionary-p))
   :returns (ans (acl2-number-listp ans)
                 \"The list of integers associated with the given key\"
                 :hyp :fguard)
   (let ((val (regex-get key dictionary)))
     (if (consp val) 
         (cdr val) 
       nil))) ; return value in the atom case is chosen by user
})
" (DEFUND REGEX-GET (STR ALIST) (DECLARE (XARGS :GUARD (AND (STRINGP STR) (STRING-KEYED-ALIST-P ALIST)))) (LET ((__FUNCTION__ (QUOTE REGEX-GET))) (DECLARE (IGNORABLE __FUNCTION__)) (IF (ATOM ALIST) NIL (MV-LET (ERR WHOLE SUBSTRS) (DO-REGEX-MATCH STR (CAAR ALIST) (PARSE-OPTIONS (QUOTE ERE) NIL NIL NIL NIL)) (DECLARE (IGNORE SUBSTRS)) (COND (ERR (ER HARD? (QUOTE REGEX-GET) ERR)) ((EQUAL STR WHOLE) (CAR ALIST)) (T (REGEX-GET STR (CDR ALIST)))))))) (CUTIL::EXTEND-DEFINE-TABLE REGEX-GET :FN (QUOTE REGEX-GET) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . KEY-VALUE-PAIR) (DOC . "Matching regular expression paired with its value.
                            Nil if no entry is found.  Note that this is an
                            exact match, which is different from the
                            functionality of grep, which returns substrings
                            that match.") (CUTIL::RETURN-TYPE EQUAL (CONSP KEY-VALUE-PAIR) (IF KEY-VALUE-PAIR T NIL)) (CUTIL::HYP . :FGUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to lookup") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . ALIST) (GUARD STRING-KEYED-ALIST-P ALIST) (DOC . "Alistp where keys are regular expressions in
                                string form and the values are of an
                                unspecified type") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE REGEX-GET) (W STATE)) (QUOTE (IN-THEORY (ENABLE REGEX-GET))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE REGEX-GET) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . KEY-VALUE-PAIR) (DOC . "Matching regular expression paired with its value.
                            Nil if no entry is found.  Note that this is an
                            exact match, which is different from the
                            functionality of grep, which returns substrings
                            that match.") (CUTIL::RETURN-TYPE EQUAL (CONSP KEY-VALUE-PAIR) (IF KEY-VALUE-PAIR T NIL)) (CUTIL::HYP . :FGUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE REGEX-GET)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND REGEX-GET (STR ALIST) (DECLARE (XARGS :GUARD (AND (STRINGP STR) (STRING-KEYED-ALIST-P ALIST)))) (LET ((__FUNCTION__ (QUOTE REGEX-GET))) (DECLARE (IGNORABLE __FUNCTION__)) (IF (ATOM ALIST) NIL (MV-LET (ERR WHOLE SUBSTRS) (DO-REGEX-MATCH STR (CAAR ALIST) (PARSE-OPTIONS (QUOTE ERE) NIL NIL NIL NIL)) (DECLARE (IGNORE SUBSTRS)) (COND (ERR (ER HARD? (QUOTE REGEX-GET) ERR)) ((EQUAL STR WHOLE) (CAR ALIST)) (T (REGEX-GET STR (CDR ALIST)))))))) (CUTIL::EXTEND-DEFINE-TABLE REGEX-GET :FN (QUOTE REGEX-GET) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . KEY-VALUE-PAIR) (DOC . "Matching regular expression paired with its value.
                            Nil if no entry is found.  Note that this is an
                            exact match, which is different from the
                            functionality of grep, which returns substrings
                            that match.") (CUTIL::RETURN-TYPE EQUAL (CONSP KEY-VALUE-PAIR) (IF KEY-VALUE-PAIR T NIL)) (CUTIL::HYP . :FGUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to lookup") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . ALIST) (GUARD STRING-KEYED-ALIST-P ALIST) (DOC . "Alistp where keys are regular expressions in
                                string form and the values are of an
                                unspecified type") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE REGEX-GET) (W STATE)) (QUOTE (IN-THEORY (ENABLE REGEX-GET))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE REGEX-GET) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . KEY-VALUE-PAIR) (DOC . "Matching regular expression paired with its value.
                            Nil if no entry is found.  Note that this is an
                            exact match, which is different from the
                            functionality of grep, which returns substrings
                            that match.") (CUTIL::RETURN-TYPE EQUAL (CONSP KEY-VALUE-PAIR) (IF KEY-VALUE-PAIR T NIL)) (CUTIL::HYP . :FGUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND REGEX-GET (STR ALIST) (DECLARE (XARGS :GUARD (AND (STRINGP STR) (STRING-KEYED-ALIST-P ALIST)))) (LET ((__FUNCTION__ (QUOTE REGEX-GET))) (DECLARE (IGNORABLE __FUNCTION__)) (IF (ATOM ALIST) NIL (MV-LET (ERR WHOLE SUBSTRS) (DO-REGEX-MATCH STR (CAAR ALIST) (PARSE-OPTIONS (QUOTE ERE) NIL NIL NIL NIL)) (DECLARE (IGNORE SUBSTRS)) (COND (ERR (ER HARD? (QUOTE REGEX-GET) ERR)) ((EQUAL STR WHOLE) (CAR ALIST)) (T (REGEX-GET STR (CDR ALIST)))))))) (CUTIL::EXTEND-DEFINE-TABLE REGEX-GET :FN (QUOTE REGEX-GET) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . KEY-VALUE-PAIR) (DOC . "Matching regular expression paired with its value.
                            Nil if no entry is found.  Note that this is an
                            exact match, which is different from the
                            functionality of grep, which returns substrings
                            that match.") (CUTIL::RETURN-TYPE EQUAL (CONSP KEY-VALUE-PAIR) (IF KEY-VALUE-PAIR T NIL)) (CUTIL::HYP . :FGUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to lookup") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . ALIST) (GUARD STRING-KEYED-ALIST-P ALIST) (DOC . "Alistp where keys are regular expressions in
                                string form and the values are of an
                                unspecified type") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE REGEX-GET) (W STATE)) (QUOTE (IN-THEORY (ENABLE REGEX-GET))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE REGEX-GET) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . KEY-VALUE-PAIR) (DOC . "Matching regular expression paired with its value.
                            Nil if no entry is found.  Note that this is an
                            exact match, which is different from the
                            functionality of grep, which returns substrings
                            that match.") (CUTIL::RETURN-TYPE EQUAL (CONSP KEY-VALUE-PAIR) (IF KEY-VALUE-PAIR T NIL)) (CUTIL::HYP . :FGUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM RETURN-TYPE-OF-REGEX-GET (IMPLIES (AND (FORCE (STRINGP STR)) (FORCE (STRING-KEYED-ALIST-P ALIST))) (LET ((KEY-VALUE-PAIR (REGEX-GET STR ALIST))) (EQUAL (CONSP KEY-VALUE-PAIR) (IF KEY-VALUE-PAIR T NIL)))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE REGEX-GET)) (XDOC::PARENTS (QUOTE (REGEX))) (XDOC::SHORT (QUOTE "Lookup a string in the regular expression alist.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE REGEX-GET))) 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>Warning: this is likely to be a pretty slow way of doing things --
         but we currently have no experimental evidence that indicates whether
         this performance is unacceptable.  If you're looking for a place to
         suspect of bad performance, this could be a good place to start.</p>

         <p>It is likely that the user will want to use <tt>regex-get</tt> to
         implement a function that returns a value of a specific type.  Here,
         we show a couple events that we needed to provide to prove that our
         wrapper for <tt>regex-get</tt> returns an <tt>acl2-number-listp</tt>.
         We expect that users in similar situations will need comparable
         lemmas.

         Such composability is similar to the approach available and documented
         in the book <tt>defexec/other-apps/records/records</tt>.</p>

         <p>We now begin our approach.  First we setup an alist to serve as our
         regex dictionary:</p>

@({
 (include-book \"cutil/defalist\" :dir :system)

 (cutil::defalist dictionary-p (x)
   :key (stringp x)
   :val (acl2-number-listp x)
   :true-listp t)
})

        <p>Next we establish two lemmas that help us specify the return type
        for what will be our use of regex-get:</p>

@({
 (include-book \"regex/regex-ui\" :dir :system)

 (defthm dictionary-p-is-string-keyed-alist-p
   (implies (dictionary-p x)
            (string-keyed-alist-p x))
   :hints ((\"Goal\" :in-theory (enable string-keyed-alist-p))))

 (defthm regex-get-of-dictionary-p-returns-terminal-list-p
   (implies (and (stringp x)
                 (dictionary-p dict))
            (acl2-number-listp (cdr (regex-get x dict))))
   :hints ((\"Goal\" :in-theory (enable regex-get))))
})

        <p>Which enables ACL2 to admit our lookup function:</p>

@({
 (include-book \"cutil/define\" :dir :system)

 (define dictionary-lookup ((key stringp)
                            (dictionary dictionary-p))
   :returns (ans (acl2-number-listp ans)
                 \"The list of integers associated with the given key\"
                 :hyp :fguard)
   (let ((val (regex-get key dictionary)))
     (if (consp val) 
         (cdr val) 
       nil))) ; return value in the atom case is chosen by user
})
") (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 . REGEX-GET) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS REGEX) (:SHORT . "Lookup a string in the regular expression alist.") (:LONG . "<p>Warning: this is likely to be a pretty slow way of doing things --
         but we currently have no experimental evidence that indicates whether
         this performance is unacceptable.  If you're looking for a place to
         suspect of bad performance, this could be a good place to start.</p>

         <p>It is likely that the user will want to use <tt>regex-get</tt> to
         implement a function that returns a value of a specific type.  Here,
         we show a couple events that we needed to provide to prove that our
         wrapper for <tt>regex-get</tt> returns an <tt>acl2-number-listp</tt>.
         We expect that users in similar situations will need comparable
         lemmas.

         Such composability is similar to the approach available and documented
         in the book <tt>defexec/other-apps/records/records</tt>.</p>

         <p>We now begin our approach.  First we setup an alist to serve as our
         regex dictionary:</p>

@({
 (include-book \"cutil/defalist\" :dir :system)

 (cutil::defalist dictionary-p (x)
   :key (stringp x)
   :val (acl2-number-listp x)
   :true-listp t)
})

        <p>Next we establish two lemmas that help us specify the return type
        for what will be our use of regex-get:</p>

@({
 (include-book \"regex/regex-ui\" :dir :system)

 (defthm dictionary-p-is-string-keyed-alist-p
   (implies (dictionary-p x)
            (string-keyed-alist-p x))
   :hints ((\"Goal\" :in-theory (enable string-keyed-alist-p))))

 (defthm regex-get-of-dictionary-p-returns-terminal-list-p
   (implies (and (stringp x)
                 (dictionary-p dict))
            (acl2-number-listp (cdr (regex-get x dict))))
   :hints ((\"Goal\" :in-theory (enable regex-get))))
})

        <p>Which enables ACL2 to admit our lookup function:</p>

@({
 (include-book \"cutil/define\" :dir :system)

 (define dictionary-lookup ((key stringp)
                            (dictionary dictionary-p))
   :returns (ans (acl2-number-listp ans)
                 \"The list of integers associated with the given key\"
                 :hyp :fguard)
   (let ((val (regex-get key dictionary)))
     (if (consp val) 
         (cdr val) 
       nil))) ; return value in the atom case is chosen by user
})


<h3>Definitions and Theorems</h3>@(def |ACL2|::|REGEX-GET|)
@(def |ACL2|::|RETURN-TYPE-OF-REGEX-GET|)") (:FROM . "[books]/regex/regex-ui.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC REGEX-GET)))))) (VALUE-TRIPLE (QUOTE REGEX-GET))))) (RECORD-EXPANSION (MAKE-EVENT (B* ((CUTIL::CURRENT-PKG (F-GET-GLOBAL (QUOTE CURRENT-PACKAGE) STATE)) (CUTIL::BASE-PKG (PKG-WITNESS CUTIL::CURRENT-PKG)) (CUTIL::FNNAME (QUOTE REGEX-GET)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE REGEX-GET) (QUOTE ((:FORMAL (CUTIL::NAME . STR) (GUARD STRINGP STR) (DOC . "String to lookup") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . ALIST) (GUARD STRING-KEYED-ALIST-P ALIST) (DOC . "Alistp where keys are regular expressions in
                                string form and the values are of an
                                unspecified type") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . KEY-VALUE-PAIR) (DOC . "Matching regular expression paired with its value.
                            Nil if no entry is found.  Note that this is an
                            exact match, which is different from the
                            functionality of grep, which returns substrings
                            that match.") (CUTIL::RETURN-TYPE EQUAL (CONSP KEY-VALUE-PAIR) (IF KEY-VALUE-PAIR T NIL)) (CUTIL::HYP . :FGUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) CUTIL::BASE-PKG STATE)) (EVENT (LIST (QUOTE XDOC::XDOC-PREPEND) CUTIL::FNNAME CUTIL::STR))) (VALUE EVENT))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE REGEX-GET) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING:  Ignoring attempt to prepend to topic ~x0, ~
                         because no such topic is currently defined.~%" (QUOTE REGEX-GET)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) "<box><dl>
<dt>Signature</dt><dt><code>(regex-get str alist) &rarr; key-value-pair</code></dt><dt>Arguments</dt><dd><tt>str</tt> &mdash; String to lookup.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp str)').</color></dd>
<dd><tt>alist</tt> &mdash; Alistp where keys are regular expressions in
                                string form and the values are of an
                                unspecified type.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(string-keyed-alist-p alist)').</color></dd>
<dt>Returns</dt><dd><tt>key-value-pair</tt> &mdash; Matching regular expression paired with its value.
                            Nil if no entry is found.  Note that this is an
                            exact match, which is different from the
                            functionality of grep, which returns substrings
                            that match.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(equal (consp key-value-pair) (if key-value-pair t nil))'), given the @(see guard).</color></dd>
</dl></box>
" XDOC::OLD-LONG)) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))))) (40 RECORD-EXPANSION (LOCAL (ASSERT! (AND (EQUAL (CDR (REGEX-GET "abcd" *REGEX-ALIST*)) 1) (EQUAL (CDR (REGEX-GET "ab" *REGEX-ALIST*)) 2) (EQUAL (CDR (REGEX-GET "abab" *REGEX-ALIST*)) 2)))) (LOCAL (VALUE-TRIPLE :ELIDED))))
(("/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-ui.lisp" "regex-ui" "regex-ui" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 123873859) ("/usr/share/acl2-6.3/books/cutil/define.lisp" "cutil/define" "define" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1768331178) ("/usr/share/acl2-6.3/books/xdoc/fmt-to-str.lisp" "xdoc/fmt-to-str" "fmt-to-str" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 717243077) ("/usr/share/acl2-6.3/books/centaur/bridge/portcullis.lisp" "centaur/bridge/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 661758845) ("/usr/share/acl2-6.3/books/oslib/portcullis.lisp" "oslib/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197838065) ("/usr/share/acl2-6.3/books/cutil/returnspecs.lisp" "returnspecs" "returnspecs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 722876511) ("/usr/share/acl2-6.3/books/cutil/formals.lisp" "formals" "formals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 606017704) ("/usr/share/acl2-6.3/books/cutil/da-base.lisp" "da-base" "da-base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 517345789) ("/usr/share/acl2-6.3/books/cutil/look-up.lisp" "look-up" "look-up" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1505505915) ("/usr/share/acl2-6.3/books/cutil/support.lisp" "support" "support" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1180314020) ("/usr/share/acl2-6.3/books/str/case-conversion.lisp" "str/case-conversion" "case-conversion" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 646818128) (LOCAL ("/usr/share/acl2-6.3/books/str/subseq.lisp" "subseq" "subseq" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1507065012)) ("/usr/share/acl2-6.3/books/str/cat.lisp" "cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1576295912) ("/usr/share/acl2-6.3/books/regex/regex-exec.lisp" "regex-exec" "regex-exec" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 791395464) ("/usr/share/acl2-6.3/books/clause-processors/find-subterms.lisp" "clause-processors/find-subterms" "find-subterms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 928774552) ("/usr/share/acl2-6.3/books/tools/flag.lisp" "tools/flag" "flag" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1308242620) ("/usr/share/acl2-6.3/books/regex/regex-parse.lisp" "regex-parse" "regex-parse" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 392250108) ("/usr/share/acl2-6.3/books/regex/regex-parse-brace.lisp" "regex-parse-brace" "regex-parse-brace" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 738338822) ("/usr/share/acl2-6.3/books/regex/regex-parse-bracket.lisp" "regex-parse-bracket" "regex-parse-bracket" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1455349621) ("/usr/share/acl2-6.3/books/regex/input-list.lisp" "input-list" "input-list" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 354450911) ("/usr/share/acl2-6.3/books/cutil/deflist.lisp" "cutil/deflist" "deflist" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 857676809) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/under-set-equiv.lisp" "std/osets/under-set-equiv" "under-set-equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1595680367)) ("/usr/share/acl2-6.3/books/cutil/maybe-defthm.lisp" "maybe-defthm" "maybe-defthm" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 169275099) ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/defsort/duplicated-members.lisp" "defsort/duplicated-members" "duplicated-members" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 720301003) ("/usr/share/acl2-6.3/books/defsort/uniquep.lisp" "uniquep" "uniquep" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1350027706) ("/usr/share/acl2-6.3/books/defsort/defsort.lisp" "defsort" "defsort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 284418813) ("/usr/share/acl2-6.3/books/defsort/generic.lisp" "generic" "generic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 992283938) (LOCAL ("/usr/share/acl2-6.3/books/defsort/generic-impl.lisp" "generic-impl" "generic-impl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 154835353)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-lemmas.lisp" "ihs/ihs-lemmas" "ihs-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1685360399)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-lemmas.lisp" "logops-lemmas" "logops-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 998280003)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-definitions.lisp" "logops-definitions" "logops-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2048680937)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/basic-definitions.lisp" "basic-definitions" "basic-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1383521171)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/quotient-remainder-lemmas.lisp" "quotient-remainder-lemmas" "quotient-remainder-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 603178913)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-theories.lisp" "ihs-theories" "ihs-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2130795727)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/math-lemmas.lisp" "math-lemmas" "math-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1617928370)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-init.lisp" "ihs-init" "ihs-init" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1992988803)) (LOCAL ("/usr/share/acl2-6.3/books/data-structures/utilities.lisp" "data-structures/utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1536684829)) (LOCAL ("/usr/share/acl2-6.3/books/data-structures/doc-section.lisp" "doc-section" "doc-section" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1486104990)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-doc-topic.lisp" "ihs-doc-topic" "ihs-doc-topic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 664631734)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/no-duplicatesp.lisp" "std/lists/no-duplicatesp" "no-duplicatesp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 334869696)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "std/lists/revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "std/lists/duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854) ("/usr/share/acl2-6.3/books/std/osets/top.lisp" "std/osets/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2045504100) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/under-set-equiv.lisp" "under-set-equiv" "under-set-equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1595680367)) ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "std/lists/sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/sort.lisp" "sort" "sort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 335087178)) ("/usr/share/acl2-6.3/books/tools/mv-nth.lisp" "tools/mv-nth" "mv-nth" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82993140) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/outer.lisp" "outer" "outer" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 883866964)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/cardinality.lisp" "cardinality" "cardinality" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 101478632)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/difference.lisp" "difference" "difference" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1211437825)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/intersect.lisp" "intersect" "intersect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 464592124)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/union.lisp" "union" "union" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 895011797)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/delete.lisp" "delete" "delete" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 929878553)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/membership.lisp" "membership" "membership" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 48714967)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/primitives.lisp" "primitives" "primitives" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 392002111)) ("/usr/share/acl2-6.3/books/std/osets/computed-hints.lisp" "computed-hints" "computed-hints" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 537896665) ("/usr/share/acl2-6.3/books/std/osets/instance.lisp" "instance" "instance" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1528243117) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/misc/total-order.lisp" "misc/total-order" "total-order" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619824963) (LOCAL ("/usr/share/acl2-6.3/books/misc/total-order-bsd.lisp" "total-order-bsd" "total-order-bsd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 449327279)) ("/usr/share/acl2-6.3/books/str/cat.lisp" "str/cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1576295912) ("/usr/share/acl2-6.3/books/str/ieqv.lisp" "ieqv" "ieqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 620245362) ("/usr/share/acl2-6.3/books/std/lists/list-defuns.lisp" "std/lists/list-defuns" "list-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 321177760) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sublistp.lisp" "sublistp" "sublistp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1635583873)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/same-lengthp.lisp" "same-lengthp" "same-lengthp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2063823673)) ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262) ("/usr/share/acl2-6.3/books/std/lists/mfc-utils.lisp" "mfc-utils" "mfc-utils" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1043482843) ("/usr/share/acl2-6.3/books/std/lists/rcons.lisp" "rcons" "rcons" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105042482) ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/final-cdr.lisp" "final-cdr" "final-cdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 96013958)) ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854) ("/usr/share/acl2-6.3/books/std/lists/flatten.lisp" "flatten" "flatten" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1125138266) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/usr/share/acl2-6.3/books/str/char-case.lisp" "char-case" "char-case" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2059343298) ("/usr/share/acl2-6.3/books/str/eqv.lisp" "eqv" "eqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1920438599) (LOCAL ("/usr/share/acl2-6.3/books/str/arithmetic.lisp" "arithmetic" "arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 216355320)) ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "std/lists/repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "std/lists/nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/len.lisp" "std/lists/len" "len" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 963137114)) ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "std/lists/take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "std/lists/rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "std/lists/equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916) ("/usr/share/acl2-6.3/books/str/coerce.lisp" "coerce" "coerce" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053051260) ("/usr/share/acl2-6.3/books/str/make-character-list.lisp" "make-character-list" "make-character-list" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1622566814) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "std/lists/append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) ("/usr/share/acl2-6.3/books/std/lists/list-fix.lisp" "list-fix" "list-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1844974260) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) ("/usr/share/acl2-6.3/books/str/char-fix.lisp" "char-fix" "char-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 70055851) ("/usr/share/acl2-6.3/books/misc/definline.lisp" "misc/definline" "definline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1571016648) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "tools/bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439) ("/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))
1534509542