GUARD-EVALUATION-TABLE

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.

Note: The default setting for guard-checking (that is, the initial value for (@ 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 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 :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))