		Search-engine friendly clone of the ACL2 documentation.

Concatenation

Rchars-to-string

Possibly optimized way to reverse a character list and coerce it to a string.

(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

Function: rchars-to-string

(defun rchars-to-string (rchars)
       (declare (xargs :guard (character-listp rchars)))
       (reverse (the string (coerce rchars 'string))))