Set-table-guard
Set the :guard for a table
This macro is a convenient interface for setting a table's
guard to produce user-friendly error messages when the guard fails. See table for background on table guards. As noted there, the table guard may
reference variables KEY, VAL, WORLD, ENS, and STATE;
that is the case for the guard and coda mentioned below. Also
particularly relevant here is the fact that the table guard can return a
single value, but it can also return (mv flg msg); in the latter case, if
flg is nil then msg is an error message. Set-table-guard
is supplied a guard term that returns a single value, but sets the table guard
to a corresponding term that returns values (mv flg msg), where msg
is constructed to be user-friendly when it is non-nil.
General Form:
(set-table-guard name guard
:topic topic
:show show
:coda coda)
where name is the name of a table, guard is a term returning a
single value that specifies the guard of that table, and the optional keyword
arguments are as follows.
- :Topic defaults to name. Otherwise it is the name of a documentation topic to which the user is directed when the table guard
fails.
- :Show is nil by default, in which case the guard term is not
included in the error message; otherwise it is included.
- :Coda is nil by default. Otherwise it should be a message (see
msgp) to be printed, preceded by two spaces, after the message that
would otherwise be printed.
The error message when keywords are omitted is as shown in the example
below, but (of course) where FOO, MY-KEY, and MY-VAL are
replaced respectively by the table name, the key, and the value. We start our
example by evaluating the following two events.
(defun foo-check (key val world)
(declare (ignore val))
(function-symbolp key world))
(set-table-guard foo (foo-check key val world))
Then evaluation of (table foo 'my-key 'my-val) produces the following
error message.
ACL2 Error in ( TABLE FOO ...): The TABLE :guard for FOO disallows
the combination of key MY-KEY and value MY-VAL. See :DOC FOO.
Here we show what happens to the error message if instead we set the table
guard as follows. As before, it should be clear from this example what the
message would look like in general. This time we evaluate:
(set-table-guard foo (foo-check key val world)
:topic set-foo
:show t
:coda (and (eq val 'my-val)
(msg "~x0 is an odd name for a value!"
val)))
This time, evaluation of (table foo 'my-key 'my-val) produces an error
message that references :DOC topic
SET-FOO instead of FOO (because of the :topic argument), shows
the table guard (because of the :show argument), and prints a final coda
(because of the :coda argument).
ACL2 Error in ( TABLE FOO ...): The TABLE :guard for FOO disallows
the combination of key MY-KEY and value MY-VAL. The :guard requires
(FOO-CHECK KEY VAL WORLD). See :DOC SET-FOO. MY-VAL is an odd name
for a value!
It can be helpful for the table guard to be well-guarded. For the examples
above, the error message from (table foo 3 'my-val) is ugly because
3 fails to satisfy the guard of function-symbolp, which is called by
foo-check. Here is a version of that function that produces the desired
error message.
(defun foo-check (key val world)
(declare (xargs :guard t)
(ignore val))
(and (symbolp key) ; for guard of function-symbolp
(plist-worldp world) ; for guard of function-symbolp
(function-symbolp key world)))
Finally, here are two examples from the ACL2 source code. They illustrate
that :show t is reasonable when the table guard is concise, and that
:topic is necessary when the table name is undocumented.
(set-table-guard invisible-fns-table
(invisible-fns-entryp key val world)
:show t)
(set-table-guard inhibit-warnings-table
(stringp key)
:topic set-inhibit-warnings)
