Major Section: EVENTS
Examples: (table tests 1 '(...)) ; set contents of tests to '(...) (table tests 25) ; get contents of tests (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 guardwhere
General Form: (table table-name key-term value-term op term)
table-nameis a symbol that is the name of a (possibly new) table,
value-term, if present, are arbitrary terms involving (at most) the single variable
op, if present, is one of the table operations below, and
term, if present, is a term.
Tablereturns an acl2 ``error triple.'' The effect of
opand how many arguments are presented. Some invocations actually have no effect on the ACL2 world and hence an invocation of
tableis not always an ``event''. We explain below, after giving some background information.
Important Note: The
table forms above are calls of a macro
that expand to involve the special variable
state. This will
prevent you from accessing a table from within a hint or theory where
where you do not have the
state variable. However, the form
(table-alist 'tests world)returns the alist representation of the table named
testin the given world. Often you have access to
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
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. By
convention, no table is important to ACL2's soundness, even though
some features of the system use tables, and the user is invited to
make free use of tables. Because tables are stored in the ACL2
world they are restored by
include-book and undone by
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
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. Each table has a ``name,'' which must be a symbol. Given
a table name, there are six operations one might perform on the
: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
: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.
When the operations above suggest that the table or its
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
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
: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 formevaluates the key- and value-terms, obtaining two objects that we call
value, checks that the
:guardon the named table and then ``modifies'' the named table so that the value associated with
value. When used like this,
tableis actually an event in the sense that it changes the ACL2 world. In general, the forms evaluated to obtain the
valuemay involve the variable
world, which is bound to the then-current world during the evaluation of the forms. However, in the special case that the table in question is named
valueterms may not contain any variables. Essentially, the keys and values used in events setting the
acl2-defaults-tablemust be explicitly given constants. See acl2-defaults-table.
(table name key-term nil :get) ; long form (table name key-term) ; short formevaluates the key-term (see note below), obtaining an object,
key, and returns the value associated with
keyin the named table (or,
nilif there is no value associated with
key). When used like this,
tableis not an event; the value is simply returned.
(table name nil nil :alist) ; long form (table name) ; short formreturns an alist representing the named table; for every key in the table with a non-
nilassociated value, the alist pairs the key and its value. The order in which the keys are presented is unspecified. When used like this,
tableis 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
:putmakes for each key and value of
val. When used like this,
tableis 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)Provided the named table is empty and has not yet been assigned a
term(which is not evaluated) is a term that mentions at most the variables
world, this event sets the
:guardof the named table to
term. Whenever a subsequent
termwill be evaluated with
keybound to the key argument of the
valbound to the
valargument of the
worldbound to the then current world. An error will be caused by the
:putif the result of the evaluation is
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
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
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
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
as a function, causing the table to contain a value that could not
:put there anymore. Observe that not all state-sensitive
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
:Put does a
getprop to the get the table
put-assoc-equal to record the new association, and a
putprop to store the new table alist -- plus the overhead associated
: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
: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
:pe name will never display a table event (for a
logical name other than
:pe name will display a
``normal'' event such as
(defun name ...) or
(defthm name ...) or
: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.
Similarly, we do not permit table names to have documentation
strings, since the same name might already have a documentation
string. If you want to associate a documentation string with a
table name that is being used no other way, define the name as a
label and use the
doc feature of
(see deflabel); also see defdoc.