Possibly optimized way to reverse a character list and coerce it to a
(rchars-to-string rchars) is logically equal to
(reverse (implode rchars))
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 revappend-chars.
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 coerce first means that the reverse is done on a
string (i.e., an array) instead of a list, which is generally efficient.
But if you are willing to accept a trust tag, then you may optionally
load the book:
(include-book "str/fast-cat" :dir :system)
This may improve the performance of rchars-to-string by replacing the
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.
Definitions and Theorems
(defun rchars-to-string (rchars)
(declare (xargs :guard (character-listp rchars)))
(reverse (the string (coerce rchars 'string))))