|
|
|---|
|
|
|
|---|
Introduction to guards in ACL2
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
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
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 function'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 function that generally performs, we expect, nearly as well as submitted function; see evaluation for relevant background on these two functions. 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.