Major Section: EVENTS
Examples: (set-measure-function nqthm::count)Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
General Form: (set-measure-function name)where
nameis a function symbol of one argument. This macro is equivalent to
(table acl2-defaults-table :measure-function 'name), which is also an event (see table), but no output results from a
This event sets the default measure function to
if a recursively defined function is submitted to
defun with no
defun ``guesses'' the measure
(name var), where
name is the then current default measure function
var is the first formal found to be tested along every branch
and changed in every recursive call.
Major Section: EVENTS
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
Because the variable symbol
STATE denotes the ``current ACL2
state,'' ACL2 treats the symbol very restrictively when it occurs as
a formal parameter of a defined function. The novice user, who is
unlikely to be aware of the special status of that symbol, is
likely to be confused when error messages about
STATE are printed
in response to the innocent choice of that symbol as a formal
variable. Therefore the top-level ACL2 loop can operate in a mode
STATE is simply disallowed as a formal parameter.
For a discussion of
STATE, See state. Roughly speaking, at
the top-level, the ``current ACL2 state'' is denoted by the variable
STATE. Only the current state may be passed into a
function expecting a state as an argument. Furthermore, the name of
the formal parameter into which the current state is passed must be
STATE and nothing but the current state may be passed into a
formal of that name. Therefore, only certain access and change
functions can use that formal -- namely with a
STATE formal --
and if any such function produces a new state it becomes the
``current state'' and must be passed along in the
thereafter. Thus, ACL2 requires that the state be single-threaded.
This, in turn, allows us to represent only one state at a time and
to produce new states from it destructively in a von Neumaneque
fashion. The syntactic restrictions on the variable
enforced by the translate mechanism (see trans and see term) when
terms are read.
To prevent the novice user from seeing messages prohibiting certain
uses of the variable symbol
STATE ACL2 has a mode in which it
simply disallows the use of that symbol as a formal parameter. Use of
the symbol causes a simple error message. The system is initially
in that mode.
To get out of that mode, execute:
:set-state-ok tIt is not recommended that you do this until you have read the documentation of
To enter the mode in which use of
state is prohibited as a formal
The mode is stored in the defaults table, See acl2-defaults-table.
Thus, the mode may be set locally in books.
Major Section: EVENTS
Example Forms: try guard verification? (set-verify-guards-eagerness 0) ; no, unless :verify-guards t (set-verify-guards-eagerness 1) ; yes if a :guard is supplied (set-verify-guards-eagerness 2) ; yes, unless :verify-guards nilNote: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
General Form: (set-verify-guards-eagerness n)where
nis a variable-free term that evaluates to
2. This macro is equivalent to
(table acl2-defaults-table :verify-guards-eagerness term).However, unlike that simple call of the
tableevent function (see table), no output results from a
Set-verify-guards-eagerness may be thought of as an event that
merely sets a flag to
2. The flag is used by
defun events to determine whether guard verification is
tried. The flag is irrelevant to those
defun events in
program mode and to those
defun events in which an explicit
verify-guards setting is provided among the
xargs. In the
former case, guard verification is not done because it can only be
done when logical functions are being defined. In the latter case,
verify-guards setting determines whether guard
verification is tried. So consider a
verify-guards setting is provided. Is guard
verification tried? The answer depends on the eagerness setting as
follows. If the eagerness is
0, guard verification is not tried.
If the eagerness is
1, it is tried iff a
guard is explicitly
provided in the
defun. If the eagerness is
verification is tried.
The default behavior of the system is as though the
Major Section: EVENTS
Examples: (set-well-founded-relation lex2)provided
lex2has been proved to be a well-founded relation (see well-founded-relation). Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
General Form: (set-well-founded-relation rel)where
relhas been proved to be a well-founded relation on objects satisfying some predicate,
mp, as described in the documentation for well-founded-relation. This macro is equivalent to
(table acl2-defaults-table :well-founded-relation 'rel).
This event sets the default well-founded relation to be that imposed
mp-measures by the relation
rel. Subsequently, if a recursively
defined function is submitted to
defun with no explicitly given
defun uses the default relation,
rel, and the associated domain predicate
mp used in its
well-foundedness theorem. That is, the termination conditions
generated will require proving that the measure used by the
mp-measure and that in every recursive call the measure of the
arguments decreases according to
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.
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 insure 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.
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. 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.
Major Section: EVENTS
Example: (table term-table t '((binary-+ x y) '3 'nil (car x)))
See table for a general discussion of tables and the
event used to manipulate tables.
term-table'' is used at the time a meta rule is checked for
syntactic correctness. Each proposed metafunction is run on each
term in this table, and the result in each case is checked to make
sure that it is a
termp in the current world. In each case where
this test fails, a warning is printed.
Whenever a metafunction is run in support of the application of a
meta rule, the result must be a term in the current world. When the
result is not a term, a hard error arises. The
term-table is simply
a means for providing feedback to the user at the time a meta rule
is submitted, warning of the definite possibility that such a hard
error will occur at some point in the future.
The key used in
term-table is arbitrary. The top-most value is
always the one that is used; it is the entire list of terms to be
considered. Each must be a
termp in the current ACL2 world.
Major Section: EVENTS
Example: (theory-invariant (not (and (member-equal '(:rewrite left-to-right) theory) (member-equal '(:rewrite right-to-left) theory))))where
General Forms: (theory-invariant term) ; conjoin a new invariant term or (theory-invariant term key) ; change an existing invariant term
termis a term that uses no variables other than
keyis an arbitrary ``name'' for this invariant. If
keyis omitted, an integer is generated and used.
Theory-invariantis an event that adds to or modifies the table of user-supplied theory invariants that are checked each time a theory expression is evaluated.
The theory invariant mechanism is provided via a table
(see table) named
theory-invariant-table. In fact, the
theory-invariant ``event'' is just a macro that expands into a use
table event. More general access to the
table is provided by
table itself. For example, the table can be
inspected or cleared (setting the invariant to
Theory-invariant-table maps arbitrary keys to terms mentioning, at
most, the variables
world. Every time an alleged theory
expression is evaluated, e.g., in the
in-theory event or
hint, each of the terms in
theory-invariant-table is evaluated with
theory bound to the runic theory (see theories) obtained from
the theory expression and
world bound to the current ACL2 world
(see world). If the result is
nil, a warning message is
printed. Thus, the table can be thought of as a list of conjuncts.
term in the table has a ``name,'' which is just the key under
which the term is stored. When a theory violates the restrictions
specified by some term, both the name and the term are printed. By
theory-invariant with a new term but the same name, you can
overwrite that conjunct of the theory invariant.
Theory invariants are particularly useful in the context of large rule sets intended for re-use. Such sets often contain conflicting rules, e.g., rules that are to be enabled when certain function symbols are disabled, rules that rewrite in opposite directions and thus loop if simultaneously enabled, groups of rules which should be enabled in concert, etc. The developer of such rule sets understands these restrictions and probably documents them. The theory invariant mechanism allows the developer to codify his restrictions so that when they are violated the user is warned.
Since theory invariants are arbitrary terms, macros may be used to express commonly used restrictions. Because theory invariants are a new idea in ACL2, we have only defined one such macro for illustrative purposes. Executing the event
(theory-invariant (incompatible (:rewrite left-to-right) (:rewrite right-to-left)))would subsequently cause a warning message any time the current theory contained both of the two runes shown. Of course, incompatible is just defined as a macro. Its definition may be inspected with
Note: If the table event is used directly to
:put a term into the
theory invariant table, be aware that the term must be in translated
form. This is enforced by the
value invariant for
theory-invariant-table. But the upshot of this is that you will be
unable to use macros in theory invariants stored directly with the
:put table event.
Major Section: EVENTS
Examples: (verify-guards flatten) (verify-guards flatten :hints (("Goal" :use (:instance assoc-of-app))) :otf-flg t :doc "string")See guard for a general discussion of guards. In the General Form above,
General Form: (verify-guards name :hints hints :otf-flg otf-flg :doc doc-string)
nameis the name of a
logicfunction (see defun-mode) or of a theorem or axiom. In the most common case
nameis the name of a function that has not yet had its guards verified, each subroutine of which has had its guards verified.
otf-flgare as described in the corresponding
doc-string, if supplied, is a string not beginning with ``
:Doc-Section''. The three keyword arguments above are all optional.
Verify-guardswill attempt to prove that the guard on the named function implies the guards of all of the subroutines called in the body of the function. If successful,
nameis considered to have had its guards verified.
name is one of several functions in a mutually recursive clique,
verify-guards will attempt to verify the guards of all of the
name is a theorem or axiom name,
verify-guards verifies the
guards of the associated formula. When a theorem has had its guards
verified then you know that the theorem will evaluate to non-
in all Common Lisps, without causing a runtime error (other than possibly
a resource error). In particular, you know that the theorem's validity
does not depend upon ACL2's arbitrary completion of the domains of partial
Common Lisp functions.
For example, if
app is defined as
(defun app (x y) (declare (xargs :guard (true-listp x))) (if (endp x) y (cons (car x) (app (cdr x) y))))then we can verify the guards of
appand we can prove the theorem:
(defthm assoc-of-app (equal (app (app a b) c) (app a (app b c))))However, if you go into almost any Common Lisp in which
appis defined as shown and evaluate
(equal (app (app 1 2) 3) (app 1 (app 2 3)))we get an error or, perhaps, something worse like
nil! How can this happen since the formula is an instance of a theorem? It is supposed to be true!
It happens because the theorem exploits the fact that ACL2 has completed
the domains of the partially defined Common Lisp functions like
cdr, defining them to be
nil on all non-conses. The formula
above violates the guards on
app. It is therefore ``unreasonable''
to expect it to be valid in Common Lisp.
But the following formula is valid in Common Lisp:
(if (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))) t)That is, no matter what the values of
cthe formula above evaluates to
tin all Common Lisps (unless the Lisp engine runs out of memory or stack computing it). Furthermore the above formula is a theorem:
(defthm guarded-assoc-of-app (if (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))) t))This formula,
guarded-assoc-of-app, is very easy to prove from
assoc-of-app. So why prove it? The interesting thing about
guarded-assoc-of-appis that we can verify the guards of the formula. That is,
(verify-guards guarded-assoc-of-app)succeeds. Note that it has to prove that if
bare true lists then so is
(app a b)to establish that the guard on the outermost
appon the left is satisfied. By verifying the guards of the theorem we know it will evaluate to true in all Common Lisps. Put another way, we know that the validity of the formula does not depend on ACL2's completion of the partial functions or that the formula is ``well-typed.''
One last complication: The careful reader might have thought we could
(implies (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))))rather than using the
ifform of the theorem. We cannot! The reason is technical:
impliesis defined as a function in ACL2. When it is called, both arguments are evaluated and then the obvious truth table is checked. That is,
impliesis not ``lazy.'' Hence, when we write the guarded theorem in the
impliesform we have to prove the guards on the conclusion without knowing that the hypothesis is true. It would have been better had we defined
impliesas a macro that expanded to the
ifform, making it lazy. But we did not and after we introduced guards we did not want to make such a basic change.
Recall however that
verify-guards is almost always used to verify
the guards on a function definition rather than a theorem. We now
return to that discussion.
name is not uniquely associated with the
(it necessarily names a previously defined function) the
doc-string, is not stored in the
documentation data base. Thus, we actually prohibit
from having the form of an ACL2 documentation string;
Verify-guards must often be used when the value of a recursive call
of a defined function is given as an argument to a subroutine that
is guarded. An example of such a situation is given below. Suppose
app (read ``append'') has a guard requiring its first argument to be
(defun rev (x) (declare (xargs :guard (true-listp x))) (cond ((endp x) nil) (t (app (rev (cdr x)) (list (car x))))))Observe that the value of a recursive call of
revis being passed into a guarded subroutine,
app. In order to verify the guards of this definition we must show that
(rev (cdr x))produces a
true-listp, since that is what the guard of
apprequires. How do we know that
(rev (cdr x))is a
true-listp? The most elegant argument is a two-step one, appealing to the following two lemmas: (1) When
(cdr x)is a
true-listp. (2) When
(rev z)is a
true-listp. But the second lemma is a generalized property of
rev, the function we are defining. This property could not be stated before
revis defined and so is not known to the theorem prover when
Therefore, we might break the admission of
rev into three steps:
rev without addressing its guard verification, prove some
general properties about
rev, and then verify the guards. This can
be done as follows:
(defun rev (x) (declare (xargs :guard (true-listp x) :verify-guards nil)) ; Note this additional xarg. (cond ((endp x) nil) (t (app (rev (cdr x)) (list (car x))))))The ACL2 system can actually admit the original definition of
(defthm true-listp-rev (implies (true-listp x2) (true-listp (rev x2))))
rev, verifying the guards as part of the
defunevent. The reason is that, in this particular case, the system's heuristics just happen to hit upon the lemma
true-listp-rev. But in many more complicated functions it is necessary for the user to formulate the inductively provable properties before guard verification is attempted.
Major Section: EVENTS
Examples: (verify-termination fact) (verify-termination fact (declare (xargs :guard (and (integerp x) (>= x 0)))))where
General Forms: (verify-termination fn dcl ... dcl) (verify-termination (fn1 dcl ... dcl) (fn2 dcl ... dcl) ...)
fniare function symbols having
programmode (see defun-mode) and all of the
dcls are either
declareforms or documentation strings. The first form above is an abbreviation for
(verify-termination (fn dcl ... dcl))so we limit our discussion to the second form. Each of the
fnimust be in the same clique of mutually recursively defined functions, but not every function in the clique need be among the
Verify-termination attempts to establish the admissibility of the
Verify-termination retrieves their definitions, creates modified
definitions using the
dcls supplied above, and resubmits these
definitions. You could avoid using
verify-termination by typing the new
definitions yourself. So in that sense,
verify-termination adds no new
functionality. But if you have prototyped your system in
mode and tested it, you can use
verify-termination to resubmit your
definitions and change their defun-modes to
hints without having to retype or recopy the code. You can also add or
modify guards at this time.
defun command executed by
verify-termination is obtained
by retrieving the
mutual-recursion) command that
introduced the clique in question and then possibly modifying each
definition as follows. Consider a function,
fn, in the clique.
fn is not among the
fni above, its definition is left
fn is some
fni and we modify its
definition by inserting into it the corresponding
fni in the arguments to
verify-termination. In addition,
we throw out from the old declarations in
specification and anything that is specified in the new
For example, suppose that
fact was introduced with:
(defun fact (n) (declare (type integer n) (xargs :mode :program)) (if (zp n) 1 (* n (fact (1- n))))).Suppose later we do
(verify-termination fact). Then the following definition is submitted.
(defun fact (n) (declare (type integer n)) (if (zp n) 1 (* n (fact (1- n))))).Observe that this is the same definition as the original one, except the old specification of the
:modehas been deleted so that the defun-mode now defaults to
logic. Although the termination proof succeeds, ACL2 also tries to verify the guard, because we have (implicitly) provided a guard, namely
(integerp n), for this function. (See guard for a general discussion of guards, and see type-spec for a discussion of how type declarations are used in guards.) Unfortunately, the guard verification fails, because the subterm
(zp n)requires that
nbe nonnegative, as can be seen by invoking
:args zp. (For a discussion of termination issues relating to recursion on the naturals, see zero-test-idioms.) So we might want to submit
(verify-termination fact (declare (xargs :guard (and (integerp n) (<= 0 n)))))which will submit the definition
(defun fact (n) (declare (xargs :guard (and (integerp n) (<= 0 n)))) (if (zp n) 1 (* n (fact (1- n))))).Observe that the declaration in the
verify-terminationcommand has been inserted into the definition. In fact, this command succeeds.