Cat
Alternative to concatenate that has a shorter name and may in
some cases be more efficient.
Concatenating strings is a fundamentally slow operation in Common
Lisp; see concatenation.
In some Lisps, using (concatenate 'string ...) can be even worse than
the necessary cost of creating and initializing a new array. This is because
the concatenate function is quite flexible and can handle many types of
input (e.g., lists and vectors). This flexibility can cause some overhead if
the Lisp does not optimize for the 'string case.
If you are willing to accept a trust tag, then you may optionally
load the book:
(include-book "str/fast-cat" :dir :system)
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 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.
Definitions and Theorems
Function: fast-string-append
(defun fast-string-append (str1 str2)
"May be redefined under-the-hood in str/fast-cat.lisp"
(declare (type string str1 str2))
(string-append str1 str2))
Function: fast-string-append-lst
(defun 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))
