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
78
79
80
81
82
83
84
85
86
|
<html>
<head><title>TYPE-SPEC.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>TYPE-SPEC</h2>type specifiers in declarations
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<pre>
Examples:
The symbol INTEGER in (declare (type INTEGER i j k)) is a type-spec. Other
type-specs supported by ACL2 include RATIONAL, COMPLEX, (INTEGER 0 127),
(RATIONAL 1 *), CHARACTER, and ATOM.
</pre>
<p>
The type-specs and their meanings (when applied to the variable <code>x</code>
as in <code>(declare (type type-spec x))</code> are given below.
<pre>
type-spec meaning
(AND type1 ... typek) (AND (p1 X) ... (pk X))
where (pj x) is the meaning for type-spec typej
ATOM (ATOM X)
BIT (OR (EQUAL X 1) (EQUAL X 0))
CHARACTER (CHARACTERP X)
COMPLEX, (AND (COMPLEX-RATIONALP X)
(COMPLEX RATIONAL) (RATIONALP (REALPART X))
(RATIONALP (IMAGPART X)))
(COMPLEX type) (AND (COMPLEX-RATIONALP X)
(p (REALPART X))
(p (IMAGPART X)))
where (p x) is the meaning for type-spec type
CONS (CONSP X)
INTEGER (INTEGERP X)
(INTEGER i j) (AND (INTEGERP X) ; See notes below
(<= i X)
(<= X j))
(MEMBER x1 ... xn) (MEMBER X '(x1 ... xn))
(MOD i) same as (INTEGER 0 i-1)
NIL NIL
(NOT type) (NOT (p X))
where (p x) is the meaning for type-spec type
NULL (EQ X NIL)
(OR type1 ... typek) (OR (p1 X) ... (pk X))
where (pj x) is the meaning for type-spec typej
RATIO (AND (RATIONALP X) (NOT (INTEGERP X)))
RATIONAL (RATIONALP X)
(RATIONAL i j) (AND (RATIONALP X) ; See notes below
(<= i X)
(<= X j))
REAL (RATIONALP X) ; (REALP X) in ACL2(r)
(REAL i j) (AND (RATIONALP X) ; See notes below
(<= i X)
(<= X j))
(SATISFIES pred) (pred X) ; Lisp requires a unary function, not a macro
SIGNED-BYTE (INTEGERP X)
(SIGNED-BYTE i) same as (INTEGER -2**i-1 (2**i-1)-1)
STANDARD-CHAR (STANDARD-CHARP X)
STRING (STRINGP X)
(STRING max) (AND (STRINGP X) (EQUAL (LENGTH X) max))
SYMBOL (SYMBOLP X)
T T
UNSIGNED-BYTE same as (INTEGER 0 *)
(UNSIGNED-BYTE i) same as (INTEGER 0 (2**i)-1)
</pre>
<em>Notes:</em><p>
In general, <code>(integer i j)</code> means
<pre>
(AND (INTEGERP X)
(<= i X)
(<= X j)).
</pre>
But if <code>i</code> is the symbol <code>*</code>, the first inequality is omitted. If <code>j</code>
is the symbol <code>*</code>, the second inequality is omitted. If instead of
being an integer, the second element of the type specification is a
list containing an integer, <code>(i)</code>, then the first inequality is made
strict. An analogous remark holds for the <code>(j)</code> case. The <code>RATIONAL</code>
and <code>REAL</code> type specifiers are similarly generalized.
<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>
|
