This is documentation for ACL2 Version 3.4
Copyright (C) 2008  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

REDO-FLAT    redo up through a failure in an encapsulate or progn

When one submits an encapsulate or progn event and one of its
sub-events fails, ACL2 restores its logical world as though the
encapsulate or progn had not been run.  But sometimes one would like to
debug the failure by re-executing all sub-events that succeeded up to
the point of failure, and then re-executing the failed sub-event.  Said
differently, imagine that the top-level encapsulate or progn form, as
well as all such sub-forms, were flattened into a list of events that
were then submitted to ACL2 up to the point of failure.  This would put
us in the state in which the original failed event had failed, so we
could now submit that failed event and try modifying it, or first
proving additional events, in order to get it admitted.

Redo-flat is provided for this purpose.  Consider the following (rather
nonsensical) example, in which the defun of f3 fails (the body is y but
the formal parameter list is (x)).

     (encapsulate
      ()
      (defun f1 (x) x)
      (encapsulate ()
                   (local (defthm hack (equal (car (cons x y)) x))))
      (encapsulate ()
                   (local (defthm hack (equal (+ x y) (+ y x)))))
      (encapsulate ()
                   (make-event '(defun f2 (x) x))
                   (progn (defthm foo (equal x x) :rule-classes nil)
                          (defun f3 (x) y)))
      (defun f4 (x) x)
      (defun f5 (x) y))

After this attempt fails, you can evaluate the following form.

     (redo-flat)

This will first lay down a deflabel event, (deflabel r), so that you
can eventually remove your debugging work with (:ubt! r).  Then the
successful sub-events that preceded the failure will be executed with
proofs skipped (so that this execution is fast).  Then, the failed
event will be executed.  Finally, a :pbt command is executed so that
you can see a summary of the events that executed successfully.

You can eliminate some of the steps above by supplying keyword values,
as follows.

     (redo-flat
      :succ  succ ; Skip the successful sub-events if val is nil.
      :fail  fail ; Skip the failed sub-event if val is nil.
      :label lab  ; Skip deflabel if lab or succ is nil, else use (deflabel lab).
      :pbt   val  ; Skip the final :pbt if val, lab, or succ is nil.
      )

Also, you can avoid skipping proofs for the successful sub-events by
supplying keyword :succ-ld-skip-proofsp with a valid value for
ld-skip-proofsp; see LD-SKIP-PROOFSP.

If you prefer only to see the successful and failed sub-events, without
any events being re-executed, you may evaluate the following form
instead.

     (redo-flat :show t)

For the example above, this command produces the following output.

     List of events (from encapsulate or progn) preceding the failure:

     ((DEFUN F1 (X) X)
      (ENCAPSULATE NIL
                   (LOCAL (DEFTHM HACK (EQUAL (CAR (CONS X Y)) X))))
      (ENCAPSULATE NIL
                   (LOCAL (DEFTHM HACK (EQUAL (+ X Y) (+ Y X)))))
      (MAKE-EVENT '(DEFUN F2 (X) X))
      (DEFTHM FOO (EQUAL X X)
              :RULE-CLASSES NIL))

     Failed event:

     (DEFUN F3 (X) Y)
     ACL2 !>

Redo-flat uses a scheme that should not cause spurious name conflicts
for local events.  Above, it is mentioned that events are "flattened";
now we clarify this notion.  Each sub-event that succeeds and is an
encapsulate or progn is left intact.  Only such events that fail are
replaced by their component events.  Thus, in the example above, there
is no conflict between the two local sub-events named "hack," because
these are contained in successful encapsulate sub-events, which are
therefore not flattened.  The progn and two encapsulate events
surrounding the definition of f3 are, however, flattened, because that
definition failed to be admitted.

Unfortunately, an event must actually fail in order for redo-flat to
work.  So if the system is "stuck" on an event, then you may find it
helpful to insert an illegal event just in front of it before
submitting the encapsulate or progn.

REMOVE-CUSTOM-KEYWORD-HINT    remove a custom keyword hint

     Example Forms:
     (remove-custom-keyword-hint :my-hint)

     General Form:
     (remove-custom-keyword-hint keyword)

where keyword is a keywordp.

For an explanation of how custom keyword hints are processed, see
CUSTOM-KEYWORD-HINTS; also see ADD-CUSTOM-KEYWORD-HINT.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

SET-BODY    set the definition body

     Examples:
     (set-body foo (:definition foo)) ; restore original definition of foo
     (set-body foo foo) ; same as just above
     (set-body foo my-foo-def) ; use my-foo-def for the body of foo
     (set-body foo (:definition my-foo-def)) ; same as just above

Rules of class :definition can install a new definition body, used for
example by :expand hints.  See DEFINITION and also see
HINTS for a detailed discussion of the :install-body fields of
:definition rules and their role in :expand hints.

There may be several such definitions, but by default, the latest one
is used by :expand hints.  Although the :with keyword may be used in
:expand hints to override this behavior locally (see HINTS), it
may be convenient to install a definition for expansion other than the
latest one -- for example, the original definition.  Set-body may be
used for this purpose.

     General Form:
     (set-body function-symbol rule-name)

where rule-name is either a :definition rune or is a function symbol,
sym, which represents the rune (:definition sym).

You can view all definitions available for expansion; see
SHOW-BODIES.

SHOW-CUSTOM-KEYWORD-HINT-EXPANSION    print out custom keyword hints when they are expanded

       Examples:
       (show-custom-keyword-hint-expansion t)
       (show-custom-keyword-hint-expansion nil)

       General Form:
       (show-custom-keyword-hint-expansion flg)

If the value of flg is non-nil, then when custom keyword hints are
expanded, the system prints the results of each expansion.  This is
sometimes   useful for debugging custom keyword hints and, from time to
time, may be   useful in understanding how a custom hint affects some
proof attempt.

The default setting is nil.

For an explanation of how custom keyword hints are processed,   see
CUSTOM-KEYWORD-HINTS.

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

     * Menu:

     * USING-TABLES-EFFICIENTLY:: Notes on how to use tables efficiently

     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 single variable world, 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 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 test in the given
world.  Often you have access to world.

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.  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 :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.  Each
table has a "name," which must be a symbol.  Given a table name, there
are six operations one might perform 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.

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 evaluated to obtain the key and value may 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 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)

Provided the named table is empty and has not yet been assigned a
:guard and term (which is not evaluated) is a term that mentions at
most the variables key, val and world, this event sets the :guard of
the named table to term.  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, and world bound to the then current
world.  An error will be caused by the :put if the result of the
evaluation is nil.

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.  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 deflabel (see DEFLABEL); also
see DEFDOC.

USING-TABLES-EFFICIENTLY    Notes on how to use tables efficiently

(Thanks to Jared Davis for contributing this documentation topic, to
which we have made only minor modifications.)

Support your book contains table events, or macros that expand into
table events, of the following form:

        (table my-table 'my-field <computation>)

Then <computation> will be evaluated _twice_ during certify-book and
_again_ every time you include the book with include-book.  In some
cases this overhead can be avoided using make-event.

See also books/make-event/defconst-fast.lisp for an analogous trick
involving defconst.

Related topics other than immediate subtopics:

As an example, suppose we want to store numbers in a table only if they
satisfy some computationally expensive predicate.  We'll introduce a new
book, number-table.lisp, and create a table to store these numbers:

       (table number-table 'data nil)

Instead of implementing a "computationally expensive predicate," we'll
write a function that just prints a message when it is called and
accepts even numbers:

     (defun expensive-computation (n)
       (prog2$ (cw "Expensive computation on ~x0.~%" n)
               (evenp n)))

Now we'll implement a macro, add-number, which will add its argument to
the table only if it satisfies the expensive predicate:

     (defmacro add-number (n)
       `(table number-table 'data
               (let ((current-data
                      (cdr (assoc-eq 'data (table-alist 'number-table world)))))
                 (if (expensive-computation ,n)
                     (cons ,n current-data)
                   current-data))))

Finally, we'll call add-number a few times to finish the book.

     (add-number 1)
     (add-number 2)
     (add-number 3)

When we now invoke (certify-book "number-table"), we see the expensive
predicate being called twice for each number: once in Step 2, the main
pass, then again in Step 3, the admissibility check.  Worse, the
computation is performed again for each number when we use include-book
to load number-table, e.g.,

        ACL2 !>(include-book "number-table")
        Expensive computation on 1.
        Expensive computation on 2.
        Expensive computation on 3.

To avoid these repeated executions, we can pull the test out of the
table event using make-event.  Here's an alternate implementation of
add-number that won't repeat the computation:

     (defmacro add-number (n)
       `(make-event
         (if (expensive-computation ,n)
             '(table number-table 'data
                     (cons ,n (cdr (assoc 'data
                                          (table-alist 'number-table world)))))
           '(value-triple :expensive-computation-failed))))

When we recertify number-table.lisp, we'll see the expensive computation
is still called once for each number in Step 2, but is no longer called
during Step 3.  Similarly, the include-book no longer shows any calls
of the expensive computation.

THEORY-INVARIANT    user-specified invariants on theories

     Examples:
     (theory-invariant (not (and (active-runep '(:rewrite left-to-right))
                                 (active-runep '(:rewrite right-to-left))))
                       :key my-invariant
                       :error nil)

     ; Equivalent to the above:
     (theory-invariant (incompatible (:rewrite left-to-right)
                                     (:rewrite right-to-left))
                       :key my-invariant
                       :error nil)

     General Form:
     (theory-invariant term &key key error)

where:

     o term is a term that uses no variables other than ens and state;

     o key is an arbitrary "name" for this invariant (if omitted, an
     integer is generated and used); and

     o :error specifies the action to be taken when an invariant is
     violated -- either nil if a warning is to be printed, else t (the
     default) if an error is to be caused.

Theory-invariant is 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 of the table event.
More general access to the theory-invariant table is provided by table
itself.  For example, the table can be inspected or cleared with table;
you can clear an individual theory invariant by setting the invariant
to t, or eliminate all theory invariants with the command (table
theory-invariant-table nil nil :clear).

Theory-invariant-table maps arbitrary keys to records containing terms
that mention, at most, the variables ens and state.  Every time an
alleged theory expression is evaluated, e.g., in the in-theory event or
:in-theory hint, each of the terms in theory-invariant-table is
evaluated with ens bound to a so-called "enabled structure" obtained
from the theory expression and state bound to the current ACL2 state
(see STATE).  Users generally need not know about the enabled
structure, other than that it can be accessed using the macros
active-runep and incompatible; see ACTIVE-RUNEP and see
INCOMPATIBLE.  If the result is nil, a message is printed and an
error occurs (except, only a warning occurs if :error nil is
specified).  Thus, the table can be thought of as a list of conjuncts.
Each 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 calling
theory-invariant with a new term but the same name, you can overwrite
that conjunct of the theory invariant; but see the Local Redefinition
Caveat at the end of this note.  You may want to avoid using explicit
names, since otherwise the subsequent inclusion of another book that
defines a theory invariant with the same name will override your 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 the
user is alerted when they are violated.

Since theory invariants are arbitrary terms, macros may be used to
express commonly used restrictions.  For example, executing the event

     (theory-invariant (incompatible (:rewrite left-to-right)
                                     (:rewrite right-to-left)))

would subsequently cause an error 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 :pe incompatible.

In order for a theory-invariant event to be accepted, the proposed
theory invariant must be satisfied by the current theory (see
CURRENT-THEORY).  The value returned upon successful execution of the
event is the key (whether user-supplied or generated).

Local Redefinition Caveat.  Care needs to be taken when redefining a
theory invariant in a local context.  Consider the following example.

     (theory-invariant
      (active-runep '(:definition binary-append))
      :key app-inv)

     (encapsulate
      ()
      (local (theory-invariant t :key app-inv))
      (in-theory (disable binary-append))
      (defthm ...))

The second pass of the encapsulate will fail, because the in-theory
event violates the original theory-invariant and the local
theory-invariant is skipped in the second pass of the encapsulate.  Of
course, local theory-invariants in books can cause the analogous
problem in the second (include-book) pass of a certify-book.  In both
cases, though, the theory invariants are only checked at the conclusion
of the (include-book or encapsulate) event.  Indeed, theory invariants
are checked at the end of every event related to theories, including
defun, defthm, in-theory, encapsulate, and include-book, except for
events executed on behalf of an include-book or the second pass of an
encapsulate.

UNMEMOIZE    turn off memoization for the specified function

     Example:
     (unmemoize 'foo) ; turn off memoization of foo

     General Form:
     (unmemoize fn)

where fn evaluates to a function symbol that is currently memoized; see
MEMOIZE.  An exception is that as with memoize, fn may evaluate
to the name of a macro that is associated with such a function symbol;
see MACRO-ALIASES-TABLE.

Calls of this macro generate events of the form (table memoize-table fn
nil).  When successful, the returned value is of the form (mv nil
function-symbol state).

VALUE-TRIPLE    compute a value, optionally checking that it is not nil

     Examples:
     (value-triple (+ 3 4))
     (value-triple (cw "hi") :on-skip-proofs t)
     (value-triple (@ ld-pre-eval-print))
     (value-triple (@ ld-pre-eval-print) :check t)

     General Form:
     (value-triple form
                   :on-skip-proofs sp ; optional; nil by default
                   :check chk         ; optional; nil by default
                   )

Value-triple provides a convenient way to evaluate a form in an event
context, including progn and encapsulate and in books; see
EVENTS.  The form should evaluate to a single, non-stobj value.

Calls of value-triple are generally skipped when proofs are being
skipped, in particular when ACL2 is performing the second pass through
the events of an encapsulate form or during an include-book, or indeed
any time ld-skip-proofsp is non-nil.  If you want the call evaluated
during those times as well, use a non-nil value for :on-skip-proofs.
Note that the argument to :on-skip-proofs is not evaluated.

If you expect the form to evaluate to a non-nil value and you want an
error to occur when that is not the case, you can use :check t.  More
generally, the argument of :check can be a form that evaluates to a
single, non-stobj value.  If this value is not nil, then the
aforementioned test is made (that the given form is not nil).  If an
error occurs and the value of :check is a string or indeed any
"message" suitable for printing by fmt when supplied as a value for
tilde-directive ~@, then that string or message is printed.

VERIFY-GUARDS    verify the guards of a function

     Examples:
     (verify-guards flatten)
     (verify-guards flatten
                    :hints (("Goal" :use (:instance assoc-of-app)))
                    :otf-flg t
                    :guard-debug t ; default = nil
                    :doc "string")

     General Form:
     (verify-guards name
             :hints        hints
             :otf-flg      otf-flg
             :guard-debug  t ; typically t, but any value is legal
             :doc          doc-string)

See GUARD for a general discussion of guards.  In the General
Form above, name is the name of a :logic function (see
DEFUN-MODE) or of a theorem or axiom.  In the most common case name
is the name of a function that has not yet had its guards verified,
each subroutine of which has had its guards verified. hints, otf-flg,
and guard-debug are as described in the corresponding :doc entries; and
doc-string, if supplied, is a string *not* beginning with
":Doc-Section".  The four keyword arguments above are all optional.
Verify-guards will 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, and that the guards are satisfied for all function
calls in the guard itself (under an implicit guard of t).  If
successful, name is considered to have had its guards verified.

See VERIFY-GUARDS-FORMULA for a utility that lets you view the
formula to be proved by verify-guards, but without creating an event.

If name is one of several functions in a mutually recursive clique,
verify-guards will attempt to verify the guards of all of the functions.

If 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-nil 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 app and 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 app is 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 car and
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 a, b and c the formula above
evaluates to t in 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-app is 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 a and b are true lists then so is (app a b) to
establish that the guard on the outermost app on 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
state guarded-assoc-of-app as

     (implies (and (true-listp a)
                   (true-listp b))
              (equal (app (app a b) c)
                     (app a (app b c))))

rather than using the if form of the theorem.  We cannot!  The reason
is technical:  implies is defined as a function in ACL2.  When it is
called, both arguments are evaluated and then the obvious truth table
is checked.  That is, implies is not "lazy."  Hence, when we write the
guarded theorem in the implies form we have to prove the guards on the
conclusion without knowing that the hypothesis is true.  It would have
been better had we defined implies as a macro that expanded to the if
form, 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.

Because name is not uniquely associated with the verify-guards event
(it necessarily names a previously defined function) the documentation
string, doc-string, is not stored in the documentation data base.
Thus, we actually prohibit doc-string from having the form of an ACL2
documentation string; see DOC-STRING.

If the guard on a function is not t, then guard verification requires
not only consideration of the body under the assumption that the guard
is true, but also consideration of the guard itself.  Thus, for
example, guard verification fails in the following example, even though
there are no proof obligations arising from the body, because the guard
itself can cause a guard violation when evaluated for an arbitrary
value of x:

     (defun foo (x)
       (declare (xargs :guard (car x)))
       x)

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 a
true-listp.  Consider

     (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 rev is 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 app requires.  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 x is a true-listp, (cdr
x) is a true-listp.  (2) When z is a true-listp, (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 rev
is defined and so is not known to the theorem prover when rev is
defined.

Therefore, we might break the admission of rev into three steps: define
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))))))

     (defthm true-listp-rev
       (implies (true-listp x2)
                (true-listp (rev x2))))

     (verify-guards rev)

The ACL2 system can actually admit the original definition of rev,
verifying the guards as part of the defun event.  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.

*Note on computation of guard conjectures and evaluation*.  When ACL2
computes the guard conjecture for the body of a function, it evaluates
any ground subexpressions (those with no free variables), for calls of
functions whose :executable-counterpart runes are enabled.  Note that
here, "enabled" refers to the current global theory, not to any :hints
given to the guard verification process; after all, the guard
conjecture is computed even before its initial goal is produced.  Also
note that this evaluation is done in an environment as though
:set-guard-checking :all had been executed, so that we can trust that
this evaluation takes place without guard violations; see
SET-GUARD-CHECKING.

VERIFY-TERMINATION    convert a function from :program mode to :logic mode

     Example:
     (verify-termination fact)

     General Forms:
     (verify-termination fn dcl ... dcl)
     (verify-termination (fn1 dcl ... dcl)
                         (fn2 dcl ... dcl)
                         ...)

where fn and the fni are function symbols having :program mode (see
DEFUN-MODE) and all of the dcls are either declare forms 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 fni must be
in the same clique of mutually recursively defined functions, but not
every function in the clique need be among the fni.

Verify-termination attempts to establish the admissibility of the fni.
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 :program mode
and tested it, you can use verify-termination to resubmit your
definitions and change their defun-modes to :logic, addings hints
without having to retype or recopy the code.

The defun command executed by verify-termination is obtained by
retrieving the defun (or mutual-recursion) command that introduced the
clique in question and then possibly modifying each definition as
follows.  Consider a function, fn, in the clique.  If fn is not among
the fni above, its definition is left unmodified other than to add
(declare (xargs :mode :logic)).  Otherwise, fn is some fni and we
modify its definition by inserting into it the corresponding dcls listed
with fni in the arguments to verify-termination, as well as (declare
(xargs :mode :logic)).  In addition, we throw out from the old
declarations in fn the :mode specification and anything that is
specified in the new dcls.

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 :mode has 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 n be 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
be tempted to submit the following:

     (verify-termination
      fact
      (declare (xargs :guard (and (integerp n) (<= 0 n))))).

However, this is considered a changing of the guard (from (integerp n)),
which is illegal.  If we instead change the guard in the earlier defun
after undoing that earlier definition with :ubt fact, then
(verify-termination fact) will succeed.

HISTORY    functions that display or change history

ACL2 keeps track of the commands that you have executed that have
extended the logic or the rule data base, as by the definition of
macros, functions, etc.  Using the facilities in this section you can
review the sequence of commands executed so far.  For example, you can
ask to see the most recently executed command, or the command 10 before
that, or the command that introduced a given function symbol.  You can
also undo back through some previous command, restoring the logical
world to what it was before the given command.

The annotations printed in the margin in response to some of these
commands (such as `P', `L', and `V') are explained in the documentation
for :pc.

Several technical terms are used in the documentation of the history
commands.  You must understand these terms to use the commands.  These
terms are documented via :doc entries of their own.  See
COMMAND, see EVENTS, see COMMAND-DESCRIPTOR, and see
LOGICAL-NAME.

OOPS    undo a :u or :ubt

The keyword command :oops will undo the most recent :ubt (or :u, which
we here consider just another :ubt).  A second :oops will undo the next
most recent :ubt, a third will undo the :ubt before that one, and a
fourth :oops will return the logical world to its configuration before
the first :oops.

Consider the logical world (see WORLD) that represents the
current extension of the logic and ACL2's rules for dealing with it.
The :ubt and :u commands "roll back" to some previous world (see
UBT).  Sometimes these commands are used to inadvertently undo useful
work and user's wish they could "undo the last undo."  That is the
function provided by :oops.

:Oops is best described in terms of an implementation.  Imagine a ring
of four worlds and a marker (*) indicating the current ACL2 world:

                  *
                w0
              /    \
            w3      w1
              \    /
                w2

This is called the "kill ring" and it is maintained as follows.  When
you execute an event the current world is extended and the kill ring is
not otherwise affected.  When you execute :ubt or :u, the current world
marker is moved one step counterclockwise and that world in the ring is
replaced by the result, say w0', of the :ubt or :u.

                w0
              /    \
           *w0'     w1
              \    /
                w2

If you were to execute events at this point, w0' would be extended and
no other changes would occur in the kill ring.

When you execute :oops, the marker is moved one step clockwise.  Thus
the kill ring becomes

                  *
                w0
              /    \
            w0'     w1
              \    /
                w2

and the current ACL2 world is w0 once again.  That is, :oops "undoes"
the :ubt that produced w0' from w0.  Similarly, a second :oops will
move the marker to w1, undoing the undo that produced w0 from w1.  A
third :oops makes w2 the current world.  Note however that a fourth
:oops restores us to the configuration previously displayed above in
which w0' has the marker.

In general, the kill ring contains the current world and the three most
recent worlds in which a :ubt or :u were done.

While :ubt may appear to discard the information in the events undone,
we can see that the world in which the :ubt occurred is still
available.  No information has been lost about that world.  But :ubt
does discard information!  :Ubt discards the information necessary to
recover from the third most recent ubt!  An :oops, on the other hand,
discards no information, it just selects the next available world on
the kill ring and doing enough :oopses will return you to your starting
point.

We can put this another way.  You can freely type :oops and inspect the
world that you thus obtain with :pe, :pc, and other history commands.
You can repeat this as often as you wish without risking the permanent
loss of any information.  But you must be more careful typing :ubt or
:u.  While :oops makes :ubt seem "safe" because the most recent :ubt
can always be undone, information is lost when you execute :ubt.

We note that :ubt and :u may remove compiled definitions (but note that
in some Lisps, including CCL (OpenMCL) and SBCL, functions are always
compiled).  When the original world is restored using :oops, restored
functions will not generally be compiled (except for Lisps as above),
though the user can remedy this situation; see COMP.

Finally, we note that our implementation of oops can use a significant
amount of memory, because of the saving of old logical worlds.  Most
users are unlikely to experience a memory problem, but if you do, then
you may want to disable oops by evaluting (reset-kill-ring 0 state);
see RESET-KILL-RING.

PBT    print the commands back through a command descriptor

     Examples:
     :pbt :max      ; print back through the most recent command
     :pbt :x        ; print back through the most recent command
     :pbt fn        ; print back through the introduction of fn
     :pbt 5         ; print back through the fifth command executed
     :pbt (:x -4)   ; print back through the most recent five commands

See COMMAND-DESCRIPTOR.

Pbt takes one argument, a command descriptor, and prints the commands
from :max (aka :x) through the one described.  See
COMMAND-DESCRIPTOR for a description of what a command descriptor is.
See PC for a description of the format used to display
commands.  Pbt will print the commands that ubt will undo.