Major Section: GUARD
See set-guard-checking for an introduction to the topic discussed here. Also see guard for a general discussion of guards, and see guard-evaluation-examples-script for a script that illustrates combinations presented below.
The table below illustrates the interaction of the defun-mode with the
value supplied to
set-guard-checking. The first row considers
functions defined in
program mode; the other two consider
functions defined in
logic mode. The columns correspond to four
values of state global
'guard-checking-on, as supplied to
set-guard-checking. (A fifth value,
:nowarn, is similar to
but suppresses warnings encountered with
t (as explained in those warning
messages), and is not considered here.) During proofs,
'guard-checking-on is set to
nil regardless of how this variable has
been set in the top-level loop.
Below this table, we make some comments about its entries, ordered by row and
then by column. For example, when we refer to ``b2'' we are discussing the
execution of a
logic mode function whose guards have not been
verified, after having executed
guard-checking-on: (1)t (2):all (3):none (4)nil
(a) :program a1 a2 a3 a4 (b) guards not verified b1 b2 b3 b4 (c) guards verified c1 c2 c3 c4
a1. Check the guard upon entry, then use the raw Lisp code if the guard
checks (else cause an error). This is a common setting when one wants a
little guard checking but also wants the efficiency of raw Lisp. But note
that you can get raw Lisp errors. For example, if you make the definition
(defun foo (x) (car x)) in
program mode and execute
t, and then execute
(foo 3), you will
likely get an error from the call
(car 3) made in raw Lisp.
a2. For built-in (predefined) functions, see a1 instead. Otherwise:
Check the guard, without exception. Thus, we never run the raw Lisp code in this case. This can be useful when testing
functions, but you may want to run
t or at least
:exec in this case, so that the execution is done using
a3. For built-in (predefined) functions, see a4 instead. Otherwise:
Do not check the guard. For
program mode functions, we never
run the raw Lisp code in this case; so if you care about efficiency, see the
comment in a2 above about
comp. This combination is useful if you
are using ACL2 as a programming language and do not want to prove theorems
about your functions or suffer guard violations. In this case, you can
forget about any connection between ACL2 and Common Lisp.
a4. Run the raw Lisp code without checking guards at all. Thus, for
program mode functions, the
nil setting is often preferable to
:none setting because you get the efficiency of raw Lisp execution.
nil you can therefore get hard Lisp errors as in a1 above.
b1. Guards are checked at the top-level, though not at self-recursive calls. We never run the raw Lisp code in this case; guards would need to be verified first.
b2. Unlike the
t setting, guards are checked even on self-recursive
calls. But like the
t setting, we do not run the raw Lisp code. Use
this setting if you want guards checked on each recursive call in spite of
the cost of doing so.
b3, b4. Execution avoids the raw Lisp code and never checks guards. The
:none settings behave the same in this case (i.e., for
logic mode functions whose guards have not been verified).
c1, c2. Guards are checked. If the checks pass, evaluation takes place using
the raw Lisp code. If the checks fail, we get a guard violation. Either
way, we do not execute ``in the logic''; we only execute using the raw Lisp
code. Note that
:all behave the same in this case, (i.e. for
logic mode functions whose guards have been verified).
c3, c4. For the
functions whose guards have been verified will never cause guard violations.
nil, guards are still checked: if the check succeeds, then
evaluation is done using the raw Lisp code, and if not, it is done by the
``logic'' code, including self-recursive calls (though unlike the
we will not see a warning about this). But with
:none, no guard checking
is done, so the only time the raw Lisp code will be executed is when the
t (so that no evaluation is necessary). Thus, if you use
:none and you want a function
(foo x) with guard
(g x) to execute
using raw Lisp code, you can write a ``wrapper'' function with a guard of
(defun foo-wrap (x) (if (g x) (foo x) 'do-not-case))If you want the speed of executing raw Lisp code and you have non-trivial guards on functions that you want to call at the top-level, use