Characters
Characters in ACL2 and operations on them
ACL2 accepts 256 distinct characters, which are the characters
obtained by applying the function code-char to each integer from
0 to 255. Among these, Common Lisp designates certain ones as
standard characters, namely those of the form (code-char n) where
n is from 33 to 126, together with #\Newline and
#\Space. The actual standard characters may be viewed by evaluating the
defconst *standard-chars*.
To be more precise, Common Lisp does not specify the precise relationship
between code-char and the standard characters. However, we check that
the underlying Common Lisp implementation uses a particular relationship that
extends the usual ASCII coding of characters. We also check that Space, Tab,
Newline, Page, Rubout, and Return correspond to characters with respective
char-codes 32, 9, 10, 12, 127, and
13.
Code-char has an inverse, char-code. Thus, when char-code is applied to an ACL2 character, c, it returns a number n
between 0 and 255 inclusive such that (code-char n) =
c.
The preceding paragraph implies that there is only one ACL2 character with
a given character code. CLTL allows for ``attributes'' for characters, which
could allow distinct characters with the same code, but ACL2 does not allow
this.
The Character Reader
ACL2 supports the `#\' notation for characters provided by Common
Lisp, with some restrictions. First of all, for every character c, the
notation
#\c
may be used to denote the character object c. That is, the user may
type in this notation and ACL2 will read it as denoting the character object
c. In this case, the character immediately following c must be one
of the following ``terminating characters'': a Tab, a Newline, a Page
character, a space, or one of the characters:
" ' ( ) ; ` ,
Other than the notation above, ACL2 accepts alternate notation for five
characters.
#\Space
#\Tab
#\Newline
#\Page
#\Rubout
#\Return
Again, in each of these cases the next character must be from among the set
of ``terminating characters'' described in the single-character case. Our
implementation is consistent with ISO-8859-1, even though we don't provide
#\ syntax for entering characters other than that described above.
Finally, we note that it is our intention that any object printed by ACL2's
top-level-loop may be read back into ACL2. Please notify the implementors if
you find a counterexample to this claim.
Subtopics
- Character-listp
- Recognizer for a true list of characters
- Characterp
- Recognizer for characters
- Coerce
- Coerce a character list to a string and a string to a list
- Digit-char-p
- The number, if any, corresponding to a given character
- Code-char
- The character corresponding to a given numeric code
- Char-code
- The numeric code for a given character
- Char-upcase
- Turn lower-case characters into upper-case characters
- Char-downcase
- Turn upper-case characters into lower-case characters
- Standard-char-p
- Recognizer for standard characters
- Char
- The nth element (zero-based) of a string
- Alpha-char-p
- Recognizer for alphabetic characters
- Explode-nonnegative-integer
- The list of characters in the radix-r form of a number
- Upper-case-p
- Recognizer for upper case characters
- Lower-case-p
- Recognizer for lower case characters
- Explode-atom
- Convert any atom into a character-listp that contains
its printed representation, rendering numbers in your choice of print base.
- Char-equal
- Character equality without regard to case
- Digit-to-char
- Map a digit to a character
- Char<
- Less-than test for characters
- Char>=
- Greater-than-or-equal test for characters
- Make-character-list
- coerce to a list of characters
- Char>
- Greater-than test for characters
- Char<=
- Less-than-or-equal test for characters
- Standard-char-listp
- Recognizer for a true list of standard characters
- Character-alistp
- Recognizer for association lists with characters as keys
- Standard-char-p+
- Recognizer for standard characters whose guard is t
- Chars-upcase-gen
- Upcase any list of characters (even non-standard ones).
- Chars-downcase-gen
- Downcase any list of characters (even non-standard ones).
- Char-upcase-gen
- Upcase any character (even a non-standard one).
- Char-downcase-gen
- Downcase any character (even a non-standard one).
