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


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

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.