Major Section: GUARD
Most users can probably profit by avoiding dealing with guards most
of the time. If they seem to get in the way, they can be ``turned
off'' using the command :set-guard-checking nil; for more
about this, see set-guard-checking. For more about guards in
general, see guard.
The guard on a function symbol is a formula about the formals of the
function. To see the guard on a function, use the keyword command
:args. See args. To specify the guard on a function at
defun-time, use the :guard xarg. See xargs.
Guards can be seen as having either of two roles: (a) they are a specification device allowing you to characterize the kinds of inputs a function ``should'' have, or (b) they are an efficiency device allowing logically defined functions to be executed directly in Common Lisp. Briefly: If the guards of a function definition are ``verified'' (see verify-guards), then the evaluation of a call of that function on arguments satisfying its guard will have the following property:
All subsequent function calls during that evaluation will be on arguments satisfying the guard of the called function.The consequence of this fact for (a) is that your specification function is well-formed, in the sense that the values returned by this function on appropriate arguments only depend on the restrictions of the called functions to their intended domains. The consequence of this fact for (b) is that in the ACL2 system, when a function whose guards have been verified is called on arguments that satisfy its guard, then the raw lisp function defined by this functions's
defun event is used to evaluate the call. Note
however that even when the user-supplied defun is not used, ACL2
uses a corresponding ``executable counterpart'' that generally
performs, we expect, nearly as well as the raw lisp function.
See comp to see how compilation can speed up both kinds of
execution.
Let us turn next to the issue of the relationship between guards and
evaluation. See guards-and-evaluation.