Specify what is printed when a guard is violated
This is an advanced feature that may require considerable
understanding of ACL2 programming.
ACL2 provides default error messages for guard violations. However, ACL2 also
provides a table,
Consider the following example.
(defun foo (x) (declare (xargs :mode :program :guard (consp x))) (car x)) (set-guard-msg foo (msg "An error for call ~x0." (cons 'foo args)))
Corresponding output for a guard violation is as follows.
ACL2 !>(foo 3) ACL2 Error in TOP-LEVEL: An error for call (FOO 3). ACL2 !>
Continuing in the same session, suppose we provide this fancier error message specification.
(set-guard-msg foo (msg "An error for call ~x0 in a world of length ~x1.~@2" (cons 'foo args) (length world) ; length of the current ACL2 world coda))
The corresponding error is shown below. Notice that the coda starts on a new line, with the same "See :DOC ..." message that one would see if the default error message were supplied for the same guard violation.
ACL2 !>(foo 3) ACL2 Error in TOP-LEVEL: An error for call (FOO 3) in a world of length 98582. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>
The capability shown above for function symbols is also available for macro
names. However, the variable,