		Search-engine friendly clone of the ACL2 documentation.

Type-spec

Type specifiers can be used in Common Lisp type declarations and the forms, and may result in improved efficiency of execution.

ACL2 permits the use of type declarations in certain contexts; see declare for background. Here is an example of a type declaration; here the symbol, integer, is what we refer to as a ``type-spec'':

(let ((x (+ a b)))
  (declare (type integer x))   ;; <-- type declaration
  (+ 1 x))

A Common Lisp compiler might be able to use the above declaration to improve the execution efficiency of the resulting code. In particular, the Common Lisp + operation is rather elaborate: it must be capable of adding together integers, rationals, floats, etc. When we tell the compiler that this x is surely an integer, it may be able to use a more efficient version of (+ 1 x) that only deals with the integer case.

Type declarations can be added to functions, let bindings, and other places as described in declare, and interact with the ACL2's guard mechanism. For instance, during guard verification, the above type declaration will result in a guard obligation: we will need to prove that (+ a b) is always an integer. Type declarations about the formals of a function generally become part of the guard of the function, but see also split-types for a way to gain more control over this.

Whether or not a particular type declaration will actually improve the efficiency of your functions depends on the Lisp compiler. For instance, many Lisp compilers will not benefit much from a plain integer declaration. If you are trying to optimize code by adding type declarations, it may be useful to use disassemble$ to inspect the impact that your declarations have on the resulting code.

While type specs may be used in defstobj events, the HASH-TABLE and STOBJ-TABLE type specs may only be used in those events. We say nothing further about them in the present topic.

Type Specs

The syntax that Common Lisp compilers use for these type declarations—e.g., the symbol integer above—is different than the usual syntax of ACL2.

We use the name type-spec to refer to the supported types that can be mentioned in declarations. For instance:

Declaration	Type-Spec
(type string x y z)	string
(type (integer 0 7) x)	(integer 0 7)
(type rational x)	rational
(type (rational 1 *) x)	(rational 1 *)

The supported type-specs and their meanings (when applied to the variable x as in (declare (type type-spec x)) are given below.

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)
                            (RATIONALP (REALPART X))
                            (RATIONALP (IMAGPART X)))
(COMPLEX RATIONAL)     same as COMPLEX, above
(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)
DOUBLE-FLOAT           (DFP X) ; See :DOC df.
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)
NUMBER                 (ACL2-NUMBERP x)
(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 k m) where k=-2^(i-1), m=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)
----------------------------------------------------------------------

Notes

In general, (integer i j) means

(AND (INTEGERP X)
     (<= i X)
     (<= X j)).

But if i is the symbol *, the first inequality is omitted. If j is the symbol *, the second inequality is omitted. If instead of being an integer, the second element of the type specification is a list containing an integer, (i), then the first inequality is made strict. An analogous remark holds for the (j) case. The rational and real type specifiers are similarly generalized.

Common Lisp supports a richer set of type specifiers than ACL2 supports.