Control checking guards during execution of top-level forms
Detailed comments about the arguments of this function may be found
elsewhere: see guard-evaluation-table. Here we provide an introduction
to the use of
New users are encouraged to execute one of the following forms in order to avoid evaluation errors due to guards:
(set-guard-checking :none) (set-guard-checking nil)
The former avoids all guard-checking on user-defined functions and should
generally work fine for new users, the only drawback being efficiency loss on
compute-intensive problems. All settings other than
You may put one of the above forms in the
Note that guards are not part of the ACL2 logic, and hence new users
can completely ignore the notion of guard (and the rest of this
documentation section after this paragraph!). For example,
(thm (equal (car 3) nil))
Moreover, unless your functions or top-level forms call built-in ACL2
functions that are defined in
(set-guard-checking :none)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.
See guard-evaluation-table for a succinct table, with associated discussion, that covers in detail the material presented in the rest of the present topic.
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
means guard checking is on and
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)
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 confuse
For further discussion on evaluation and guards see guards-and-evaluation, in particular the exception for safe-mode in the ``Aside'' there. See guard for a general discussion of guards.
Now we fulfill our promise above to discuss two other values for
: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
For technical reasons,
We conclude with a remark about the use of
ACL2 !>(defun foo (x) (declare (xargs :mode :program)) (car x)) Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) FOO ACL2 !>(foo 3) Error: Attempt to take the car of 3 which is not listp. [condition type: TYPE-ERROR] Restart actions (select using :continue): 0: Abort entirely from this (lisp) process. [Current process: Initial Lisp Listener]  ACL2(1): [RAW LISP] :pop ACL2 !>:set-guard-checking :none Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(foo 3) NIL ACL2 >:set-guard-checking :all Turning guard checking on, value :ALL. ACL2 !>(foo 3) ACL2 Error in TOP-LEVEL: The guard for the function symbol CAR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CAR 3). See :DOC trace for a useful debugging utility. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. ACL2 !>