Table
User-managed tables
Examples:
(table tests 1 '(...)) ; set contents of tests[1] to '(...)
(table tests 25) ; get contents of tests[25]
(table tests) ; return table tests as an alist
(table tests nil nil :clear) ; clear table tests
(table tests nil '((foo . 7)) :clear) ; set table tests to ((foo . 7))
(table tests nil nil :guard) ; fetch the table guard
(table tests nil nil :guard term) ; set the table guard
General Form:
(table table-name key-term value-term op term)
where table-name is a symbol that is the name of a (possibly new)
table; key-term and value-term, if present, are arbitrary terms
involving (at most) the variables WORLD and ENS; op, if
present, is one of the table operations below; and term, if present, is a
term. Table returns an ACL2 error-triple. The effect of
table on state depends on op and how many arguments are
presented. Some invocations actually have no effect on the ACL2 world
and hence an invocation of table is not always an ``event''. We explain
below, after giving some background information.
Important Note: The table forms above are calls of a macro that
expands to involve the special variable state. This will prevent you
from accessing a table from within a hint or theory where you do not have the
state variable. However, the form
(table-alist 'tests world)
returns the alist representation of the table named tests in the given
world. Often you can provide a suitable expression for world,
for example, (w state).
The ACL2 system provides ``tables'' by which the user can associate one
object with another. Tables are in essence just conventional association
lists — lists of pairs — but the ACL2 environment provides a means
of storing these lists in the ``ACL2 world'' of the current state.
The ACL2 user could accomplish the same ends by using ACL2 ``global
variables''; however, limitations on global variable names are imposed to
ensure ACL2's soundness. Some features of the system use tables, and the user
is invited to make free use of tables. By convention, no user-defined table
is important to ACL2's soundness. Because tables are stored in the ACL2 world they are restored by include-book and undone by :ubt. Many users of Nqthm requested a facility by which user data could be
saved in Nqthm ``lib files'' and tables are ACL2's answer to that request.
Abstractly, each table is an association list mapping ``keys'' to
``values.'' In addition, each table has a ``:guard,'' which is a term
that must be true of any key and value used. By setting the :guard on a
table you may enforce an invariant on the objects in the table, e.g., that all
keys are positive integers and all values are symbols. Note that attachments
are allowed when evaluating a table guard (see defattach). Each table
has a ``name,'' which must be a symbol. Given a table name, the following
operations can be performed on the table.
:put — associate a value with a key (possibly changing the value
currently associated with that key).
:get — retrieve the value associated with a key (or nil if no
value has been associated with that key).
:alist — return an alist showing all keys and non-nil values in
the table.
:clear — clear the table (so that every value is nil), or if val
is supplied then set table to that value (which must be an alist).
:guard — fetch or set the :guard of the table. See set-table-guard for a convenient way to set a table's :guard to produce
user-friendly error messages.
When the operations above suggest that the table or its :guard are
modified, what is actually meant is that the current state is redefined
so that in it, the affected table name has the appropriate properties. In
such cases, the table form is an event (see events). In the
:put case, if the key is already in the table and associated with the
proposed value, then the table event is redundant (see redundant-events).
Table forms are commonly typed by the user while interacting with the
system. :Put and :get forms are especially common. Therefore, we
have adopted a positional syntax that is intended to be convenient for most
applications. Essentially, some operations admit a ``short form'' of
invocation.
(table name key-term value-term :put) ; long form
(table name key-term value-term) ; short form
evaluates the key- and value-terms, obtaining two objects that we call
key and value, checks that the key and value satisfy the
:guard on the named table and then ``modifies'' the named table so that
the value associated with key is value. When used like this,
table is actually an event in the sense that it changes the ACL2 world. In general, the forms that are evaluated to obtain the key and
value may involve two variables: WORLD, which is bound to the
then-current world; and ENS, which is bound to the enabled
structure representing the current theory. (The enabled structure is passed
as a formal parameter to many built-in functions; for example, see system-utilities for a description of built-in utilities enabled-numep
and enabled-runep.) However, in the special case that the table in
question is named ACL2-defaults-table, the key and value
terms may not contain any variables. Essentially, the keys and values used in
events setting the ACL2-defaults-table must be explicitly given
constants. See ACL2-defaults-table.
(table name key-term nil :get) ; long form
(table name key-term) ; short form
evaluates the key-term (see note below), obtaining an object, key, and
returns the value associated with key in the named table (or, nil if
there is no value associated with key). When used like this, table
is not an event; the value is simply returned.
(table name nil nil :alist) ; long form
(table name) ; short form
returns an alist representing the named table; for every key in the table
with a non-nil associated value, the alist pairs the key and its value.
The order in which the keys are presented is unspecified. When used like
this, table is not an event; the alist is simply returned.
(table name nil val :clear)
sets the named table to the alist val, making the checks that
:put makes for each key and value of val. When used like this,
table is an event because it changes the ACL2 world.
(table name nil nil :guard)
returns the translated form of the guard of the named table.
(table name nil nil :guard term)
This event sets the :guard of the named table to term, provided
the following requirements are met. The named table must be empty and it must
not have been assigned a :guard yet. Term (which is not evaluated)
should be a term that mentions at most the variables KEY, VAL,
WORLD, ENS, and STATE. In the common case term will
evaluate to a single value, but it can return two values as discussed later
below; either way, it must not return STATE.
Whenever a subsequent :put occurs, term will be evaluated with
KEY bound to the key argument of the :put, VAL bound to the
val argument of the :put, WORLD bound to the then current world, ENS bound to the enabled structure representing the current
theory, and STATE bound to the ACL2 state. The term is evaluated.
An error will be caused by the :put if the result of the evaluation is
nil when a single value is returned; what if two values are returned?
If the term returns multiple values (mv okp msg), then an error will
be caused if okp is nil. In that case, if msg is also nil
then a generic error message is printed about the illegal key/value pair, just
as in the single-value return case. Otherwise msg should be a msgp — a string or a cons suitable for printing with the fmt
directive, ~@. In that case, msg is printed (using fmt
~@) instead of the generic error message. Here is a simple example
adapted from former code in the ACL2 sources.
(defun my-table-guard (fn val wrld)
(let ((msg0 ; nil if fn/val is OK as a key/value pair, else a msg
(my-table-guard-msg fn val wrld)))
(cond
(msg0 (mv nil
(msg
"Illegal my-table key and value (see :DOC ~
memoize-partial):~|key = ~y0value = ~y1Reason:~%~@2~|~%"
fn val msg0)))
(t (mv t nil)))))
(table my-table nil nil
:guard
(my-table-guard key val world))
Note that it is not allowed to change the :guard on a table once it
has been explicitly set. Before the :guard is explicitly set, it is
effectively just t. After it is set it can be changed only by undoing
the event that set it. The purpose of this restriction is to prevent the user
from changing the :guards on tables provided by other people or the
system.
The intuition behind the :guard mechanism on tables is to enforce
invariants on the keys and values in a table, so that the values, say, can be
used without run-time checking. But if the :guard of a table is
sensitive to the ACL2 world, it may be possible to cause some value in
the table to cease satisfying the :guard without doing any operations on
the table. Consider for example the :guard ``no value in this table is
the name of an event.'' As described, that is enforced each time a value is
stored. Thus, 'bang can be :put in the table provided there is no
event named bang. But once it is in the table, there is nothing to
prevent the user from defining bang as a function, causing the table to
contain a value that could not be :put there anymore. Observe that not
all state-sensitive :guards suffer this problem. The :guard ``every
value is an event name'' remains invariant, courtesy of the fact that undoing
back through an event name in the table would necessarily undo the :put
of the name into the table.
Table was designed primarily for convenient top-level use. Tables are
not especially efficient. Each table is represented by an alist stored on the
property list of the table name. :Get is just a getprop and assoc-equal. :Put does a getprop to the get the table alist, a
put-assoc-equal to record the new association, and a putprop to
store the new table alist — plus the overhead associated with
:guards and undoable events, and checking (for redundancy) if the
key is already bound to its proposed value. Note that there are never
duplicate keys in the resulting alist; in particular, when the operation
:clear is used to install new alist, duplicate keys are removed from
that alist.
A table name may be any symbol whatsoever. Symbols already in use as
function or theorem names, for example, may be used as table names. Symbols
in use only as table names may be defined with defun, etc. Because
there are no restrictions on the user's choice of table names, table names are
not included among the logical names. Thus, :pe name will never display
a table event (for a logical name other than :here). Either :pe
name will display a ``normal'' event such as (defun name ...) or
(defthm name ...) or else :pe name will cause an error indicating
that name is not a logical name. This happens even if name is in
use as a table name.
Subtopics
- ACL2-defaults-table
- A table specifying certain defaults, e.g., the default defun-mode
- Set-table-guard
- Set the :guard for a table
- Using-tables-efficiently
- Notes on how to use tables efficiently
