Major Section: ACL2-BUILT-INS
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, and
Rubout correspond to characters with respective char-codes 32, 9,
10, 12, and 127.
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
#\cmay 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
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
IS0-8859, 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.
