CHARACTERS

characters in ACL2 
Major Section:  PROGRAMMING

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 

#\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

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.