Charset-p
A way to represent a fixed set of characters.
- Signature
(charset-p x) → bool
- Returns
- bool — Type (booleanp bool).
When writing a lexer, it is often useful to introduce character
sets that recognize sets of characters such as whitespace, alphabetic
characters, digits, and so forth.
A charset-p represents such a set of characters as a natural number.
In this representation, the character whose code is i is a member of the
set x exactly when the ith bit of x is 1. This may as well be
thought of as a bit-array lookup.
To introduce new sets of characters, e.g., to recognize "whitespace
characters," or "hex digits," or whatever, we use the defcharset
macro.
We generally treat character sets as opaque. It would be quite odd to,
e.g., allow the theorem prover to expand a character set's definition into its
bit-mask form, or to reason about functions like logbitp in conjunction
with character sets. If you find yourself doing this, something is probably
wrong.
Definitions and Theorems
Function: charset-p
(defun charset-p (x)
(declare (xargs :guard t))
(let ((acl2::__function__ 'charset-p))
(declare (ignorable acl2::__function__))
(natp x)))
Theorem: booleanp-of-charset-p
(defthm booleanp-of-charset-p
(b* ((bool (charset-p x)))
(booleanp bool))
:rule-classes :type-prescription)
Subtopics
- Defcharset
- Define a recognizer for a particular set of characters.
- Count-leading-charset
- Count how many characters at the start of a list are members of a
particular character set.
- Str-count-leading-charset-fast
- Fixnum optimized version of str-count-leading-charset.
- Str-count-leading-charset
- String version of count-leading-charset.
- Chars-in-charset-p
- (chars-in-charset-p x set) recognizes lists of characters x
where every character is a member of the charset-p set.
- Code-in-charset-p
- (code-in-charset-p code set) determines if the character whose code is
code is a member of the character set set.
- Char-in-charset-p
- (char-in-charset-p char set) determines if the character char is a
member of the character set set.
