Major Section: GUARD
Below is a script that illustrates the combination of defun-modes --
:program mode, :logic mode without guards verified,
and :logic mode with guards verified -- with values from
set-guard-checking -- t (the default), :all, :none, and
nil. (It does not illustrate the value :nowarn, which is the same as
t except for inhibiting a warning.) The script also illustrates cases
where the guard is not, or is, t.
See guard-evaluation-examples-log for result of running this script. Before presenting the script below, we give some instructions in case you want to run it yourself.
See set-guard-checking for discussion of the interaction between defun-modes and guard-checking that is illustrated by this script. Also see guard-evaluation-table for a succinct table, with associated discussion, that covers in detail the interactions illustrated here.
The script mentions the running of ``Tracing Code''. The code is the following sequence of commands.
(trace$ fact) :set-guard-checking t (fact 2) (fact t) :set-guard-checking :all (fact 2) (fact t) :set-guard-checking :none (fact 2) (fact t) :set-guard-checking nil (fact 2) (fact t)
If you want to run the script yourself, you may find it handy to use the following Emacs keyboard macro for running the tracing code in 2-window mode, with the cursor in the window with the script and ACL2 running in the other window.
(fset 'step-guard-script
[?C-a ?C- ?C-e ?M-w ?C-a ?C-n
?C-x ?o ?M-> ?C-y return ?C-x ?o])
; Put it on a key (if you have defined the indicated keymap by using
; emacs/emacs-acl2.el):
(define-key ctl-t-keymap "r" 'step-guard-script)
The script follows.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Program mode
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun fact (x)
(declare (xargs :guard (integerp x)
:mode :program))
(if (posp x)
(* x (fact (1- x)))
1))
; Run the Tracing Code here. It shows execution in raw Lisp in the t and nil
; cases of :set-guard-checking, but not in the :all or :none cases. We get a
; guard violation for argument t in the case :set-guard-checking t.
:u
(defun fact (x)
(declare (xargs :guard t
:mode :program))
(if (posp x)
(* x (fact (1- x)))
1))
; Run the Tracing Code here. It should give the same results as above,
; except that we no longer get a guard violation in the case
; :set-guard-checking t.
:u
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Logic mode, guard other than t
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun fact (x)
(declare (xargs :guard (integerp x)
:verify-guards nil
:mode :logic))
(if (posp x)
(* x (fact (1- x)))
1))
; Run the Tracing Code here. It should give guard violations for (fact t)
; with guard-checking set to t or :all. It should never run in raw Lisp,
; because we have not verified guards. In the t case, we can get a warning
; about avoiding the guard check on recursive calls, but only if we do not
; trace the function, fact.
(verify-guards fact)
; Run the Tracing Code here. The results should be as described just above,
; except that now we go into raw Lisp for (fact 2) with guard-checking other
; than :none.
:u
:u
; The following definition is the same as above, except that guards are
; verified.
(defun fact (x)
(declare (xargs :guard (integerp x)
:mode :logic))
(if (posp x)
(* x (fact (1- x)))
1))
; Run the Tracing Code here. We should get the same traces as in the
; immediately preceding case, since guards had been verified in both cases.
:u
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Logic mode, guard t
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun fact (x)
(declare (xargs :guard t
:verify-guards nil
:mode :logic))
(if (posp x)
(* x (fact (1- x)))
1))
; Run the Tracing Code here. We should never go in to raw Lisp, because
; guards have not been verified. We will see the same traces for (fact 2) as
; with the (integerp x) guard above with :verify-guards nil specified, except
; that even without tracing, there is no warning for :set-guard-checking t
; about recursive calls. And, there are no guard violations for (fact t), of
; course, since posp (necessarily, if we are to verify guards) has a guard of
; t.
(verify-guards fact)
; Run the Tracing Code here. You shouldn't see any surprises. Note however
; that if we back up to the start (using :u :u) and then define fact as just
; above but without :verify-guards nil, then the :none setting will allow us
; to go into raw Lisp: although :none generally avoids execution of raw Lisp
; counterparts, it allows this when the guard is T and guards have been
; verified.
