Major Section: OTHER
The top-level ACL2 loop has a variable which controls which sense of
execution is provided. To turn ``guard checking on,'' by which we
mean that guards are checked at runtime, execute the top-level form
:set-guard-checking t. To turn it off, do :set-guard-checking nil.
The status of this variable is reflected in the prompt.
ACL2 !>means guard checking is on and
ACL2 >means guard checking is off. The exclamation mark can be thought of as ``barring'' certain computations. The absence of the mark suggests the absence of error messages or unbarred access to the logical axioms. Thus, for example
ACL2 !>(car 'abc)will signal an error, while
ACL2 >(car 'abc)will return
nil.
Whether guards are checked during evaluation is independent of the
default-defun-mode. We note this simply because it is easy to
confuse ``:program mode'' with ``evaluation in Common Lisp'' and
thus with ``guard checking on;'' and it is easy to confuse
``:logic mode'' with ``evaluation in the logic'' and with ``guard
checking off.'' But the default-defun-mode determines whether
newly submitted definitions introduce programs or add logical
axioms. That mode is independent of whether evaluation checks
guards or not. You can operate in :logic mode with runtime guard
checking on or off. Analogously, you can operate in :program
mode with runtime guard checking on or off.
However, one caveat is appropriate: functions introduced only as
programs have no logical definitions and hence when they are
evaluated their Common Lisp definitions must be used and thus their
guards (if any) checked. That is, if you are defining
functions in :program mode and evaluating expressions
containing only such functions, guard checking may as well be
on because guards are checked regardless. This same caveat
applies to a few ACL2 system functions that take state as an
argument. This list of functions includes all the keys of the alist
*super-defun-wart-table* and all function whose names are members
of the list *initial-untouchables*.