Major Section: OTHER
By default, ACL2 checks input constraints on functions, known as
guards. When guards are violated, an informative message is printed;
but sometimes it is useful to investigate why the guard check fails. The
print-gv is provided for that purpose. (Alternatively, you may
prefer to avoid guards entirely with
Example Forms: (print-gv) (print-gv :evisc-tuple (evisc-tuple 4 4 nil nil)) (print-gv :evisc-tuple (evisc-tuple 4 ; print-level 5 ; print-length (world-evisceration-alist state nil) nil ; hiding-cars ))
General Form: (print-gv :evisc-tuple x)where the
:evisc-tupleargument is optional and defaults to one that hides only the ACL2 logical world, by printing
<world>instead of a very large structure. See evisc-tuple for a discussion of evisc-tuples.
To see how one might use
print-gv, consider the following definition.
(defun foo (x) (declare (xargs :guard (and (my-first-predicate x) (my-second-predicate x)))) (cdr x))Now suppose we evaluate a call of
fooand obtain a guard violation.
ACL2 !>(foo 3)We can obtain (in essence) the guard form that was false, as follows.
ACL2 Error in TOP-LEVEL: The guard for the function call (FOO X), which is (AND (MY-FIRST-PREDICATE X) (MY-SECOND-PREDICATE X)), is violated by the arguments in the call (FOO 3). To debug: See :DOC print-gv, see :DOC trace, and see :DOC wet. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users.
ACL2 !>(print-gv)But which conjunct is to blame? With a bit of editing we can try each conjunct in turn.
(LET ((X '3)) (DECLARE (IGNORABLE X)) (AND (MY-FIRST-PREDICATE X) (MY-SECOND-PREDICATE X)))
ACL2 !>(LET ((X '3)) (DECLARE (IGNORABLE X)) (MY-FIRST-PREDICATE X)) T ACL2 !>(LET ((X '3)) (DECLARE (IGNORABLE X)) (MY-SECOND-PREDICATE X)) NIL ACL2 !>Aha! Now we can investigate why the second predicate fails for 3.
Finally, we mention a hack that will give you access in raw Lisp to the form
(print-gv). After a guard violation, just submit this form to
(print-gv1 (cdr (assoc 'ev-fncall-guard-er-wormhole *wormhole-outputs*)) (w state))
And even more finally, we note that while
print-gv is a utility for
debugging guard violations, in contrast, see guard-debug for a utility to
assist in debugging failed proofs arising from guard verification.