Major Section: OTHER
New users are encouraged to execute the following form in order to avoid evaluation errors due to guards:
(set-guard-checking nil)Alternatively, put the above form in the
"acl2-customization.lisp"file in your current directory (see cbd) or your home directory; see acl2-customization.
Note that guards are not part of the ACL2 logic, and hence new users can
completely ignore the notion of guard (including the rest of this
documentation section!). For example,
(car 3) and
nil can be proved
equal in the ACL2 logic, as follows, even though the guard on
requires its first argument to be a
cons pair or
(thm (equal (car 3) nil))However, the evaluation of
(car 3)will cause a guard violation unless
set-guard-checkinghas been invoked.
Here we are assuming that you define your functions in
the default. See guards-and-evaluation, speficially the discussion ``Guards
and evaluation IV: functions having :program mode'', if you use
program mode. But with that caveat we can summmarize as follows.
(set-guard-checking nil)will allow evaluation of forms such as
(car 3)to take place without error in the top level loop, not only when proving theorems.
If you feel bold, then you may wish to read the rest of this documentation topic; also see guard.
The top-level ACL2 loop has a variable which controls which sense of
execution is provided. To turn ``guard checking on,'' by which we
mean that guards are checked at runtime, execute the top-level form
:set-guard-checking t. To turn it off, do
The status of this variable is reflected in the prompt.
ACL2 !>means guard checking is on and
ACL2 >means guard checking is off. The exclamation mark can be thought of as ``barring'' certain computations. The absence of the mark suggests the absence of error messages or unbarred access to the logical axioms. Thus, for example
ACL2 !>(car 'abc)will signal an error, while
ACL2 >(car 'abc)will return
We will return at the end of this documentation topic to discuss two other
Whether guards are checked during evaluation is independent of the
default-defun-mode. We note this simply because it is easy to
program mode'' with ``evaluation in Common Lisp'' and
thus with ``guard checking on;'' and it is easy to confuse
logic mode'' with ``evaluation in the logic'' and with ``guard
checking off.'' But the
default-defun-mode determines whether
newly submitted definitions introduce programs or add logical
axioms. That mode is independent of whether evaluation checks
guards or not. You can operate in
logic mode with runtime guard
checking on or off. Analogously, you can operate in
mode with runtime guard checking on or off.
However, one caveat is appropriate: functions introduced only as
programs have no logical definitions and hence when they are
evaluated their Common Lisp definitions must be used and thus their
guards (if any) checked. That is, if you are defining
program mode and evaluating expressions
containing only such functions, guard checking may as well be
on because guards are checked regardless. This same caveat
applies to a few ACL2 system functions that take
state as an
argument. This list of functions includes all the keys of the alist
*super-defun-wart-table* and all function whose names are members
of the list
See guard for a general discussion of guards.
Finally, we fulfill our promise above to discuss two other values for
:set-guard-checking :nowarn :set-guard-checking :allThe meaning of these values is perhaps best described by the following example provided by David Rager.
ACL2 !>(defun my-test (expr) (declare (xargs :guard (true-listp expr) :verify-guards nil)) (if (atom expr) expr (cons (my-test (car expr)) (my-test (cdr expr)))))If you think about evaluation of
The admission of MY-TEST is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT EXPR). We could deduce no constraints on the type of MY- TEST. However, in normalizing the definition we used primitive type reasoning.
Summary Form: ( DEFUN MY-TEST ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) MY-TEST ACL2 !>(my-test '(a b c))
ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited on recursive calls of the executable counterpart (i.e., in the ACL2 logic) of MY-TEST. To check guards on all recursive calls: (set-guard-checking :all) To leave behavior unchanged except for inhibiting this message: (set-guard-checking :nowarn)
(A B C) ACL2 !>
(my-test '(a b c)), you will see that it leads to the recursive call
(my-test 'a), which one might expect to cause a guard violation since the symbol
ais not a
true-listp. However, as the warning above explains, we do not by default check guards on recursive calls. The reason is efficiency -- imagine a simple definition with a guard that is slow to evaluate. The values
:set-guard-checkinghave been introduced as ways of dealing with the above warning. The value
:nowarnsimply turns off the warning above. The value
:allcauses all guards to be checked, even on recursive calls and even on all calls of non-built-in
programmode functions -- unless, of course, a call is made of a function whose guard has been verified (see verify-guards), in which case the corresponding call is made in raw Lisp without subsidiary guard-checking. We still say that ``guard-checking is on'' after
:set-guard-checkingis invoked with values
:all, otherwise (after value
nil) we say ``guard-checking is off.
For technical reasons,
:all does not have its advertised effect in the
case of built-in
program-mode functions. If you are interested in
this technical detail, see the comment ``In the boot-strap world...'' in