Concatenation
Functions for joining strings together.
Efficiency Warning.
Concatenating strings in ACL2 is fundamentally slow. Why? In Common Lisp,
strings are just arrays of characters, and there is not any mechanism for
efficiently splicing together arrays. Any kind of string concatenation, then,
minimally requires creating a completely new array and copying all of the input
characters into it. This makes it especially slow to repeatedly use, e.g.,
cat to build up a string.
To build strings more efficiently, a good general strategy is to build up a
reverse-order character list, and then convert it into a string at the end.
See for instance the functions revappend-chars and rchars-to-string, which make this rather easy to do.
Subtopics
- Revappend-chars
- Append a string's characters onto a list, in reverse order.
- Join
- Concatenate a list of strings with some separator between.
- Append-chars
- Append a string's characters onto a list.
- Cat
- Alternative to concatenate that has a shorter name and may in
some cases be more efficient.
- Rchars-to-string
- Possibly optimized way to reverse a character list and coerce it to a
string.
- Prefix-strings
- Concatenates a prefix onto every string in a list of strings.
