The
Special form for execution efficiency or run-time type checks
THE is a Common Lisp special form. It is usually used as a
way to boost performance 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. When
evaluating code directly in the top-level loop or in :logic-mode
functions that have not been guard-verified, THE can perform
run-type type 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.
A term of the form (the double-float <term>) will assist ACL2's syntax
checking by telling ACL2 that <term> returns a df. See df for
relevant background.
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.
