Std/strings
A library with many useful functions for working with strings, and
for reasoning about ACL2's built-in string operations and these new
operations.
The std/strings library is a rudimentary string library for
ACL2. The functions here are all in logic mode, with verified guards. In many
cases, some effort has been spent to make them both efficient and relatively
straightforward to reason about.
Loading the library
Note: All of the library's functions are found in the STR
package.
Ordinarily, to use the library one should run
(include-book "std/strings/top" :dir :system)
To keep the top book more lightweight, certain functionality is excluded by
default. Here are additional books you may want to include:
- std/strings/base64 — support for base64 encoding/decoding
- std/strings/pretty — support for pretty-printing ACL2 expressions
Advanced Options
If you are willing to accept a trust tag, you may also include the
fast-cat book for faster string-concatenation; see cat for
details.
If you only need some subset of the available functions, it's generally
reasonable to just include individual books instead of the top book.
However, book names and dependencies do sometimes change, so in general we
recommend just loading the top book.
If you want to be able to use the string operations but don't have any need
to reason about them, e.g., because you are writing code for macros, then you
might instead want to load either:
- std/strings/defs — logic mode definitions, minimal theorems
- std/strings/defs-program — program mode definitions, no theorems
These books may load slightly faster than the top book and may help to
minimize the effects of loading the library on your theory.
Subtopics
- Pretty-printing
- A fast, state-free, logic-mode re-implementation of
much of ACL2's built-in pretty-printing capabilities.
- Printtree
- A tree structure for building up a block of text from components.
- Base64
- Routines for Base 64 string encoding/decoding.
- Charset-p
- A way to represent a fixed set of characters.
- Strtok!
- Variant of strtok
that does not treat contiguous delimiters as one.
- Cases
- Functions for recognizing and translating between upper- and
lower-case.
- Concatenation
- Functions for joining strings together.
- Html-encoding
- Routines to encode HTML entities, e.g., < becomes <.
- Character-kinds
- Predicates that characterize various kinds of characters,
and lists of such characters.
- Substrings
- Functions for detecting substrings, prefixes, and suffixes.
- Strtok
- Tokenize a string with character delimiters.
- Equivalences
- Basic equivalence relations.
- Url-encoding
- Functions for % encoding strings for use in URLs, as described in RFC 3986.
- Lines
- Functions for operating on the lines of a string.
- Explode-implode-equalities
- Theorems about equalities involving
explode and implode.
- Ordering
- Functions for comparing and ordering strings in various ways.
- Numbers
- Functions for working with numbers in strings.
- Pad-trim
- Functions for trimming whitespace and padding with spaces.
- Coercion
- Functions for converting between strings, symbols, character lists,
and so on.
- Std/strings/digit-to-char
- Theorems about the built-in digit-to-char.
- Substitution
- Functions for doing string replacement.
- Symbols
- Functions for working with symbols.
