The
The is a special form that can be used to optimize the execution
efficiency of guard-verified ACL2 definitions, or (less frequently) to
carry out a low-level run-time type checks. (Advanced)
The is a special Common Lisp form. It is usually used as a
way to boost the performance of ACL2 definitions by telling the Common Lisp
compiler that a certain expression will always produce a result of a certain
type. This information may allow the Common Lisp compiler to avoid certain
run-time checks. See declare and type-spec for general, related
background.
General form:
(the <typ> <val>) ;; returns <val>, or causes a run-time error
- <typ> is a type-spec
- <val> is some expression that should produce a value of that type.
Typical example:
(defun merge-bytes (b1 b2)
;; Combine two 8-bit bytes into a 16-bit result.
(declare (type (unsigned-byte-p 8) b1 b2))
(the (unsigned-byte 16)
(logior (the (unsigned-byte 16) (ash b1 8))
b2)))
On most Lisp implementations 16-bit numbers are fixnums. The the
forms above are promises to the Lisp compiler that these ash and
logior operations will always produce 16-bit numbers. Ideally, the
compiler could use this information to generate more efficient code, i.e., by
omitting whatever code is normally required to handle bignum results. (Of
course, a sufficiently smart compiler could have figured this out on its own;
in practice Lisp compilers vary in their reasoning abilities.)
Relation to Guards
To justify that type declarations are correct, the is integrated into
ACL2's guard mechanism. A call of (the TYPE EXPR) in the body of
a function definition generates a guard proof obligation that the type,
TYPE, holds for the value of the expression, EXPR. Consider the
following example.
(defun f (x)
(declare (xargs :guard (p1 x)))
(if (p2 x)
(the integer (h x))
17))
The guard proof obligation generated for the THE expression
above is as follows.
(implies (and (p1 x) (p2 x))
(let ((var (h x))) (integerp var)))
For the to provide any execution speed benefit, guards must be
verified.
In contexts where guards have not been verified, the acts as a
low-level, run-time type check that val satisfies the type specification
typ (see type-spec). An error is caused if the check fails;
otherwise, val is returned. Here are some examples:
(the integer 3) ; returns 3
(the (integer 0 6) 3) ; returns 3
(the (integer 0 6) 7) ; causes an error (see below for exception)
There is an exception to the rule that failure of the type-check causes an
error: there is no error when guard-checking has been turned off, that
is, in any of the following ways; also set-guard-checking and see with-guard-checking.
Further resources
The b* macro provides a special syntax that may make using the
forms more pleasant; see patbind-the for more information.
When optimizing functions with type declarations, you may wish to manually
inspect the compiler's output with disassemble$ or conduct experiments
to measure the impact of your optimizations.
THE is defined in Common Lisp. See any Common Lisp documentation for
more information.
Subtopics
- Type-spec
- Type specifiers can be used in Common Lisp type declarations and
the forms, and may result in improved efficiency of execution.
- Patbind-the
- b* type declaration operator.
