Guard-evaluation-table
A table that shows combinations of defun-modes and guard-checking
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.
Note: The default setting for guard-checking (that is, the initial value
for state global (@ guard-checking-on)) is T.
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 t but
suppresses warnings; a remark with details for system hackers is at the end of
this topic.) Note that 'guard-checking-on is set to nil during
proofs but is set to t during certify-book, and include-book, regardless of how this variable has been set in the top-level
loop (see the ``Essay on Guard Checking'' in source file
other-events.lisp if you are interested in a rationale).
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 :set-guard-checking
:all.
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
:set-guard-checking 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 :program mode
functions, but you may want to run :comp t or at least
:comp :exec in this case, so that the execution is done
using compiled code.
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 the :none setting because you get the efficiency of raw Lisp
execution. However, with 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
nil and :none settings behave the same in this case (i.e., for
:logic mode functions whose guards have not been verified),
except that recursive calls are never inlined for :none and tracing (see
trace) will show recursive calls for :none but not for
nil.
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 t and :all behave the same in this case,
(i.e. for :logic mode functions whose guards have been
verified).
c3, c4. For the :none and nil settings, :logic mode
functions whose guards have been verified will never cause guard violations.
However, with nil and for built-in functions in :logic mode, 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 t case, we will not see a warning
about this). But with :none for user-defined functions, no guard
checking is done, and the only time the raw Lisp code will be executed is when
the guard is t and guards are verified at the time the
executable-counterpart of the function is defined (i.e., when the function is
admitted unless it is later defined again and compiled using :comp). 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 t:
(defun foo-wrap (x)
(declare (xargs :guard t))
(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 nil
rather than :none.
Remark for system hackers. As noted above, a fifth value, :nowarn, is
similar to t but suppresses warnings. Only the four values in the column
headers above and :nowarn are legal for set-guard-checking,
with-guard-checking, with-guard-checking-error-triple, and
with-guard-checking-event. Behavior is technically undefined if you
set state global guard-checking-on directly to other than those
five values, say using assign, f-put-global, or state-global-let*. However, as of this writing (in August 2021), such a
value will cause the same behavior as value :nowarn. End of
Remark.
