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.

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).

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, 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, no guard checking is done, so the only time the raw Lisp code will be executed is when the guard is 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 t:

(defun foo-wrap (x)
  (if (g x)
      (foo x)
    'do-not-case))