acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / cat.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((6 RECORD-EXPANSION (DEFSECTION STR::CAT :PARENTS (STR::CONCATENATION) :SHORT "Concatenate strings." :LONG "<p>@('(str::cat x y z ...)') is like @('(concatenate 'string x y z
...)'), but is less to type.</p>

<p>  If that's your goal, you might instead consider using the approach
outlined in @(see revappend-chars).</p>

<p>In some Lisps, using @('(concatenate 'string ...)') to join strings can be
even worse than just the cost of creating and initializing a new array.  The
@(see concatenate) function is quite flexible and can handle many types of
input, and this flexibility can cause some overhead if the Lisp does not
optimize for the @(''string') case.</p>

<p>So, if you are willing to accept a trust tag, then you may <b>optionally</b>
load the book:</p>

@({
  (include-book \"str/fast-cat\" :dir :system)
})

<p>which may improve the performance of @('str::cat').  How does this work?
Basically @('str::cat') calls one of @('fast-string-append') or
@('fast-string-append-lst'), depending on how many arguments it is given.  By
default, these functions are aliases for ACL2's @(see string-append) and
@('string-append-lst') functions.  But if you load the @('fast-cat') book,
these functions will be redefined to use raw Lisp array operations, and the
result may be faster.</p>" (DEFUN STR::FAST-STRING-APPEND (STR::STR1 STR::STR2) "May be redefined under-the-hood in str/fast-cat.lisp" (DECLARE (TYPE STRING STR::STR1 STR::STR2)) (STRING-APPEND STR::STR1 STR::STR2)) (DEFUN STR::FAST-STRING-APPEND-LST (X) "May be redefined under-the-hood in str/fast-cat.lisp" (DECLARE (XARGS :GUARD (STRING-LISTP X))) (STRING-APPEND-LST X)) (DEFMACRO STR::FAST-CONCATENATE (STR::RESULT-TYPE &REST STR::SEQUENCES) (DECLARE (XARGS :GUARD (MEMBER-EQUAL STR::RESULT-TYPE (QUOTE ((QUOTE STRING) (QUOTE LIST)))))) (COND ((EQUAL STR::RESULT-TYPE (QUOTE (QUOTE STRING))) (COND ((AND STR::SEQUENCES (CDR STR::SEQUENCES) (NULL (CDDR STR::SEQUENCES))) (LIST (QUOTE STR::FAST-STRING-APPEND) (CAR STR::SEQUENCES) (CADR STR::SEQUENCES))) (T (LIST (QUOTE STR::FAST-STRING-APPEND-LST) (CONS (QUOTE LIST) STR::SEQUENCES))))) (T (CONS (QUOTE APPEND) (CONS (CONS (QUOTE LIST) STR::SEQUENCES) (QUOTE NIL)))))) (DEFMACRO STR::CAT (&REST ARGS) (CONS (QUOTE STR::FAST-CONCATENATE) (CONS (CONS (QUOTE QUOTE) (CONS (QUOTE STRING) (QUOTE NIL))) ARGS)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::CAT)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUN STR::FAST-STRING-APPEND (STR::STR1 STR::STR2) "May be redefined under-the-hood in str/fast-cat.lisp" (DECLARE (TYPE STRING STR::STR1 STR::STR2)) (STRING-APPEND STR::STR1 STR::STR2)) (DEFUN STR::FAST-STRING-APPEND-LST (X) "May be redefined under-the-hood in str/fast-cat.lisp" (DECLARE (XARGS :GUARD (STRING-LISTP X))) (STRING-APPEND-LST X)) (DEFMACRO STR::FAST-CONCATENATE (STR::RESULT-TYPE &REST STR::SEQUENCES) (DECLARE (XARGS :GUARD (MEMBER-EQUAL STR::RESULT-TYPE (QUOTE ((QUOTE STRING) (QUOTE LIST)))))) (COND ((EQUAL STR::RESULT-TYPE (QUOTE (QUOTE STRING))) (COND ((AND STR::SEQUENCES (CDR STR::SEQUENCES) (NULL (CDDR STR::SEQUENCES))) (LIST (QUOTE STR::FAST-STRING-APPEND) (CAR STR::SEQUENCES) (CADR STR::SEQUENCES))) (T (LIST (QUOTE STR::FAST-STRING-APPEND-LST) (CONS (QUOTE LIST) STR::SEQUENCES))))) (T (CONS (QUOTE APPEND) (CONS (CONS (QUOTE LIST) STR::SEQUENCES) (QUOTE NIL)))))) (DEFMACRO STR::CAT (&REST ARGS) (CONS (QUOTE STR::FAST-CONCATENATE) (CONS (CONS (QUOTE QUOTE) (CONS (QUOTE STRING) (QUOTE NIL))) ARGS))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::CAT)) (XDOC::PARENTS (QUOTE (STR::CONCATENATION))) (XDOC::SHORT (QUOTE "Concatenate strings.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::CAT))) 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>@('(str::cat x y z ...)') is like @('(concatenate 'string x y z
...)'), but is less to type.</p>

<p>  If that's your goal, you might instead consider using the approach
outlined in @(see revappend-chars).</p>

<p>In some Lisps, using @('(concatenate 'string ...)') to join strings can be
even worse than just the cost of creating and initializing a new array.  The
@(see concatenate) function is quite flexible and can handle many types of
input, and this flexibility can cause some overhead if the Lisp does not
optimize for the @(''string') case.</p>

<p>So, if you are willing to accept a trust tag, then you may <b>optionally</b>
load the book:</p>

@({
  (include-book \"str/fast-cat\" :dir :system)
})

<p>which may improve the performance of @('str::cat').  How does this work?
Basically @('str::cat') calls one of @('fast-string-append') or
@('fast-string-append-lst'), depending on how many arguments it is given.  By
default, these functions are aliases for ACL2's @(see string-append) and
@('string-append-lst') functions.  But if you load the @('fast-cat') book,
these functions will be redefined to use raw Lisp array operations, and the
result may be faster.</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 . STR::CAT) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CONCATENATION) (:SHORT . "Concatenate strings.") (:LONG . "<p>@('(str::cat x y z ...)') is like @('(concatenate 'string x y z
...)'), but is less to type.</p>

<p>  If that's your goal, you might instead consider using the approach
outlined in @(see revappend-chars).</p>

<p>In some Lisps, using @('(concatenate 'string ...)') to join strings can be
even worse than just the cost of creating and initializing a new array.  The
@(see concatenate) function is quite flexible and can handle many types of
input, and this flexibility can cause some overhead if the Lisp does not
optimize for the @(''string') case.</p>

<p>So, if you are willing to accept a trust tag, then you may <b>optionally</b>
load the book:</p>

@({
  (include-book \"str/fast-cat\" :dir :system)
})

<p>which may improve the performance of @('str::cat').  How does this work?
Basically @('str::cat') calls one of @('fast-string-append') or
@('fast-string-append-lst'), depending on how many arguments it is given.  By
default, these functions are aliases for ACL2's @(see string-append) and
@('string-append-lst') functions.  But if you load the @('fast-cat') book,
these functions will be redefined to use raw Lisp array operations, and the
result may be faster.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|FAST-STRING-APPEND|)
@(def |STR|::|FAST-STRING-APPEND-LST|)") (:FROM . "[books]/str/cat.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::CAT)))))) (VALUE-TRIPLE (QUOTE STR::CAT))))) (7 RECORD-EXPANSION (DEFSECTION STR::APPEND-CHARS :PARENTS (STR::CONCATENATION) :SHORT "Append a string's characters onto a list." :LONG "<p>@(call append-chars) takes the characters from the string @('x')
and appends them onto @('y').</p>

<p>Its logical definition is nothing more than @('(append (explode x) y)').</p>

<p>In the execution, we traverse the string @('x') using @(see char) to avoid
the overhead of @(see coerce)-ing it into a character list before performing
the @(see append).  This reduces the overhead from @('2n') conses to @('n')
conses, where @('n') is the length of @('x').</p>" (DEFUND STR::APPEND-CHARS-AUX (X N Y) "Appends the characters from x[0:n] onto y" (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) N) (XARGS :GUARD (< N (LENGTH X)))) (IF (ZP N) (CONS (CHAR X 0) Y) (STR::APPEND-CHARS-AUX X (THE (INTEGER 0 *) (- N 1)) (CONS (CHAR X N) Y)))) (LOCAL (DEFTHM STR::LEMMA (IMPLIES (AND (NOT (ZP N)) (<= N (LEN X))) (EQUAL (APPEND (TAKE (- N 1) X) (CONS (NTH (- N 1) X) Y)) (APPEND (TAKE N X) Y))) :HINTS (("goal" :IN-THEORY (ENABLE TAKE-REDEFINITION) :INDUCT (TAKE N X))))) (DEFTHM STR::APPEND-CHARS-AUX-CORRECT (IMPLIES (AND (STRINGP X) (NATP N) (< N (LENGTH X))) (EQUAL (STR::APPEND-CHARS-AUX X N Y) (APPEND (TAKE (+ 1 N) (EXPLODE X)) Y))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::APPEND-CHARS-AUX) :INDUCT (STR::APPEND-CHARS-AUX X N Y)))) (LOCAL (IN-THEORY (DISABLE STR::APPEND-CHARS-AUX-CORRECT))) (LOCAL (DEFTHM STR::APPEND-CHARS-AUX-CORRECT-BETTER (IMPLIES (AND (STRINGP X) (NATP N) (< N (LENGTH X))) (EQUAL (STR::APPEND-CHARS-AUX X N Y) (APPEND (TAKE (+ 1 N) (EXPLODE X)) Y))) :HINTS (("Goal" :USE ((:INSTANCE STR::APPEND-CHARS-AUX-CORRECT)))))) (DEFINLINED STR::APPEND-CHARS (X Y) (DECLARE (TYPE STRING X)) (MBE :LOGIC (APPEND (EXPLODE X) Y) :EXEC (B* (((THE (INTEGER 0 *) STR::XL) (LENGTH X)) ((WHEN (EQL STR::XL 0)) Y) ((THE (INTEGER 0 *) N) (- STR::XL 1))) (STR::APPEND-CHARS-AUX X N Y)))) (LOCAL (IN-THEORY (ENABLE STR::APPEND-CHARS))) (DEFTHM STR::CHARACTER-LISTP-OF-APPEND-CHARS (EQUAL (CHARACTER-LISTP (STR::APPEND-CHARS X Y)) (CHARACTER-LISTP Y))) (DEFCONG STR::STREQV EQUAL (STR::APPEND-CHARS X Y) 1) (DEFCONG STR::ISTREQV STR::ICHARLISTEQV (STR::APPEND-CHARS X Y) 1) (DEFCONG LIST-EQUIV LIST-EQUIV (STR::APPEND-CHARS X Y) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (STR::APPEND-CHARS X Y) 2) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::APPEND-CHARS X Y) 2)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::APPEND-CHARS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::APPEND-CHARS-AUX (X N Y) "Appends the characters from x[0:n] onto y" (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) N) (XARGS :GUARD (< N (LENGTH X)))) (IF (ZP N) (CONS (CHAR X 0) Y) (STR::APPEND-CHARS-AUX X (THE (INTEGER 0 *) (- N 1)) (CONS (CHAR X N) Y)))) (LOCAL (DEFTHM STR::LEMMA (IMPLIES (AND (NOT (ZP N)) (<= N (LEN X))) (EQUAL (APPEND (TAKE (- N 1) X) (CONS (NTH (- N 1) X) Y)) (APPEND (TAKE N X) Y))) :HINTS (("goal" :IN-THEORY (ENABLE TAKE-REDEFINITION) :INDUCT (TAKE N X))))) (DEFTHM STR::APPEND-CHARS-AUX-CORRECT (IMPLIES (AND (STRINGP X) (NATP N) (< N (LENGTH X))) (EQUAL (STR::APPEND-CHARS-AUX X N Y) (APPEND (TAKE (+ 1 N) (EXPLODE X)) Y))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::APPEND-CHARS-AUX) :INDUCT (STR::APPEND-CHARS-AUX X N Y)))) (LOCAL (IN-THEORY (DISABLE STR::APPEND-CHARS-AUX-CORRECT))) (LOCAL (DEFTHM STR::APPEND-CHARS-AUX-CORRECT-BETTER (IMPLIES (AND (STRINGP X) (NATP N) (< N (LENGTH X))) (EQUAL (STR::APPEND-CHARS-AUX X N Y) (APPEND (TAKE (+ 1 N) (EXPLODE X)) Y))) :HINTS (("Goal" :USE ((:INSTANCE STR::APPEND-CHARS-AUX-CORRECT)))))) (DEFINLINED STR::APPEND-CHARS (X Y) (DECLARE (TYPE STRING X)) (MBE :LOGIC (APPEND (EXPLODE X) Y) :EXEC (B* (((THE (INTEGER 0 *) STR::XL) (LENGTH X)) ((WHEN (EQL STR::XL 0)) Y) ((THE (INTEGER 0 *) N) (- STR::XL 1))) (STR::APPEND-CHARS-AUX X N Y)))) (LOCAL (IN-THEORY (ENABLE STR::APPEND-CHARS))) (DEFTHM STR::CHARACTER-LISTP-OF-APPEND-CHARS (EQUAL (CHARACTER-LISTP (STR::APPEND-CHARS X Y)) (CHARACTER-LISTP Y))) (DEFCONG STR::STREQV EQUAL (STR::APPEND-CHARS X Y) 1) (DEFCONG STR::ISTREQV STR::ICHARLISTEQV (STR::APPEND-CHARS X Y) 1) (DEFCONG LIST-EQUIV LIST-EQUIV (STR::APPEND-CHARS X Y) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (STR::APPEND-CHARS X Y) 2) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::APPEND-CHARS X Y) 2))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::APPEND-CHARS)) (XDOC::PARENTS (QUOTE (STR::CONCATENATION))) (XDOC::SHORT (QUOTE "Append a string's characters onto a list.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::APPEND-CHARS))) 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>@(call append-chars) takes the characters from the string @('x')
and appends them onto @('y').</p>

<p>Its logical definition is nothing more than @('(append (explode x) y)').</p>

<p>In the execution, we traverse the string @('x') using @(see char) to avoid
the overhead of @(see coerce)-ing it into a character list before performing
the @(see append).  This reduces the overhead from @('2n') conses to @('n')
conses, where @('n') is the length of @('x').</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 . STR::APPEND-CHARS) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CONCATENATION) (:SHORT . "Append a string's characters onto a list.") (:LONG . "<p>@(call append-chars) takes the characters from the string @('x')
and appends them onto @('y').</p>

<p>Its logical definition is nothing more than @('(append (explode x) y)').</p>

<p>In the execution, we traverse the string @('x') using @(see char) to avoid
the overhead of @(see coerce)-ing it into a character list before performing
the @(see append).  This reduces the overhead from @('2n') conses to @('n')
conses, where @('n') is the length of @('x').</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|APPEND-CHARS-AUX|)
@(def |STR|::|APPEND-CHARS-AUX-CORRECT|)
@(def |STR|::|APPEND-CHARS$INLINE|)
@(def |STR|::|CHARACTER-LISTP-OF-APPEND-CHARS|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-APPEND-CHARS-1|)
@(def |STR|::|ISTREQV-IMPLIES-ICHARLISTEQV-APPEND-CHARS-1|)
@(def |ACL2|::|LIST-EQUIV-IMPLIES-LIST-EQUIV-APPEND-CHARS-2|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-APPEND-CHARS-2|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-ICHARLISTEQV-APPEND-CHARS-2|)") (:FROM . "[books]/str/cat.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::APPEND-CHARS)))))) (VALUE-TRIPLE (QUOTE STR::APPEND-CHARS))))) (8 RECORD-EXPANSION (DEFSECTION STR::REVAPPEND-CHARS :PARENTS (STR::CONCATENATION) :SHORT "Append a string's characters onto a list, in reverse order." :LONG "<p>@(call revappend-chars) takes the characters from the string
@('x'), reverses them, and appends the result onto @('y').</p>

<p>Its logical definition is nothing more than @('(revappend (explode x) y)').</p>

<p>In the execution, we traverse the string @('x') using @(see char) to avoid
the overhead of @(see coerce)-ing it into a character list before performing
the @(see revappend).  This reduces the overhead from @('2n') conses to @('n')
conses, where @('n') is the length of @('x').</p>

<p>This function may seem strange at first glance, but it provides a convenient
way to efficiently, incrementally build a string out of small parts.  For
instance, a sequence such as:</p>

@({
 (let* ((acc nil)
        (acc (str::revappend-chars \"Hello, \" acc))
        (acc (str::revappend-chars \"World!\" acc))
        (acc ...))
    (reverse (implode acc)))
})

<p>Is essentially the same as:</p>

@({
 (let* ((acc \"\")
        (acc (str::cat acc \"Hello, \"))
        (acc (str::cat acc \"World!\"))
        (acc ...))
   acc)
})

<p>But it is comparably much more efficient because it avoids the creation of
the intermediate strings.  See the performance discussion in @(see str::cat)
for more details.  Also see @(see rchars-to-string), which is a potentially
more efficient way to do the final @(see reverse)/@(see coerce) steps.</p>" (DEFUND STR::REVAPPEND-CHARS-AUX (X N STR::XL Y) (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) N STR::XL) (XARGS :GUARD (AND (<= N STR::XL) (EQUAL STR::XL (LENGTH X))) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (EQL N STR::XL)) Y (STR::REVAPPEND-CHARS-AUX X (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX N)))) STR::XL (CONS (CHAR X N) Y)))) (DEFTHM STR::REVAPPEND-CHARS-AUX-CORRECT (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (<= N STR::XL) (EQUAL STR::XL (LENGTH X))) (EQUAL (STR::REVAPPEND-CHARS-AUX X N STR::XL Y) (REVAPPEND (NTHCDR N (EXPLODE X)) Y))) :HINTS (("Goal" :IN-THEORY (E/D (STR::REVAPPEND-CHARS-AUX) (REVAPPEND-REMOVAL)) :INDUCT (STR::REVAPPEND-CHARS-AUX X N STR::XL Y)))) (DEFINLINED STR::REVAPPEND-CHARS (X Y) (DECLARE (XARGS :GUARD (STRINGP X)) (TYPE STRING X)) (MBE :LOGIC (REVAPPEND (EXPLODE X) Y) :EXEC (STR::REVAPPEND-CHARS-AUX X 0 (LENGTH X) Y))) (LOCAL (IN-THEORY (ENABLE STR::REVAPPEND-CHARS))) (DEFTHM STR::CHARACTER-LISTP-OF-REVAPPEND-CHARS (EQUAL (CHARACTER-LISTP (STR::REVAPPEND-CHARS X Y)) (CHARACTER-LISTP Y))) (DEFCONG STR::STREQV EQUAL (STR::REVAPPEND-CHARS X Y) 1) (DEFCONG STR::ISTREQV STR::ICHARLISTEQV (STR::REVAPPEND-CHARS X Y) 1) (DEFCONG LIST-EQUIV LIST-EQUIV (STR::REVAPPEND-CHARS X Y) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (STR::REVAPPEND-CHARS X Y) 2) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::REVAPPEND-CHARS X Y) 2)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::REVAPPEND-CHARS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::REVAPPEND-CHARS-AUX (X N STR::XL Y) (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) N STR::XL) (XARGS :GUARD (AND (<= N STR::XL) (EQUAL STR::XL (LENGTH X))) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (EQL N STR::XL)) Y (STR::REVAPPEND-CHARS-AUX X (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX N)))) STR::XL (CONS (CHAR X N) Y)))) (DEFTHM STR::REVAPPEND-CHARS-AUX-CORRECT (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (<= N STR::XL) (EQUAL STR::XL (LENGTH X))) (EQUAL (STR::REVAPPEND-CHARS-AUX X N STR::XL Y) (REVAPPEND (NTHCDR N (EXPLODE X)) Y))) :HINTS (("Goal" :IN-THEORY (E/D (STR::REVAPPEND-CHARS-AUX) (REVAPPEND-REMOVAL)) :INDUCT (STR::REVAPPEND-CHARS-AUX X N STR::XL Y)))) (DEFINLINED STR::REVAPPEND-CHARS (X Y) (DECLARE (XARGS :GUARD (STRINGP X)) (TYPE STRING X)) (MBE :LOGIC (REVAPPEND (EXPLODE X) Y) :EXEC (STR::REVAPPEND-CHARS-AUX X 0 (LENGTH X) Y))) (LOCAL (IN-THEORY (ENABLE STR::REVAPPEND-CHARS))) (DEFTHM STR::CHARACTER-LISTP-OF-REVAPPEND-CHARS (EQUAL (CHARACTER-LISTP (STR::REVAPPEND-CHARS X Y)) (CHARACTER-LISTP Y))) (DEFCONG STR::STREQV EQUAL (STR::REVAPPEND-CHARS X Y) 1) (DEFCONG STR::ISTREQV STR::ICHARLISTEQV (STR::REVAPPEND-CHARS X Y) 1) (DEFCONG LIST-EQUIV LIST-EQUIV (STR::REVAPPEND-CHARS X Y) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (STR::REVAPPEND-CHARS X Y) 2) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::REVAPPEND-CHARS X Y) 2))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::REVAPPEND-CHARS)) (XDOC::PARENTS (QUOTE (STR::CONCATENATION))) (XDOC::SHORT (QUOTE "Append a string's characters onto a list, in reverse order.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::REVAPPEND-CHARS))) 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>@(call revappend-chars) takes the characters from the string
@('x'), reverses them, and appends the result onto @('y').</p>

<p>Its logical definition is nothing more than @('(revappend (explode x) y)').</p>

<p>In the execution, we traverse the string @('x') using @(see char) to avoid
the overhead of @(see coerce)-ing it into a character list before performing
the @(see revappend).  This reduces the overhead from @('2n') conses to @('n')
conses, where @('n') is the length of @('x').</p>

<p>This function may seem strange at first glance, but it provides a convenient
way to efficiently, incrementally build a string out of small parts.  For
instance, a sequence such as:</p>

@({
 (let* ((acc nil)
        (acc (str::revappend-chars \"Hello, \" acc))
        (acc (str::revappend-chars \"World!\" acc))
        (acc ...))
    (reverse (implode acc)))
})

<p>Is essentially the same as:</p>

@({
 (let* ((acc \"\")
        (acc (str::cat acc \"Hello, \"))
        (acc (str::cat acc \"World!\"))
        (acc ...))
   acc)
})

<p>But it is comparably much more efficient because it avoids the creation of
the intermediate strings.  See the performance discussion in @(see str::cat)
for more details.  Also see @(see rchars-to-string), which is a potentially
more efficient way to do the final @(see reverse)/@(see coerce) steps.</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 . STR::REVAPPEND-CHARS) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CONCATENATION) (:SHORT . "Append a string's characters onto a list, in reverse order.") (:LONG . "<p>@(call revappend-chars) takes the characters from the string
@('x'), reverses them, and appends the result onto @('y').</p>

<p>Its logical definition is nothing more than @('(revappend (explode x) y)').</p>

<p>In the execution, we traverse the string @('x') using @(see char) to avoid
the overhead of @(see coerce)-ing it into a character list before performing
the @(see revappend).  This reduces the overhead from @('2n') conses to @('n')
conses, where @('n') is the length of @('x').</p>

<p>This function may seem strange at first glance, but it provides a convenient
way to efficiently, incrementally build a string out of small parts.  For
instance, a sequence such as:</p>

@({
 (let* ((acc nil)
        (acc (str::revappend-chars \"Hello, \" acc))
        (acc (str::revappend-chars \"World!\" acc))
        (acc ...))
    (reverse (implode acc)))
})

<p>Is essentially the same as:</p>

@({
 (let* ((acc \"\")
        (acc (str::cat acc \"Hello, \"))
        (acc (str::cat acc \"World!\"))
        (acc ...))
   acc)
})

<p>But it is comparably much more efficient because it avoids the creation of
the intermediate strings.  See the performance discussion in @(see str::cat)
for more details.  Also see @(see rchars-to-string), which is a potentially
more efficient way to do the final @(see reverse)/@(see coerce) steps.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|REVAPPEND-CHARS-AUX|)
@(def |STR|::|REVAPPEND-CHARS-AUX-CORRECT|)
@(def |STR|::|REVAPPEND-CHARS$INLINE|)
@(def |STR|::|CHARACTER-LISTP-OF-REVAPPEND-CHARS|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-REVAPPEND-CHARS-1|)
@(def |STR|::|ISTREQV-IMPLIES-ICHARLISTEQV-REVAPPEND-CHARS-1|)
@(def |ACL2|::|LIST-EQUIV-IMPLIES-LIST-EQUIV-REVAPPEND-CHARS-2|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-REVAPPEND-CHARS-2|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-ICHARLISTEQV-REVAPPEND-CHARS-2|)") (:FROM . "[books]/str/cat.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::REVAPPEND-CHARS)))))) (VALUE-TRIPLE (QUOTE STR::REVAPPEND-CHARS))))) (9 RECORD-EXPANSION (DEFSECTION STR::PREFIX-STRINGS :PARENTS (STR::CONCATENATION) :SHORT "Concatenates a prefix onto every string in a list of strings." :LONG "<p>@(call prefix-strings) produces a new string list by concatenating
@('prefix') onto every member of @('x').</p>" (DEFUND STR::PREFIX-STRINGS (STR::PREFIX X) (DECLARE (TYPE STRING STR::PREFIX) (XARGS :GUARD (STRING-LISTP X))) (IF (ATOM X) NIL (CONS (STR::CAT STR::PREFIX (CAR X)) (STR::PREFIX-STRINGS STR::PREFIX (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::PREFIX-STRINGS))) (DEFTHM STR::PREFIX-STRINGS-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::PREFIX-STRINGS STR::PREFIX X) NIL))) (DEFTHM STR::PREFIX-STRINGS-OF-CONS (EQUAL (STR::PREFIX-STRINGS STR::PREFIX (CONS A X)) (CONS (STR::CAT STR::PREFIX A) (STR::PREFIX-STRINGS STR::PREFIX X)))) (DEFTHM STR::STRING-LISTP-OF-PREFIX-STRINGS (STRING-LISTP (STR::PREFIX-STRINGS STR::PREFIX X))) (DEFTHM STR::LEN-OF-PREFIX-STRINGS (EQUAL (LEN (STR::PREFIX-STRINGS STR::PREFIX X)) (LEN X))) (DEFCONG STR::STREQV EQUAL (STR::PREFIX-STRINGS STR::PREFIX X) 1) (LOCAL (DEFTHMD STR::L0 (EQUAL (STR::PREFIX-STRINGS STR::PREFIX (LIST-FIX X)) (STR::PREFIX-STRINGS STR::PREFIX X)))) (DEFCONG LIST-EQUIV EQUAL (STR::PREFIX-STRINGS STR::PREFIX X) 2 :HINTS (("Goal" :IN-THEORY (ENABLE LIST-EQUIV) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::PREFIX-STRINGS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::PREFIX-STRINGS (STR::PREFIX X) (DECLARE (TYPE STRING STR::PREFIX) (XARGS :GUARD (STRING-LISTP X))) (IF (ATOM X) NIL (CONS (STR::CAT STR::PREFIX (CAR X)) (STR::PREFIX-STRINGS STR::PREFIX (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::PREFIX-STRINGS))) (DEFTHM STR::PREFIX-STRINGS-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::PREFIX-STRINGS STR::PREFIX X) NIL))) (DEFTHM STR::PREFIX-STRINGS-OF-CONS (EQUAL (STR::PREFIX-STRINGS STR::PREFIX (CONS A X)) (CONS (STR::CAT STR::PREFIX A) (STR::PREFIX-STRINGS STR::PREFIX X)))) (DEFTHM STR::STRING-LISTP-OF-PREFIX-STRINGS (STRING-LISTP (STR::PREFIX-STRINGS STR::PREFIX X))) (DEFTHM STR::LEN-OF-PREFIX-STRINGS (EQUAL (LEN (STR::PREFIX-STRINGS STR::PREFIX X)) (LEN X))) (DEFCONG STR::STREQV EQUAL (STR::PREFIX-STRINGS STR::PREFIX X) 1) (LOCAL (DEFTHMD STR::L0 (EQUAL (STR::PREFIX-STRINGS STR::PREFIX (LIST-FIX X)) (STR::PREFIX-STRINGS STR::PREFIX X)))) (DEFCONG LIST-EQUIV EQUAL (STR::PREFIX-STRINGS STR::PREFIX X) 2 :HINTS (("Goal" :IN-THEORY (ENABLE LIST-EQUIV) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV)))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::PREFIX-STRINGS)) (XDOC::PARENTS (QUOTE (STR::CONCATENATION))) (XDOC::SHORT (QUOTE "Concatenates a prefix onto every string in a list of strings.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::PREFIX-STRINGS))) 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>@(call prefix-strings) produces a new string list by concatenating
@('prefix') onto every member of @('x').</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 . STR::PREFIX-STRINGS) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CONCATENATION) (:SHORT . "Concatenates a prefix onto every string in a list of strings.") (:LONG . "<p>@(call prefix-strings) produces a new string list by concatenating
@('prefix') onto every member of @('x').</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|PREFIX-STRINGS|)
@(def |STR|::|PREFIX-STRINGS-WHEN-ATOM|)
@(def |STR|::|PREFIX-STRINGS-OF-CONS|)
@(def |STR|::|STRING-LISTP-OF-PREFIX-STRINGS|)
@(def |STR|::|LEN-OF-PREFIX-STRINGS|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-PREFIX-STRINGS-1|)
@(def |ACL2|::|LIST-EQUIV-IMPLIES-EQUAL-PREFIX-STRINGS-2|)") (:FROM . "[books]/str/cat.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::PREFIX-STRINGS)))))) (VALUE-TRIPLE (QUOTE STR::PREFIX-STRINGS))))) (10 RECORD-EXPANSION (DEFSECTION STR::RCHARS-TO-STRING :PARENTS (STR::CONCATENATION) :SHORT "Possibly optimized way to reverse a character list and coerce it to a
string." :LONG "<p>@(call rchars-to-string) is logically equal to</p>

@({
   (reverse (coerce rchars 'string))
})

<p>We leave it enabled and would not expect to ever reason about it.  This
operation is useful as the final step in a string-building strategy where
characters are accumulated onto a list in reverse order; see for instance @(see
revappend-chars).</p>

<p>When you just load books like @('str/top') or @('str/cat'), this logical
definition is exactly what gets executed.  This definition is not too bad, and
doing the @(see coerce) first means that the @(see reverse) is done on a
string (i.e., an array) instead of a list, which is generally efficient.</p>

<p>But if you are willing to accept a trust tag, then you may <b>optionally</b>
load the book:</p>

@({
  (include-book \"str/fast-cat\" :dir :system)
})

<p>This may improve the performance of @('rchars-to-string') by replacing the
@(see reverse) call with a call of @('nreverse').  We can \"obviously\" see
that this is safe since the string produced by the @('coerce') is not visible
to any other part of the program.</p>" (DEFUN STR::RCHARS-TO-STRING (STR::RCHARS) "May be redefined under-the-hood in str/fast-cat.lisp" (DECLARE (XARGS :GUARD (CHARACTER-LISTP STR::RCHARS))) (THE STRING (REVERSE (THE STRING (COERCE (THE LIST STR::RCHARS) (QUOTE STRING))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::RCHARS-TO-STRING)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUN STR::RCHARS-TO-STRING (STR::RCHARS) "May be redefined under-the-hood in str/fast-cat.lisp" (DECLARE (XARGS :GUARD (CHARACTER-LISTP STR::RCHARS))) (THE STRING (REVERSE (THE STRING (COERCE (THE LIST STR::RCHARS) (QUOTE STRING)))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::RCHARS-TO-STRING)) (XDOC::PARENTS (QUOTE (STR::CONCATENATION))) (XDOC::SHORT (QUOTE "Possibly optimized way to reverse a character list and coerce it to a
string.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::RCHARS-TO-STRING))) 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>@(call rchars-to-string) is logically equal to</p>

@({
   (reverse (coerce rchars 'string))
})

<p>We leave it enabled and would not expect to ever reason about it.  This
operation is useful as the final step in a string-building strategy where
characters are accumulated onto a list in reverse order; see for instance @(see
revappend-chars).</p>

<p>When you just load books like @('str/top') or @('str/cat'), this logical
definition is exactly what gets executed.  This definition is not too bad, and
doing the @(see coerce) first means that the @(see reverse) is done on a
string (i.e., an array) instead of a list, which is generally efficient.</p>

<p>But if you are willing to accept a trust tag, then you may <b>optionally</b>
load the book:</p>

@({
  (include-book \"str/fast-cat\" :dir :system)
})

<p>This may improve the performance of @('rchars-to-string') by replacing the
@(see reverse) call with a call of @('nreverse').  We can \"obviously\" see
that this is safe since the string produced by the @('coerce') is not visible
to any other part of the program.</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 . STR::RCHARS-TO-STRING) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CONCATENATION) (:SHORT . "Possibly optimized way to reverse a character list and coerce it to a
string.") (:LONG . "<p>@(call rchars-to-string) is logically equal to</p>

@({
   (reverse (coerce rchars 'string))
})

<p>We leave it enabled and would not expect to ever reason about it.  This
operation is useful as the final step in a string-building strategy where
characters are accumulated onto a list in reverse order; see for instance @(see
revappend-chars).</p>

<p>When you just load books like @('str/top') or @('str/cat'), this logical
definition is exactly what gets executed.  This definition is not too bad, and
doing the @(see coerce) first means that the @(see reverse) is done on a
string (i.e., an array) instead of a list, which is generally efficient.</p>

<p>But if you are willing to accept a trust tag, then you may <b>optionally</b>
load the book:</p>

@({
  (include-book \"str/fast-cat\" :dir :system)
})

<p>This may improve the performance of @('rchars-to-string') by replacing the
@(see reverse) call with a call of @('nreverse').  We can \"obviously\" see
that this is safe since the string produced by the @('coerce') is not visible
to any other part of the program.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|RCHARS-TO-STRING|)") (:FROM . "[books]/str/cat.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::RCHARS-TO-STRING)))))) (VALUE-TRIPLE (QUOTE STR::RCHARS-TO-STRING))))) (11 RECORD-EXPANSION (DEFSECTION STR::JOIN :PARENTS (STR::CONCATENATION) :SHORT "Concatenate a list of strings with some separator between." :LONG "<p>@(call join) joins together the list of strings @('x'), inserting
the string @('separator') between the members.  For example:</p>

@({
 (join '(\"a\" \"b\" \"c\") \".\") = \"a.b.c\"
 (join '(\"a\" \"b\" \"c\") \"->\") = \"a->b->c\"
})

<p>We always return a string; an empty @('x') results in the empty string, and
any empty strings within @('x') just implicitly don't contribute to the
result.</p>

<p>Any sort of string concatenation is slow, but @('join') is reasonably
efficient: it creates a single character list for the result (in reverse order)
without any use of @(see coerce), then uses @(see rchars-to-string) to build
and reverse the result string.</p>" (DEFUND STR::JOIN-AUX (X STR::SEPARATOR STR::ACC) (DECLARE (XARGS :GUARD (STRING-LISTP X)) (TYPE STRING STR::SEPARATOR)) (COND ((ATOM X) STR::ACC) ((ATOM (CDR X)) (STR::REVAPPEND-CHARS (CAR X) STR::ACC)) (T (LET* ((STR::ACC (STR::REVAPPEND-CHARS (CAR X) STR::ACC)) (STR::ACC (STR::REVAPPEND-CHARS STR::SEPARATOR STR::ACC))) (STR::JOIN-AUX (CDR X) STR::SEPARATOR STR::ACC))))) (DEFUND STR::JOIN (X STR::SEPARATOR) (DECLARE (TYPE STRING STR::SEPARATOR)) (DECLARE (XARGS :GUARD (STRING-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (COND ((ATOM X) "") ((ATOM (CDR X)) (IF (STRINGP (CAR X)) (CAR X) "")) (T (STR::CAT (CAR X) STR::SEPARATOR (STR::JOIN (CDR X) STR::SEPARATOR)))) :EXEC (STR::RCHARS-TO-STRING (STR::JOIN-AUX X STR::SEPARATOR NIL)))) (LOCAL (IN-THEORY (ENABLE STR::JOIN STR::JOIN-AUX))) (DEFTHM STR::JOIN-AUX-REMOVAL (IMPLIES (AND (STRING-LISTP X) (STRINGP STR::SEPARATOR)) (EQUAL (STR::JOIN-AUX X STR::SEPARATOR STR::ACC) (REVAPPEND (COERCE (STR::JOIN X STR::SEPARATOR) (QUOTE LIST)) STR::ACC))) :HINTS (("Goal" :INDUCT (STR::JOIN-AUX X STR::SEPARATOR STR::ACC) :IN-THEORY (ENABLE STR::REVAPPEND-CHARS)))) (VERIFY-GUARDS STR::JOIN) (DEFTHM STR::STRINGP-OF-JOIN (STRINGP (STR::JOIN X STR::SEPARATOR)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (EQUAL (STR::JOIN (LIST-FIX X) STR::SEPARATOR) (STR::JOIN X STR::SEPARATOR)))) (DEFCONG LIST-EQUIV EQUAL (STR::JOIN X STR::SEPARATOR) 1 :HINTS (("Goal" :IN-THEORY (ENABLE LIST-EQUIV) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV)))))) (DEFCONG STR::STREQV EQUAL (STR::JOIN X STR::SEPARATOR) 2) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::JOIN X STR::SEPARATOR) 2)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::JOIN)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::JOIN-AUX (X STR::SEPARATOR STR::ACC) (DECLARE (XARGS :GUARD (STRING-LISTP X)) (TYPE STRING STR::SEPARATOR)) (COND ((ATOM X) STR::ACC) ((ATOM (CDR X)) (STR::REVAPPEND-CHARS (CAR X) STR::ACC)) (T (LET* ((STR::ACC (STR::REVAPPEND-CHARS (CAR X) STR::ACC)) (STR::ACC (STR::REVAPPEND-CHARS STR::SEPARATOR STR::ACC))) (STR::JOIN-AUX (CDR X) STR::SEPARATOR STR::ACC))))) (DEFUND STR::JOIN (X STR::SEPARATOR) (DECLARE (TYPE STRING STR::SEPARATOR)) (DECLARE (XARGS :GUARD (STRING-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (COND ((ATOM X) "") ((ATOM (CDR X)) (IF (STRINGP (CAR X)) (CAR X) "")) (T (STR::CAT (CAR X) STR::SEPARATOR (STR::JOIN (CDR X) STR::SEPARATOR)))) :EXEC (STR::RCHARS-TO-STRING (STR::JOIN-AUX X STR::SEPARATOR NIL)))) (LOCAL (IN-THEORY (ENABLE STR::JOIN STR::JOIN-AUX))) (DEFTHM STR::JOIN-AUX-REMOVAL (IMPLIES (AND (STRING-LISTP X) (STRINGP STR::SEPARATOR)) (EQUAL (STR::JOIN-AUX X STR::SEPARATOR STR::ACC) (REVAPPEND (COERCE (STR::JOIN X STR::SEPARATOR) (QUOTE LIST)) STR::ACC))) :HINTS (("Goal" :INDUCT (STR::JOIN-AUX X STR::SEPARATOR STR::ACC) :IN-THEORY (ENABLE STR::REVAPPEND-CHARS)))) (VERIFY-GUARDS STR::JOIN) (DEFTHM STR::STRINGP-OF-JOIN (STRINGP (STR::JOIN X STR::SEPARATOR)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (EQUAL (STR::JOIN (LIST-FIX X) STR::SEPARATOR) (STR::JOIN X STR::SEPARATOR)))) (DEFCONG LIST-EQUIV EQUAL (STR::JOIN X STR::SEPARATOR) 1 :HINTS (("Goal" :IN-THEORY (ENABLE LIST-EQUIV) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV)))))) (DEFCONG STR::STREQV EQUAL (STR::JOIN X STR::SEPARATOR) 2) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::JOIN X STR::SEPARATOR) 2))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::JOIN)) (XDOC::PARENTS (QUOTE (STR::CONCATENATION))) (XDOC::SHORT (QUOTE "Concatenate a list of strings with some separator between.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::JOIN))) 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>@(call join) joins together the list of strings @('x'), inserting
the string @('separator') between the members.  For example:</p>

@({
 (join '(\"a\" \"b\" \"c\") \".\") = \"a.b.c\"
 (join '(\"a\" \"b\" \"c\") \"->\") = \"a->b->c\"
})

<p>We always return a string; an empty @('x') results in the empty string, and
any empty strings within @('x') just implicitly don't contribute to the
result.</p>

<p>Any sort of string concatenation is slow, but @('join') is reasonably
efficient: it creates a single character list for the result (in reverse order)
without any use of @(see coerce), then uses @(see rchars-to-string) to build
and reverse the result string.</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 . STR::JOIN) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CONCATENATION) (:SHORT . "Concatenate a list of strings with some separator between.") (:LONG . "<p>@(call join) joins together the list of strings @('x'), inserting
the string @('separator') between the members.  For example:</p>

@({
 (join '(\"a\" \"b\" \"c\") \".\") = \"a.b.c\"
 (join '(\"a\" \"b\" \"c\") \"->\") = \"a->b->c\"
})

<p>We always return a string; an empty @('x') results in the empty string, and
any empty strings within @('x') just implicitly don't contribute to the
result.</p>

<p>Any sort of string concatenation is slow, but @('join') is reasonably
efficient: it creates a single character list for the result (in reverse order)
without any use of @(see coerce), then uses @(see rchars-to-string) to build
and reverse the result string.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|JOIN-AUX|)
@(def |STR|::|JOIN|)
@(def |STR|::|JOIN-AUX-REMOVAL|)
@(def |STR|::|STRINGP-OF-JOIN|)
@(def |ACL2|::|LIST-EQUIV-IMPLIES-EQUAL-JOIN-1|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-JOIN-2|)
@(def |STR|::|ISTREQV-IMPLIES-ISTREQV-JOIN-2|)") (:FROM . "[books]/str/cat.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::JOIN)))))) (VALUE-TRIPLE (QUOTE STR::JOIN))))))
(("/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/str/cat.lisp" "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/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/std/lists/same-lengthp.lisp" "same-lengthp" "same-lengthp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2063823673)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/mfc-utils.lisp" "mfc-utils" "mfc-utils" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1043482843)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/rcons.lisp" "rcons" "rcons" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105042482)) (LOCAL ("/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)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854)) (LOCAL ("/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/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/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)) (LOCAL ("/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)) (LOCAL ("/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) (LOCAL ("/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)) (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/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/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/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))
526058003