		Search-engine friendly clone of the ACL2 documentation.

Set-guard-msg

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, guard-msg-table, that allows custom error messages for guard-checking failures. The macro set-guard-msg provides a convenient way to update this table. The keys of the table are symbols, which can be expected to be function symbols or names of macros. Each value is a (translated) term whose only free variables are world, args, and coda. When guard-checking fails, the term is evaluated to create a message suitable for "~@" formatted printing directives; see fmt. That evaluation is done with world bound to the current ACL2 logical world, with args bound to the actual parameters of the call, and with coda bound to the message that would typically be printed by default at the end of a guard violation. (See ACL2 source function guard-er-message-coda for details, or simply experiment.)

Example

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, coda, should not be used for macro names.