1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
<html>
<head><title>CHARACTERS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>CHARACTERS</h2>characters in ACL2
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
ACL2 accepts 256 distinct characters, which are the characters
obtained by applying the function <code><a href="CODE-CHAR.html">code-char</a></code> to each integer from <code>0</code>
to <code>255</code>. Among these, Common Lisp designates certain ones as
<em>standard characters</em>, namely those of the form <code>(code-char n)</code>
where <code>n</code> is from <code>33</code> to <code>126</code>, together with <code>#\Newline</code> and <code>#\Space</code>. The
actual standard characters may be viewed by evaluating the
<code><a href="DEFCONST.html">defconst</a></code> <code>*standard-chars*</code>.
<p>
To be more precise, Common Lisp does not specify the precise
relationship between <code><a href="CODE-CHAR.html">code-char</a></code> 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 <code><a href="CHAR-CODE.html">char-code</a></code>s <tt>32</tt>, <tt>9</tt>,
<tt>10</tt>, <tt>12</tt>, and <tt>127</tt>.<p>
<code><a href="CODE-CHAR.html">Code-char</a></code> has an inverse, <code><a href="CHAR-CODE.html">char-code</a></code>. Thus, when <code><a href="CHAR-CODE.html">char-code</a></code> is
applied to an ACL2 character, <code>c</code>, it returns a number <code>n</code> between <code>0</code> and
<code>255</code> inclusive such that <code>(code-char n)</code> = <code>c</code>.<p>
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.<p>
<em>The Character Reader</em><p>
ACL2 supports the `<code>#\</code>' notation for characters provided by Common
Lisp, with some restrictions. First of all, for every character <code>c</code>,
the notation
<pre>
#\c
</pre>
may be used to denote the character object <code>c</code>. That is, the user may
type in this notation and ACL2 will read it as denoting the
character object <code>c</code>. In this case, the character immediately
following <code>c</code> must be one of the following ``terminating characters'':
a Tab, a Newline, a Page character, a space, or one of the
characters:
<pre>
" ' ( ) ; ` ,
</pre>
Other than the notation above, ACL2 accepts alternate notation for
five characters.
<pre>
#\Space
#\Tab
#\Newline
#\Page
#\Rubout
</pre>
<p>
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 <code>#\</code> syntax for entering
characters other than that described above.<p>
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.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
