print a form whose evaluation caused a guard violation
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 utility print-gv is provided for that purpose. (Alternatively, you may prefer to avoid guards entirely with (set-guard-checking :none); see set-guard-checking.)

Example Forms:
(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-tuple argument 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 foo and obtain a guard violation.
ACL2 !>(foo 3)

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 !>

We can obtain (in essence) the guard form that was false, as follows.
ACL2 !>(print-gv)


ACL2 !>

But which conjunct is to blame? With a bit of editing we can try each conjunct in turn.
ACL2 !>(LET ((X '3))
            (DECLARE (IGNORABLE X))
            (MY-FIRST-PREDICATE X))
ACL2 !>(LET ((X '3))
            (DECLARE (IGNORABLE X))
            (MY-SECOND-PREDICATE X))
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 printed by (print-gv). After a guard violation, just submit this form to raw Lisp:

(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.