PRINT-GV

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

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)

(LET ((X '3)) (DECLARE (IGNORABLE X)) (AND (MY-FIRST-PREDICATE X) (MY-SECOND-PREDICATE X)))

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