Declare
Extra declarations that can occur in function definitions, let
bindings, and so forth.
Common Lisp provides a declaration mechanism that allows the
programmer to explain additional information to the compiler. For
instance:
- The programmer might declare that some variable always has some particular
type. The compiler might then, depending on its optimization/safety settings,
either add run-time checks to ensure that this really is true, or optimize the
compiled code by assuming the variable has the correct type.
- The programmer might declare that some variable is ignored. The
compiler might then, instead of warning the programmer that the variable is
never used, explicitly check to make sure that it really is never used.
ACL2 supports the above kinds of declarations, and also adds its own kinds
of declarations for specifying things like the guards and measures of functions, as described in xargs.
There are also other kinds of Common Lisp declarations that ACL2 does not
support, e.g., pertaining to inlining, safety settings, variable lifetime, and
so forth.
Usage
Examples:
(declare (ignore x y z))
(declare (ignorable x y z)
(irrelevant w) ; for DEFUN only
(type integer i j k)
(type (satisfies integerp) m1 m2))
(declare (xargs :guard (and (integerp i)
(<= 0 i))
:guard-hints (("Goal" :use (:instance lemma3
(x (+ i j)))))))
General Form:
(declare d1 ... dn)
where, in ACL2, each di is of one of the following forms:
- (ignore v1 ... vn)
- where each vi is a variable introduced in the immediately superior
lexical environment. These variables must not occur free in the scope of the
declaration. This declaration can be useful for inhibiting compiler warnings;
see also set-ignore-ok.
- (ignorable v1 ... vn)
- where each vi is a variable introduced in the immediately superior
lexical environment. These variables need not occur free in the scope of the
declaration. This declaration can be useful for inhibiting compiler warnings;
see also set-ignore-ok.
- (irrelevant v1 ... vn)
- where each vi is a formal parameter declared at the top level of a
surrounding defun form, as shown below. See irrelevant-formals
for more information.
- (type type-spec v1 ... vn)
- where each vi is a variable introduced in the immediately superior
lexical environment and type-spec is a type specifier (as described in
the documentation for type-spec). This declaration can be useful for
optimizing Common Lisp execution speed. See also the.
- (xargs :key1 val1 ... :keyn valn)
- where the legal values of the keys and values are described in the
documentation for xargs. These declarations are only allowed at the
top level of definitions (defun and defmacro, as shown below),
and convey information such as the guard and measure for a
function.
- (optimize ...)
- for example, (optimize (safety 3)). This is allowed only at the top
level of defun forms and is probably only rarely of any interest. See
any Common Lisp documentation for more information.
Declarations in ACL2 may occur only where dcl occurs in the following
display (not including lambda objects, discussed later below):
- (DEFUN name args doc-string dcl ... dcl body)
- (DEFMACRO name args doc-string dcl ... dcl body)
- (LET ((v1 t1) ...) dcl ... dcl body)
- (MV-LET (v1 ...) term dcl ... dcl body)
- (FLET ((name args dcl ... dcl body) ...))
- (MACROLET ((name args dcl ... dcl body) ...))
Each of the cases above permits certain declarations, as follows.
- DEFUN: (ignore ignorable
irrelevant type optimize xargs)
- DEFMACRO: (ignore ignorable type xargs)
- LET: (ignore ignorable type)
- MV-LET: (ignore ignorable type)
- FLET: (ignore ignorable type)
- MACROLET: (ignore ignorable type)
Of course, declarations are permitted in macro calls to the extent that
they are permitted in the macroexpansions. For example, declare forms
generated by calls of let* and case-match may wind up in
corresponding let forms in the macroexpansions, where they would be
subject to the restrictions on declare forms for let shown just
above.
Also see lambda for discussion of lambda objects and their legal
declare forms.
Declare is defined in Common Lisp. See any Common Lisp documentation
for more information.
Subtopics
- Xargs
- Extra arguments, for example to give hints to defun
- Type-spec
- Type specifiers can be used in Common Lisp type declarations and
the forms, and may result in improved efficiency of execution.
- Declare-stobjs
- Declaring a formal parameter name to be a single-threaded object
- Set-ignore-ok
- Allow unused formals and locals without an ignore or
ignorable declaration
- Set-irrelevant-formals-ok
- Allow irrelevant formals in definitions
