SET-GUARD-CHECKING

control checking guards during execution of top-level forms 
Major Section:  OTHER

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 :set-guard-checking nil. 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 nil.

We will return at the end of this documentation topic to discuss two other values for :set-guard-checking.

Whether guards are checked during evaluation is independent of the default-defun-mode. We note this simply because it is easy to confuse ``: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 :program 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 functions in :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 *initial-untouchables*.

See guard for a general discussion of guards.

Finally, we fulfill our promise above to discuss two other values for :set-guard-checking: 

:set-guard-checking :nowarn
:set-guard-checking :all
The 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)))))


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 !>
If you think about evaluation of (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 a is 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 :nowarn and :all for :set-guard-checking have been introduced as ways of dealing with the above warning. The value :nowarn simply turns off the warning above. The value :all causes all guards to be checked, even on recursive calls -- 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-checking is invoked with values t, :nowarn, and :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 source function add-trip.''