This is documentation for ACL2 Version 4.2
Copyright (C) 2011  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.

MUTUAL-RECURSION    define some mutually recursive functions

     Example:
     (mutual-recursion
      (defun evenlp (x)
        (if (consp x) (oddlp (cdr x)) t))
      (defun oddlp (x)
        (if (consp x) (evenlp (cdr x)) nil)))

     General Form:
     (mutual-recursion def1 ... defn)
     where each defi is a defun form or a defund form.

When mutually recursive functions are introduced it is necessary to do
the termination analysis on the entire clique of definitions.  Each
defun form specifies its own measure, either with the :measure keyword
xarg (see XARGS) or by default to acl2-count.  When a function
in the clique calls a function in the clique, the measure of the
callee's actuals must be smaller than the measure of the caller's
formals -- just as in the case of a simply recursive function.  But
with mutual recursion, the callee's actuals are measured as specified
by the callee's defun while the caller's formals are measured as
specified by the caller's defun.  These two measures may be different
but must be comparable in the sense that o< decreases through calls.

If you want to specify :hints or :guard-hints (see XARGS), you
can put them in the xargs declaration of any of the defun forms, as the
:hints from each form will be appended together, as will the
guard-hints from each form.

You may find it helpful to use a lexicographic order, the idea being to
have a measure that returns a list of two arguments, where the first
takes priority over the second.  Here is an example.

     (include-book "ordinals/lexicographic-ordering" :dir :system)

     (encapsulate
      ()
      (set-well-founded-relation l<) ; will be treated as LOCAL

      (mutual-recursion
       (defun foo (x)
         (declare (xargs :measure (list (acl2-count x) 1)))
         (bar x))
       (defun bar (y)
         (declare (xargs :measure (list (acl2-count y) 0)))
         (if (zp y) y (foo (1- y))))))

The guard analysis must also be done for all of the functions at the
same time.  If any one of the defuns specifies the :verify-guards xarg
to be nil, then guard verification is omitted for all of the functions.
Similarly, if any one of the defuns specifies the :non-executable xarg
to be t, or if any of the definitions uses defun-nx or defund-nx, then
every one of the definitions will be treated as though it specifies a
:non-executable xarg of t.

Technical Note: Each defi above must be of the form (defun ...).  In
particular, it is not permitted for a defi to be a form that will
macroexpand into a defun form.  This is because mutual-recursion is
itself a macro, and since macroexpansion occurs from the outside in, at
the time (mutual-recursion def1 ... defk) is expanded the defi have not
yet been.  But mutual-recursion must decompose the defi.  We therefore
insist that they be explicitly presented as defuns or defunds (or a
mixture of these).

Suppose you have defined your own defun-like macro and wish to use it
in a mutual-recursion expression.  Well, you can't.  (!)  But you can
define your own version of mutual-recursion that allows your defun-like
form.  Here is an example.  Suppose you define

     (defmacro my-defun (&rest args) (my-defun-fn args))

where my-defun-fn takes the arguments of the my-defun form and produces
from them a defun form.  As noted above, you are not allowed to write
(mutual-recursion (my-defun ...) ...).  But you can define the macro
my-mutual-recursion so that

     (my-mutual-recursion (my-defun ...) ... (my-defun ...))

expands into (mutual-recursion (defun ...) ... (defun ...)) by applying
my-defun-fn to each of the arguments of my-mutual-recursion.

     (defun my-mutual-recursion-fn (lst)
       (declare (xargs :guard (alistp lst)))

     ; Each element of lst must be a consp (whose car, we assume, is always
     ; MY-DEFUN).  We apply my-defun-fn to the arguments of each element and
     ; collect the resulting list of DEFUNs.

       (cond ((atom lst) nil)
             (t (cons (my-defun-fn (cdr (car lst)))
                      (my-mutual-recursion-fn (cdr lst))))))

     (defmacro my-mutual-recursion (&rest lst)

     ; Each element of lst must be a consp (whose car, we assume, is always
     ; MY-DEFUN).  We obtain the DEFUN corresponding to each and list them
     ; all inside a MUTUAL-RECURSION form.

       (declare (xargs :guard (alistp lst)))
       (cons 'mutual-recursion (my-mutual-recursion-fn lst))).

PROGN    evaluate some events

     Example Form:
     (progn (defun foo (x) x)
            (defmacro my-defun (&rest args)
              (cons 'defun args))
            (my-defun bar (x) (foo x)))

     General form:
     (progn event1 event2 ... eventk)

where k >= 0 and each eventi is a legal embedded event form (see
EMBEDDED-EVENT-FORM).  These events are evaluated in sequence.  A
utility is provided to assist in debugging failures of such execution;
see REDO-FLAT.

NOTE: If the eventi above are not all legal embedded event forms (see
EMBEDDED-EVENT-FORM), consider using er-progn or (with great
care!) progn! instead.

For a related event form that does allow introduction of constraints
and local events, see ENCAPSULATE.

ACL2 does not allow the use of progn in definitions.  Instead, the
macro er-progn can be used for sequencing state-oriented operations;
see ER-PROGN and see STATE.  If you are using
single-threaded objects (see STOBJ) you may wish to define a
version of er-progn that cascades the object through successive
changes.  ACL2's pprogn is the state analogue of such a macro.

If your goal is simply to execute a sequence of top-level forms, for
example a sequence of definitions, consider using ld instead; see
LD.

PROGN!    evaluate some forms, not necessarily events

*WARNING!*  This event is intended for advanced users who, in essence,
want to build extensions of ACL2.  See see DEFTTAG, in
particular, the "WARNING" there, and see the warning about stobjs at
the end of this documentation topic.

Progn! can be used like progn, even in books.  But unlike progn, progn!
does not require its constituent forms to be events (see
EMBEDDED-EVENT-FORM), except that the first form cannot be a symbol
unless it is :state-global-bindings (advanced feature, described
below).  However, see MAKE-EVENT for a "Restriction to the Top
Level" that still applies under a call of progn!.

Because progn! allows non-events, it differs from progn in another
important respect: progn! is illegal unless there is an active ttag;
see DEFTTAG.

See books/hacking/hacker.lisp for two macros, with-raw-mode and
with-redef-allowed, each defined in terms of progn!, that allow
arbitrary forms in contexts that would normally require legal embedded
event forms.

Given a form (progn! form1 form2 ... formk), ACL2 will evaluate each
formi in turn (for i from 1 to k).  If a form returns more than one
value (see MV) where the first value returned is not nil, then
no later form will be evaluated and the result returned by the progn!
call will be (mv erp val state) for some non-nil value erp, signifying
an error (see LD-ERROR-TRIPLES).  Otherwise the evaluation is
considered to have succeeded, and will continue with later forms.  The
value returned by a call of progn! with no such error is of the form
(mv nil v state), where v depends on the last form as follows.  If the
last form evaluates to a single value, then v is that value, except if
the value is a stobj, say ST, then v is the symbol REPLACED-ST.
Otherwise the last form evaluates to some (mv nil x ...), and v is x
unless after the final form's evaluation we are in raw-mode (see
SET-RAW-MODE), in which case the progn! call returns nil (so that
ACL2 can at least print the result -- imagine Lisp returning a pathname
object from a load call, for example).

The normal undoing mechanism does not generally apply to forms within a
progn! that are not legal ACL2 events (see EMBEDDED-EVENT-FORM).
In particular, note that a non-local call of progn! in an encapsulate
event will generally be evaluated twice: once on each pass.  This fact
is worth keeping in mind if you are using progn! to change the state of
the system; ask yourself if it is acceptable to apply that
state-changing operation more than once.

Please note that progn! may differ from progn in the following sense:
definitions within a call of progn! might not be compiled.  For
example, consider the following book.

     (in-package "ACL2")
     (defttag :test)
     (progn  (defun f1 (x) x))
     (progn! (defun f2 (x) x))

If the underlying Lisp is GCL 2.6.7, then after including this
certified book (where the default certification took place, creating a
compiled file), then f1 is a compiled function but f2 is not.  For
other Lisps supported by ACL2, both f1 and f2 are compiled, though we
are not sure that every function under every call of progn! would
similarly be compiled.

We now describe, for system hackers only, a sophisticated extension of
progn! not mentioned above: support for keyword argument
:state-global-bindings.  If the first argument of progn! is this
keyword, then the second argument is treated as a list of bindings as
expected by ACl2 system function state-global-let* (not yet documented).
Thus, in the ACL2 loop,

     (progn! :state-global-bindings bindings form1 form2 ... formk)

is treated as follows:

     (progn! (state-global-let* bindings (progn! form1 form2 ... formk)))

However, in raw Lisp the former is just:

     (progn form1 form2 ... formk)

Thus, one should use the :state-global-bindings argument with care,
since the behavior in the ACL2 loop can differ from that in Common
Lisp.  The intention is that one bind only state global variables that
are relevant to evaluation of the forms within the ACL2 loop and are
harmlessly ignored for evaluation of those forms in raw Lisp.  Here is
a typical sort of example, as state global ld-redefinition-action is
not relevant to the evaluation of defun in raw Lisp.

     (progn! (remove-untouchable 'ld-redefinition-action nil)
             (progn! :state-global-bindings
                     ((ld-redefinition-action '(:doit . :overwrite)))
                     (defun foo (x)
                       (cons x x)))
             (push-untouchable 'ld-redefinition-action nil))

Finally, we point out a pitfall of progn! related to stobjs.  The
following book can cause a hard Lisp error, depending on the host Common
Lisp, when certified with a non-nil value for compile-flg (see
CERTIFY-BOOK).

     (in-package "ACL2")
     (defstobj st fld)
     (defttag :my-ttag)
     (progn! (update-fld 3 st))

The problem is that the stobj variable st is not known to raw Lisp.
The compilation problem disappears if the last form above is replaced
with the following two forms.

     (include-book "misc/hacker" :dir :system)
     (with-raw-mode (update-fld 3 *the-live-st*))

REDO-FLAT    redo on failure of a progn, encapsulate, or certify-book

When one submits an encapsulate, progn, or certify-book command and
there is a failure, ACL2 restores its logical world as though the
command 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 events under an encapsulate, progn, or certify-book
form 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 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.

Normally, redo-flat will have the desired effect even if you interrupted
a proof (with control-c).  However, redo-flat will not produce the
desired result after an interrupt if you have enabled the debugger using
(set-debugger-enable t),

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, 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.

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.)

Suppose 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 documentation
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.

*Remark 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.

If you want to verify the guards on functions that are built into ACL2,
you will first need to put them into :logic mode.  See
VERIFY-TERMINATION, specifically the "Remark on system functions" in
that documentation.

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.

*Remark on system functions.*  There may be times when you want to apply
verify-termination (and also, perhaps, verify-guards) to functions that
are predefined in ACL2.  It may be necessary in such cases to modify the
system code first.  See
`http://www.cs.utexas.edu/users/moore/acl2/open-architecture/' for a
discussion of the process for contributing updates to the system code
and books with such verify-termination or verify-guards events.  To see
which built-in :program mode functions have already received such
treatment, see directory books/system; for example, use the Unix
utility `grep' to search:

     grep '(verify-' books/system/*.lisp

Note that if fn1 is already in :logic mode, then the verify-termination
call has no effect.  It is generally considered to be redundant, in the
sense that it returns without error; but if the fn1 is a constrained
function (i.e., introduced in the signature of an encapsulate, or by
defchoose), then an error occurs.  This error is intended to highlight
unintended uses of verify-termination; but if you do not want to see an
error in this case, you can write and use your own macro in place of
verify-termination.  The following explanation of the implementation of
verify-termination may help with such a task.

We conclude with a discussion of the use of make-event to implement
verify-termination.  This discussion can be skipped; we include it only
for those who want to create variants of verify-termination, or who are
interested in seeing an application of make-event.

Consider the following proof of nil, which succeeded up through
Version_3.4 of ACL2.

     (encapsulate
      ()
      (defun foo (x y)
        (declare (xargs :mode :program))
        (if (or (zp x) (zp y))
            (list x y)
          (foo (1+ x) (1- y))))
      (local (defun foo (x y)
               (declare (xargs :measure (acl2-count y)))
               (if (or (zp x) (zp y))
                   (list x y)
                 (foo (1+ x) (1- y)))))
      (verify-termination foo))

     (defthm bad-lemma
       (zp x)
       :hints (("Goal" :induct (foo x 1)))
       :rule-classes nil)

How did this work?  In the first pass of the encapsulate, the second
defun of foo promoted foo from :program to :logic mode, with y as the
unique measured variable.  The following call to verify-termination was
then redundant.  However, on the second pass of the encapsulate, the
second (local) definition of foo was skipped, and the
verify-termination event then used the first definition of foo to guess
the measure, based (as with all guesses of measures) on a purely
syntactic criterion.  ACL2 incorrectly chose (acl2-count x) as the
measure, installing x as the unique measured variable, which in turn led
to an unsound induction scheme subsequently used to prove nil (lemma
bad-lemma, above)

Now, verify-termination is a macro whose calls expand to make-event
calls.  So in the first pass above, the verify-termination call
generated a defun event identical to the local defun of foo, which was
correctly identified as redundant.  That expansion was recorded, and on
the second pass of the encapsulate, the expansion was recalled and used
in place of the verify-termination call (that is how make-event works).
So instead of a measure being guessed for the verify-termination call
on the second pass, the same measure was used as was used on the first
pass, and a sound induction scheme was stored.  The attempt to prove nil
(lemma bad-lemma) then failed.

FORWARD-CHAINING-REPORTS    to see reports about the forward chaining process

Debugging forward-chaining rules can be hard because their effects are
not directly visible on the goal.  In this documentation we tell you
how to get reports on the forward chaining activity occurring in your
proof attempts.  This documentation is written in several parts.  The
first part is an introduction for the first-time user of forward
chaining reports.  The next two parts describe how to read reports.
The last part describes how to monitor forward chaining activity only
for selected runes, etc.  We recommend the new user of these reports
read everything!

_A Quick Introduction to Forward Chaining Reports_

Caution: The reporting mechanism maintains some state and if you have
already used forward chaining reporting in a session the directions
below may not work as advertised!  To return to the default forward
chaining reporting state, execute this form at the top level:

     (reset-fc-reporting)

You can get a report about all forward chaining activity in subsequent
proofs by doing:

     (set-fc-criteria t)

Options will be discussed later that allow you to monitor the activity
caused by particular :forward-chaining rules or terms.

Then do a proof that is expected to cause some forward chaining.  In the
proof output you will see lines like this:

     (Forward Chaining on behalf of PREPROCESS-CLAUSE:  (FC-Report 1))

This is the only difference you should see in the proof output.

After the proof attempt has terminated, you can execute:

     (fc-report k)

for any k printed during the immediately preceding proof attempt.  That
will print a much longer report describing the activity that occurred
during the kth use of forward chaining in that proof attempt.

If you want to see these reports in real time (embedded in the proof
output), do this before invoking the prover:

     (set-fc-report-on-the-fly t)

Collecting the data used to generate these reports slows down the
prover.  If you no longer wish to see such reports, do

     (set-fc-criteria nil)

_How To Read FC Reports_

The report printed by (fc-report k) is of the form:

      Forward Chaining Report _k_:
      Caller: _token_
      Clause: (_lit1_ _lit2_ ... _litn_)
      Number of Rounds: _m_
      Contradictionp: _bool_
      Activations: (_act1_ _act2_ ...)

This report means that the _k_th use of forward chaining in the most
recent proof attempt was done on behalf of _token_ (see below).  The
initial context (set of assumptions) consisted of the negations of the
literals listed in the clause shown and the initial candidate trigger
terms are all those appearing in that clause.  This invocation of
forward chaining proceeded to do _m_ rounds of successive extensions of
the initial context and ultimately either reached a contradiction
(_bool_ = T) or returned an extended context (_bool_ = NIL).  Note that
reaching a contradiction from the negations of all the literals in a
clause is "good" because it means the clause is true.  The report
concludes with the final status of all the forward chaining rules fired
during the process.  We explain how to read one of these activation
reports in the next section.

Forward chaining is done on behalf of many proof techniques in the
system.  Each is associated with a _token_.  The main proof technique
that uses forward chaining is SIMPLIFY-CLAUSE.  This is the call of
forward chaining that sets up the context used by the rewriter to
relieve hypotheses during backchaining.  Another common caller of
forward chaining is PREPROCESS-CLAUSE, the first process in the ACL2
waterfall (see HINTS-AND-THE-WATERFALL).  Forward chaining
often proves "near propositional" goals (those depending just on
boolean implications between basic predicates).  Other tokens you may
see include INDUCT, which uses forward chaining to set up a context for
applying :induction rules, and the definitional principle (and related
utilities such as verify-termination and verify-guards) which uses
forward chaining during the construction of both measure conjectures and
guard conjectures.  When used this way, the _token_ is
defun-or-guard-verification.

_How to Read Activation Reports_

The forward chaining report concludes with a list of activation reports.

     Activations: (_act1_ _act2_ ...)

Each _acti_ is of the form:

     (_rune_
      (:TRIGGER _inst-trig_)
      ((:UNIFY-SUBST _subst_)
       (:DISPOSITION _outcome-part1_ _outcome-part2_ _inst-term_))
      ...)

where the ... indicates that the rest of the report consists of more of
those tuples listing a :UNIFY-SUBST and :DISPOSITION.  We call each
tuple a _disposition_ of the activation and each disposition describes
a substitution _subst_ identifying the final instantiation of the rule
and how the activation fared.  Suppose there are _n_ dispositions.  (If
the rule in question contains no free variables, _n_ will be 1.)

This activation report means that during the forward chaining process in
question, the :forward-chaining rune _rune_ was fired due to the
presence in the evolving context of the trigger term _inst-trig_.
(Note that _inst-trig_ is an instantiation of the trigger term of the
named rule.  That is, the variable symbols you see in _inst-trig_ are
those of the clause printed in the forward chaining report.)  The
activation  of _rune_ by _inst-trig_ proceeded to split _n_ ways as
different  choices were made for the free-variables occuring among the
hypotheses.   Each of those _n_ choices gave rise to a different
substitution _subst_,  and each succeeded or failed as described by the
corresponding  :DISPOSITION.

The :DISPOSITION of an activation is described in three parts,
_outcome-part1_, _outcome-part2_, and _inst-term_.  _Outcome-part1_ is
either SUCCESS or BLOCKED, meaning that the instance given by _subst_
either succeeded in the sense that all of its instantiated hypotheses
were found in the context, or failed because some instantiated
hypothesis was not found.

If outcome-part1 is SUCCESS then _inst-term_ is the instantiated
conclusion produced by the rule.  _Outcome-part2_ is either APPROVED or
REJECTED indicating whether the instantiated conclusion was acceptable
to our heuristics designed to prevent looping.  If the conclusion was
approved, it was added to the evolving context; otherwise, it was
discarded as dangerously worse than existing terms.

If outcome-part1 is BLOCKED then outcome-part2 is one of three possible
things: FALSE, in which case _inst-term_ is an instantiated hypothesis
of the rule that is assumed false in the current context,
UNRELIEVED-HYP, in which case _inst-term_ is an instantiated hypothesis
whose truthvalue is not determined by the context, or
UNRELIEVED-HYP-FREE, in which case _inst-term_ is an oddly instantiated
hypothesis whose truthvalue is not determined by the context and which
also contains free variables.  In the last case, the "odd"
instantiation was by the substitution _subst_ but extended so that free
variables in the hypothesis are renamed to start with the prefix
UNBOUND-FREE- to draw your attention to them.

Note:  All of the terms printed in the report are instantiated with the
relevant unifying substitution (possibly extended to bind free
variables).

_Specifying the Tracking Criteria_

During a proof attempt, the forward chaining module stores information
about the activations satisfying certain criteria.  The _criteria_ is a
list of triples.  Each triple consists of a forward chaining rune, an
instantiated trigger term, and an instantiated conclusion to watch for.
However, any or all of the components of such a triple may be t and that
is given special significance.

An activation satisfies a criteria if it satisfies at least one of the
triples.  An activation satisfies a triple if it satisfies all three of
the components.  Every activation satisfies the component t.  An
activation satisfies a rune if the activation describes a firing of the
named rule.  An activation satisfies an instantiated trigger term if
the activation was created by that trigger being present in the
context.  An activation satisfies an instantiated conclusion if the
activation _could_ produce the instantiated conclusion (with the right
choice of any free variables).

Thus, the criteria is interpreted as a disjunction of conjunctions,
making it possible to track a specific set of runes, triggers, and
conclusions.

For example, here is a triple that might appear in the criteria:

     ((:FORWARD-CHAINING ALISTP-FORWARD-TO-TRUE-LISTP)
      t
      t).

This triple would cause every activation of the given rule to be
tracked.  However, the triple

     ((:FORWARD-CHAINING ALISTP-FORWARD-TO-TRUE-LISTP)
      (ALISTP (MAKE-BINDINGS VARS (TOP-N (OP1 INST) (STACK S))))
      t)

would only track activations of that rule fired by the specific term
shown as the second element of the triple.  Futhermore

     (t
      (ALISTP (MAKE-BINDINGS VARS (TOP-N (OP1 INST) (STACK S))))
      t)

would track any forward chaining rule triggered by that term, and

     (t
      t
      (TRUE-LISTP (MAKE-BINDINGS VARS (TOP-N (OP1 INST) (STACK S)))))

would track any rule fired by any trigger that might lead to the
specific term given as the third component above.

Note: The condition on how an activation satisfies an instantiated
conclusion is a little subtle.  Consider the activation of the forward
chaining rule

     (implies (and (symbol-listp x)
                   (equal (len x) (len y)))
              (true-listp (make-bindings x y)))

triggered by (SYMBOL-LISTP VARS) arising in the current context.  This
activation _could_ produce the specific conclusion shown in the last
triple above, if it just happened that (TOP-N (OP1 INST) (STACK S))
were chosen as the binding of the free variable y.  Thus, the
activation of this rule triggered by (SYMBOL-LISTP VARS) satisfies the
last triple above.

Observe that the triple

     (t t t)

is satisfied by every activation of any rule by any trigger term
producing any conclusion.

The function set-fc-criteria sets the criteria describing which
activations are to be tracked.  For example, if you execute:

     (set-fc-criteria ((:FORWARD-CHAINING LEMMA1)
                       t t)
                      ((:FORWARD-CHAINING LEMMA2)
                       (ALISTP (BASIC-MAPPER A B))
                       t)
                      (t t (TRUE-LISTP (DLT D)))),

the system would track all activations of the forward-chaining rule
LEMMA1, plus those activations of forward-chaining rule LEMMA2
triggered by the term given in the second triple, plus any activation of
any rule that might derive (TRUE-LISTP (DLT D)).

Because criteria generally mention variable symbols used in a specific
conjecture, it is probably best to reconsider your criteria every time
you want to track forward chaining.

If the criteria is nil, then nothing is tracked.  Setting the criteria
to nil is the way you turn off tracking and reporting of forward
chaining activity.  You may do this either by (set-fc-criteria) or by
(set-fc-criteria nil).  (Technically the second form is an odd use of
set-fc-criteria, which expects any supplied arguments to be triples; if
the "triple" nil is the only one supplied, we take it to mean that the
entire criteria should be nil.)

To track every forward chaining activation you may set the criteria with
either (set-fc-criteria (t t t)) or use the abbreviation
(set-fc-criteria t).

If, when you read a forward chaining report, you see no mention of an
activation you have in mind, e.g., of a certain rune or deriving a
certain conclusion, and you have set the criteria correctly, then the
activation never happened.  (This is akin to using :brr and :monitor to
monitor the application of a rewrite rule and then seeing no
interactive break.)

For some relevant functions to help you manage criteria and when the
full reports are printed see fc-report, show-fc-criteria,
set-fc-criteria, reset-fc-reporting, and set-fc-report-on-the-fly.

FC-REPORT    to report on the forward chaining activity in the most recent proof

     Example: (fc-report 15)

     General Form: (fc-report k)

where k is the number of some forward chaining report printed in the
most recent event.

See FORWARD-CHAINING-REPORTS for details.

RESET-FC-REPORTING    reset the forward-chaining tracking state to its initial configuration

     Example:  (reset-fc-reporting)

This function erases all forward chaining tracking criteria and sets
the on-the-fly reporting flag to nil.  The next time you set the
criteria (see SET-FC-CRITERIA) the short form of reports, in
which only the caller and the fc-report number is printed, will appear
in your proof logs.

See FORWARD-CHAINING-REPORTS for details.

SET-FC-CRITERIA    to set the tracking criteria for forward chaining reports

     Examples:
     (set-fc-criteria)                 ; shut off all tracking
     (set-fc-criteria nil)

     (set-fc-criteria t)               ; to track all forward chaining
     (set-fc-criteria (t t t))

     (set-fc-criteria
      ((:FORWARD-CHAINING LEMMA1)      ; track all uses of LEMMA1,
        t
        t)
       ((:FORWARD-CHAINING LEMMA2)     ; uses of LEMMA2 triggered
        (ALISTP (BASIC-MAPPER A B))    ; by this specific ALISTP term
        t)
       (t t (TRUE-LISTP (DLT D))))     ; and every rule deriving
                                       ; this TRUE-LISTP term.

     General Forms:
     (set-fc-criteria nil)
     (set-fc-criteria t)
     (set-fc-criteria triple1 triple2 ...)

where each triple is of the form (rune inst-trigger inst-concl).  If
rune is non-t is must be a forward chaining rune.  The other two
components, inst-trigger and inst-concl, if non-t, must be terms.  The
list of all the triples supplied is called the "criteria."  In the form
(set-fc-criteria nil), the criteria used is the empty list of triples.
(Technically, supplying nil as a triple "ought" to be an error, but it
is a more "natural" way to say the list of criteria is empty than to use
the correct form (set-fc-criteria).)  In the form (set-fc-criteria t)
the criteria used is the list containing the single triple (t t t).

This function sets the tracking criteria for forward chaining reporting.
See FORWARD-CHAINING-REPORTS for a general discussion of
tracking and reporting forward chaining activity.

The forward chaining criteria is a list of triples.  Think of it as
representing a disjunction of conjunctions.  The activation of a
:forward-chaining rune by some triggering term in the current context
_satisfies_ the criteria if it satisfies one of the triples.  To
satisfy the triple (rune inst-trigger inst-concl), the activation must
satisfy each component of the triple.  Any t component is always
satisfied.  If rune is non-t it is satisfied if the activation is for
the given rune.  If inst-trigger is non-t, it is satisfied if the
activation is triggered by the given term.  ("Inst-trigger" stands for
"instantiated trigger."  It is not the trigger term of the rule but is
supposed to be an instance of that term that you believe will arise in
some proof attempt you are debugging - an instance you want to "watch"
as it fires the rule.)  If inst-concl is non-t, it is satisfied if the
activation could possibly derive the conclusion given.  (Again,
"inst-concl" stands for "instantiated conclusion" and shows the term in
your problem that you expect to be derived by forward chaining.)

Note that if the criteria is empty, it is never satisfied, so tracking
is turned off.  If the criteria is the singleton list containing just
the triple (t t t), then every activation satisfies it and so all
:forward chaining rules are tracked.

See FORWARD-CHAINING-REPORTS for details.

SET-FC-REPORT-ON-THE-FLY    to determine when forward-chaining reports are printed

     Examples:  (set-fc-report-on-the-fly t)
                (set-fc-report-on-the-fly nil)

If the flag is set to t, forward chaining tracking reports are printed
when forward chaining occurs.  If the flag is set to nil, very short
reports (giving just the caller and the report number) are printed
during forward chaining but you can use fc-report to see the full
report afterwards.

Since nothing is tracked when the criteria is nil, this function also
prints out the current criteria to remind you of what it is.

The flag manipulated by this function does not shut off tracking.  It
only determines whether reports are printed on-the-fly or not.  To shut
off tracking set-fc-criteria.

See FORWARD-CHAINING-REPORTS for details.

SHOW-FC-CRITERIA    print the forward-chaining tracking criteria

     Example:  (show-fc-criteria)

This function prints the list of triples being used to determine what
is tracked during forward chaining.

See FORWARD-CHAINING-REPORTS for details.

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.

PC    print the command described by a command descriptor

     Examples:
     :pc 3    ; print the third command executed
     :pc :max ; print the most recent command
     :pc :x   ; print the most recent command
     :pc fn   ; print the command that introduced fn

See COMMAND-DESCRIPTOR.

Pc takes one argument, a command descriptor, and prints the command
identified by that descriptor.  See COMMAND-DESCRIPTOR.  For
example

     ACL2 !>:pc foo
      LVd     52 (DEFUN FOO (X) X)

Pc always prints a space first, followed by three (possibly blank)
characters ("LVd" above) explained below.  Then pc prints the command
number, a number uniquely identifying the command's position in the
sequence of commands since the beginning of the user's session.
Finally, the command itself is printed.

While pc always prints a space first, some history commands, for
example :pcs and :pe, use the first column of output to delimit a
region of commands or to point to a particular event within a command.

For example, :pcs 52 54 will print something like

     /LVd     52 (DEFUN FOO (X) X)
      LV      53 (DEFUN BAR (X) (CONS X X))
     \        54 (DEFTHM FOO-BAR (EQUAL (CAR (BAR X)) (FOO X)))
               : ...
             127 (DEFUN LATEST (X) X)

Here, the two slash characters in the first column are intended to
suggest a bracket delimiting commands 52 through 54.  The last command
printed by pcs is always the most recent command, i.e., the command at
:here, and is separated from the rest of the display by an elipsis if
some commands are omitted.

Similarly, the :pe command will print a particular event within a
command block and will indicate that event by printing a ">" in the
first column.  The symbol is intended to be an arrow pointing at the
event in question.

For example, :pe true-listp-app might print:

              1 (INCLUDE-BOOK "list-book")
                 \
     >           (DEFTHM TRUE-LISTP-APP
                         (EQUAL (TRUE-LISTP (APP A B)) (TRUE-LISTP B)))

using the arrow to indicate the event itself.  The slash printed to
connect the command, include-book, with the event, defthm, is intended
to suggest a tree branch indicating that the event is inferior to (and
part of) the command.

The mysterious three characters sometimes preceding a command have the
following interpretations.  The first two have to do with the function
symbols introduced by the command and are blank if no symbols were
introduced.

At any time we can classify our function symbols into disjoint sets,
which we will here name with characters.  The "P" functions are those in
:program mode.  The "L" functions are those in :logic mode whose guards
have not been verified.  The "V" functions are those in :logic mode
whose guards have been verified.  You may also see the use of
(lower-case) "v" to indicate functions introduced by encapsulate.  Note
that verify-termination and verify-guards cause function symbols to be
reclassified.  If a command introduces function symbols then the first
mysterious character indicates the class of the symbols at the time of
introduction and the second character indicates the current class of the
symbols (if the current class is different from the introductory class).

Thus, the display

      PLd     52 (DEFUN FOO (X) X)

tells us that command 52 introduced a :program function but that some
command after 52 changed its mode to :logic and that the guards of foo
have not been verified.  That is, foo's termination has been verified
even though it was not verified as part of the command that introduced
foo.  Had a subsequent command verified the guards of foo, the display
would contain a V where the L is.

The display

      P d     52 (DEFUN FOO (X) X)

indicates that foo was introduced in :program mode and still is in that
mode.

The third character indicates the enabled/disabled status of the runes
introduced by the command.  If the status character is blank then all
the runes (if any) introduced are enabled.  If the status character is
"D" then some runes were introduced and they are all disabled.  If the
status character is "d" then at least one, but not all, of the runes
introduced is disabled.  Thus, in the display

      L d     52 (DEFUN FOO (X) X)

we see that some rune introduced by command 52 is disabled.  As noted
in the documentation for rune, a defun command introduces many runes,
e.g., the axiomatic definition rule, (:definition fn), the executable
counterpart rule, (:executable-counterpart fn), and type-prescriptions,
(:type-prescription fn).  The display above does not say which of the
runes based on foo is disabled, but it does tell us one of them is; see
DISABLEDP for how to obtain the disabled runes for a given
function symbol.

PCB    print the command block described by a command descriptor

     Examples:
     :pcb :max ; print the most recent command block
     :pcb :x   ; print the most recent command block
     :pcb fn   ; print the command block that introduced fn
     :pcb 5    ; print the fifth command block

See COMMAND-DESCRIPTOR.

Pcb takes one argument, a command descriptor, and prints the command
block of the command described.  See COMMAND-DESCRIPTOR for
details of command descriptors.  See PC for description of the
format in which commands are displayed.  The command block of a command
consists of the command itself and all of the events it created.  If
the command created a single event and that event is in fact the
command (i.e., if the command typed was just an event such as a defun
or defthm rather than a macro that expanded to some event forms), then
pcb just prints the command.  Pcb sketches command and all of the
events it created, rather than printing them fully.  If you wish to see
just the command, in its entirety, use pc.  If you wish to see one of
the events within the block, in its entirety, use pe.  If you wish to
see the command sketched and all of the events it created, in their
entirety, use pcb!.

PCB!    print in full the command block described by a command descriptor

     Examples:
     :pcb! :max ; print the most recent command block
     :pcb! :x   ; print the most recent command block
     :pcb! fn   ; print the command block that introduced fn
     :pcb! 5    ; print the fifth command block

See COMMAND-DESCRIPTOR.

Pcb! takes one argument, a command descriptor, and prints the command
block of the command described.  Unlike pcb, pcb! prints the event
forms in full; see PCB for details.

PCS    print the sequence of commands between two command descriptors

     Examples:
     :pcs 1 5              ; print commands 1 through 5
     :pcs 5 1              ; same as above
     :pcs :x (:x -3)       ; print the 3 most recently executed commands
     :pcs fn assoc-of-fn   ; print the commands between the one that introduced
                           ; fn and the one that introduced assoc-of-fn

Pcs takes two arguments, both of which are command descriptors, and
prints the commands between them with pc.  The order of the two
descriptors is irrelevant.  See COMMAND-DESCRIPTOR for a
description of command descriptors.  See PC for a description
of the format in which commands are displayed.

PE    print the events named by a logical name

     Example:
     :pe fn   ; sketches the command that introduced fn and
              ; prints in full the event within it that created fn.

See LOGICAL-NAME.

Pe takes one argument, a logical name, and prints in full the event
corresponding to the name.  Pe also sketches the command responsible
for that event if the command is different from the event itself.  See
PC for a description of the format used to display a command.
To remind you that the event is inferior to the command, i.e., you can
only undo the entire command, not just the event, the event is indented
slightly from the command and a slash (meant to suggest a tree branch)
connects them.

If the given logical name corresponds to more than one event, then :pe
will print the above information for every such event.  Here is an
example of such behavior.

     ACL2 !>:pe nth
           -4270  (ENCAPSULATE NIL ...)
                  \
     >V            (VERIFY-TERMINATION NTH)

     Additional events for the logical name NTH:
      PV   -4949  (DEFUN NTH (N L)
                         "Documentation available via :doc"
                         (DECLARE (XARGS :GUARD (AND (INTEGERP N)
                                                     (>= N 0)
                                                     (TRUE-LISTP L))))
                         (IF (ENDP L)
                             NIL
                             (IF (ZP N)
                                 (CAR L)
                                 (NTH (- N 1) (CDR L)))))
     ACL2 !>

If you prefer to see only the formula for the given name, for example
if it is part of a large mutual-recursion, see PF.

PE!    deprecated (see PE)

Please see PE.  :Pe now has the functionality formerly provided
by :pe!.

PF    print the formula corresponding to the given name

     Examples:
     :pf (:definition fn) ; prints the definition of fn as an equality
     :pf fn               ; same as above

     :pf (:rewrite foo)   ; prints the statement of the rewrite rule foo
     :pf foo              ; same as above

pf takes one argument, an event name or a rune, and prints the formula
associated with name.  If the argument is the name of a macro
associated with a function name by macro-aliases-table, then the
function name is used as the argument.

PL    print the rules for the given name or term

     Examples:
     :pl foo     ; prints rules that rewrite some call of foo
     :pl (+ x y) ; prints rules that rewrite (+ x y)

Also see PL2, which restricts output to rules that you specify.

Pl takes one argument, which should be a symbol or a term.  If the
argument is a function symbol (or a macro corresponding to a function;
see MACRO-ALIASES-TABLE), :pl displays the :rewrite,
:definition, and :meta rules that rewrite some term whose top function
symbol is the one specified.  Otherwise, :pl displays the :rewrite and
:definition rules that rewrite the specified term, followed by the
applicable :meta rules.  For :rewrite and :definition rules, :pl also
shows the substitution that, when applied to the left-hand side of the
rule, yields the specified term.  For :meta rules, only those are
displayed that meet two conditions: the application of the metafunction
returns a term different from the input term, and if there is a
hypothesis metafunction then it also returns a term.  (A subtlety: In
the case of extended metafunctions (see
EXTENDED-METAFUNCTIONS), a trivial metafunction context is used for
the application of the metafunction.)

The kinds of rules printed by :pl are :rewrite rules, :definition
rules, and meta rules (not, for example, :forward-chaining rules).  If
you want to see all :clause-processor rules, issue the command
:print-clause-processor-rules, and for trusted clause-processors,
(table trusted-clause-processor-table); see CLAUSE-PROCESSOR and
see DEFINE-TRUSTED-CLAUSE-PROCESSOR.

PL2    print rule(s) for the given form

     Examples:
     :pl2 (+ x y) nil ; prints all rules that rewrite (+ x y)
     :pl2 (+ x y) foo ; prints all rules named foo that rewrite (+ x y)
     :pl2 (+ x y) (:rewrite foo) ; if the rule with rune (:rewrite foo) can
                                 ;   rewrite (+ x y), then print it

Pl2 takes two arguments.  The first is a term.  The second is either
nil or one of the following "rule-ids": a symbol, a rune, or a natural
number.  The result is to print exactly what is printed by applying :pl
to the first argument -- see PL -- except that if the second
argument is not nil then it is used to filter the rewrite rules
printed, as follows.

     If the rule-id is a symbol, then only rewrite rules whose name is
     that symbol will be printed.

     If the rule-id is a rune, then at most rewrite rule will be
     printed: the rule named by that rune (if the rule would be printed
     by :pl).

     If the rule-id is a natural number, k, then the kth rewrite rule
     that would be printed by :pl is the one printed.

Note that as of this writing, meta lemmas are not filtered using the
second argument.

PR    print the rules stored by the event with the given name

     Examples:

     :pr fn ; prints the rules from the definition of fn (including any
            ; :type-prescription rule and :definition rule)

     :pr assoc-append ; if assoc-append is a rewrite rule, prints that rule

Also see PR!, which is similar but works at the command level
instead of at the event level, and see PL, which displays all
rewrite rules for calls of fn, not just those introduced at definition
time.

Pr takes one argument, a logical name, and prints the rules associated
with it.  In each case it prints the rune, the current enabled/disabled
status, and other appropriate fields from the rule.  It may be helpful
to read the documentation for various kinds of rules in order to
understand the information printed by this command.  For example, the
information printed for a linear rule might be:

       Rune:     (:LINEAR ABC)
       Status:   Enabled
       Hyps:     ((CONSP X))
       Concl:    (< (ACL2-COUNT (CAR X)) (ACL2-COUNT X))
       Max-term: (ACL2-COUNT (CAR X))
       Backchain-limit-lst:    (3)

The hyps and concl fields for this rule are fairly self-explanatory,
but it is useful to see LINEAR to learn about maximal terms
(which, as one might guess, are stored under "Max-term").

Currently, this function does not print congruence rules or equivalence
rules.

The expert user might also wish to use find-rules-of-rune.  See
FIND-RULES-OF-RUNE.

PR!    print rules stored by the command with a given command descriptor

     Examples:

     :pr! fn ; prints the rules from the definition of fn (including any
             ; :type-prescription rule and :definition rule), as well as all other
             ; rules created by the command that created by fn (which could be
             ; many rules if, for example, fn was defined by an include-book
             ; command).

     :pr! :max ; prints all the rules stored by the most recent command

Also see PR, which is similar but works at the event level
instead of at the command level.

Pr takes one argument, a command descriptor, and prints the rules
created by the corresponding event.  In each case it prints the rune,
the current enabled/disabled status, and other appropriate fields from
the rule.  See PR for further details.

PUFF    replace a compound command by its immediate subevents

     Example Forms:
     ACL2 !>:puff :max
     ACL2 !>:puff :x
     ACL2 !>:puff 15
     ACL2 !>:puff "book"

     General Form:
     :puff cd

where cd is a command descriptor (see COMMAND-DESCRIPTOR) for a
"puffable" command (see below).  Puff replaces the command at cd by the
immediate subevents of the command, executed as commands.  Puff then
prints, using pcs, the puffed region.

We consider puff to be a sort of hack; it is generally robust and sound,
but that is not guaranteed.  If any existing ACL2 event resulted from
puff, ACL2 considers proofs to have been skipped, and thus certify-book
is disallowed until such events have been undone (see UBT).

A "puffable" command is an encapsulate command, an include-book
command, or any command other than those consisting of a single
primitive event.  For example, since defun is a primitive event, a
defun command is not puffable.  But a macro form that expands into
several defun events is puffable.  The only primitive events that are
puffable are calls of encapsulate or include-book.  A puffable command
contains (interesting) subevents, namely, the events in the body of the
encapsulate, in the file of the book included, or in the command block.

(Obscure exceptions.  (1) An encapsulate command generated by the macro
define-trusted-clause-processor is not puffable.  (2) If a use of
make-event results in local events in the scope of an encapsulate or
include-book event within a command, then an attempt to puff that
command will result in an error, leaving the world unchanged, if any
such local event was necessary to support other events in the command.
(3) An attempt to puff an include-book command may fail for a book that
has been modified, as describe late in this documentation topic.)

The puff command "lifts" the immediate subevents of the indicated
command so that they become commands themselves.  The command puff*
recursively puffs the newly introduced commands.  See PUFF*,
which also gives an example illustrating both puff and puff*.  Puff
undoes the command at cd and replaces it by its immediate subevents.
Thus, in general the length of the history grows when a puff command is
executed.  If puff causes an error (see below), the logical world
remains unchanged from its initial configuration.

The intended use of puff is to allow the user access to the events
"hidden" inside compound commands.  For example, while trying to prove
some theorem, p, about a constrained function, fn, one might find that
the encapsulate, cd, that introduced fn failed to include an important
constraint, q.  Without puff, the only way to proceed is to undo back
through cd, create a suitable encapsulate that proves and exports q as
well as the old constraints, re-execute the new encapsulate, re-execute
the events since cd, and then try p again.  Unfortunately, it may be
hard to prove q and additional events may have to be inserted into the
encapsulate to prove it.  It may also be hard to formulate the "right"
q, i.e., one that is provable in the encapsulate and provides the
appropriate facts for use in the proof of p.

Using puff, the user can erase the encapsulate at cd, replacing it by
the events in its body.  Now the formerly constrained function, fn, is
defined as its witness.  The user can experiment with formulations and
proofs of q suitable for p.  Of course, to get into the ultimately
desired state -- where fn is constrained rather than defined and q is
exported by an encapsulate at cd -- the user must ultimately undo back
to cd and carry out the more tedious program described above.  But by
using puff it is easier to experiment.

Similar applications of puff allow the user of a book to expose the
innards of the book as though they had all be typed as commands.  The
user might then "partially undo" the book, keeping only some of the
events in it.

Puff operates as follows.  First, it determines the list of immediate
subevents of the command indicated by cd.  It causes an error if there
is only one subevent and that subevent is identical to the command --
i.e., if the command at cd is a primitive.  Next, puff undoes back
through the indicated command.  This not only erases the command at cd
but all the commands executed after it.  Finally, puff re-executes the
subevents of (the now erased) cd followed by all the commands that were
executed afterwards.

Observe that the commands executed after cd will generally have higher
command numbers than they did before the puff.  For example, suppose
100 commands have been executed and that :puff 80 is then executed.
Suppose command 80 contains 5 immediate subevents (i.e., is an
encapsulation of five events).  Then, after puffing, command 80 is the
first event of the puffed command, command 81 is the second, and so on;
104 commands appear to have been executed.

When puffing an encapsulate or include-book, the local commands are
executed.  Note that this will replace constrained functions by their
witnesses.

Finally, it is impossible to puff in the presence of include-book
events for certified books that have been altered since they were
included.  (Note that this restriction only applies to include-book,
not to certify-book.)  To be specific, suppose "arith" is a certified
book that has been included in a session.  Suppose that after "arith"
was included, the source file is modified.  (This might happen if the
user of "arith" is not its author and the author happens to be working
on a new version of "arith" during the same time period.)  Now suppose
the user tries to puff the command that included "arith".  The attempt
to obtain the subevents in "arith" will discover that the check sum of
"arith" has changed and an error will be caused.  No change is made in
the logical world.  A similar error is caused if, in this same
situation, the user tries to puff any command that occurred before the
inclusion of "arith"!  That is, puff may cause an error and leave the
world unchanged even if the command puffed is not one involving the
modified book.  This happens because in order to reconstruct the world
after the puffed command, puff must obtain the events in the book and
if the book's source file has changed there is no assurance that the
reconstructed world is the one the user intends.

Warning: We do not detect changes to uncertified books that have been
included and are then puffed or re-included!  The act of including an
uncertified book leaves no trace of the check sum of the book.
Furthermore, the act prints a warning message disclaiming soundness.
In light of this, :puff quietly "re-"executes the current contents of
the book.

PUFF*    replace a compound command by its subevents

     Example Forms:
     ACL2 !>:puff* :max
     ACL2 !>:puff* :x
     ACL2 !>:puff* 15
     ACL2 !>:puff* "book"

     General Form:
     :puff* cd

where cd is a command descriptor (see COMMAND-DESCRIPTOR) for a
"puffable" command.  See PUFF for the definition of "puffable"
and for a description of the basic act of "puffing" a command.  In
particular, see PUFF for a discussion of a sense in which puff,
and hence puff*, should be viewed as a hack.  Puff* is just the
recursive application of puff.  Puff* prints the region puffed, using
pcs.

To puff a command is to replace it by its immediate subevents, each of
which is executed as a command.  To puff* a command is to replace the
command by each of its immediate subevents and then to puff* each of
the puffable commands among the newly introduced ones.

For example, suppose "ab" is a book containing the following

     (in-package "ACL2")
     (include-book "a")
     (include-book "b")

Suppose that book "a" only contained defuns for the functions a1 and a2
and that "b" only contained defuns for b1 and b2.

Now consider an ACL2 state in which only two commands have been
executed, the first being (include-book "ab") and the second being
(include-book "c").  Thus, the relevant part of the display produced by
:pbt 1 would be:

     1 (INCLUDE-BOOK "ab")
     2 (INCLUDE-BOOK "c")

Call this state the "starting state" in this example, because we will
refer to it several times.

Suppose :puff 1 is executed in the starting state.  Then the first
command is replaced by its immediate subevents and :pbt 1 would show:

     1 (INCLUDE-BOOK "a")
     2 (INCLUDE-BOOK "b")
     3 (INCLUDE-BOOK "c")

Contrast this with the execution of :puff* 1 in the starting state.
Puff* would first puff (include-book "ab") to get the state shown
above.  But then it would recursively puff* the puffable commands
introduced by the first puff.  This continues recursively as long as
any puff introduced a puffable command.  The end result of :puff* 1 in
the starting state is

     1 (DEFUN A1 ...)
     2 (DEFUN A2 ...)
     3 (DEFUN B1 ...)
     4 (DEFUN B2 ...)
     5 (INCLUDE-BOOK "c")

Observe that when puff* is done, the originally indicated command,
(include-book "ab"), has been replaced by the corresponding sequence of
primitive events.  Observe also that puffable commands elsewhere in the
history, for example, command 2 in the starting state, are not affected
(except that their command numbers grow as a result of the splicing in
of earlier commands).

RESET-KILL-RING    save memory by resetting and perhaps resizing the kill ring used by oops

By default, ACL2 holds on to old logical worlds when you undo commands
(see UBT), as documented elswhere; see OOPS.  You can
free up memory by deleting those old worlds using reset-kill-ring.

     Examples:
     (reset-kill-ring t state)   ; replace each element of the kill ring by nil
     (reset-kill-ring 2 state)   ; create a new kill ring of '(nil nil)
     (reset-kill-ring 0 state)   ; create a new kill ring that is empty
     (reset-kill-ring nil state) ; just return the length of the kill ring

     General form:
     (reset-kill-ring n state)

where n evaluates either to t, to nil, or to a nonnegative integer (a
natp).  If n evaluates to t, it is treated as the length of the current
kill ring.  If n is nil, then the length k of the current kill ring is
returned as a value triple (mv nil k state).  If n is a natp, then the
kill ring is replaced with a list of n nils.

In particular, use (reset-kill-ring 0 state) to avoid saving any old
logical worlds, at the cost of disabling the effect of the oops command.

U    undo last command, without a query

     Example:
     :u

The keyword command :u is the same as :ubt :max, but with related
queries suppressed appropriately.  :Oops will undo the last :u.  See
UBT, see UBU, see UBT!, and see UBU!.

UBT    undo the commands back through a command descriptor

     Examples:
     :ubt :max      ; undo back through the most recent command
                    ; (which just means undo the most recent command)
     :ubt :x        ; same as :ubt :max
     :u             ; same as :ubt :max with no questions asked
     :ubt fn        ; undo back through the introduction of fn
                    ; (including all the other events in fn's block)
     :ubt 5         ; undo back through the fifth command executed
     :ubt (:max -4) ; undo back through the most recent five commands
     :ubt (:x -4)   ; undo back through the most recent five commands

See COMMAND-DESCRIPTOR.

Ubt takes one argument, a command descriptor, and undoes the commands
from :max (aka :x) through the one described.  See
COMMAND-DESCRIPTOR.  Pbt will print the commands that ubt will undo.
:Oops will undo the undo.  See OOPS.

Ubt can cause errors or queries.  To avoid these, see UBT!.

It is important to remember that a command may create several events.
That is, the command that introduces fn1 may also introduce fn2.
Undoing the command that created either of these will undo them both.
The events created by a command constitute the command's "block" and we
can only undo entire blocks.  Use pcb to print the command block of a
command if you wish to see what will be lost by undoing the command.

Ubt will not undo into "prehistory".  :Ubt 1 will undo all of your
commands.  But :ubt -5 will cause an error, warning you that :ubt
cannot undo system initialization.

See U for how to undo just the latest command, and see
UBU and see UBU! for how to undo back up to, but not
including, the current command.

UBT!    undo commands, without a query or an error

     Example:
     :ubt! :x-4

The keyword command :ubt! is the same as :ubt, but with related queries
suppressed appropriately, and with a guarantee that it is "error-free."
More precisely, the error triple returned by :ubt!  will always have a
first component of nil.  :Oops will undo the last :ubt!.  See
UBT, see UBU, and see U.

UBT-PREHISTORY    undo the commands back through the last reset-prehistory event

This command is only used to eliminate a reset-prehistory event.  If
your most recent reset-prehistory event does not have a flag argument
of t, then :ubt-prehistory undoes all command back through, and
including, that reset-prehistory event.

UBU    undo the commands back up to (not including) a command descriptor

     Examples:
     :ubu :x-3      ; undo the last three commands (same as :ubt :x-2)
     :ubu (:x -3)   ; same as above
     :ubu fn        ; undo back up to, but not including the introduction of fn
                    ; (so fn will continue to be defined)
     :ubu 5         ; undo back up to, but not including, the fifth command
                    ; executed (leaving the first five commands in place)

See COMMAND-DESCRIPTOR.

Ubu takes one argument, a command descriptor, and undoes the commands
from :max (aka :x) up to, but not including, the indicated command.
See COMMAND-DESCRIPTOR.

Ubu can cause errors or queries.  To avoid these, see UBU!.

Also see UBT, which is similar but also undoes the indicated
command.  As for :ubt, :oops will undo the undo (see OOPS) and
ubu will not undo into "prehistory".

See U for how to undo just the latest command, and see
UBT and see UBT! for how to undo back through (that is,
including) the current command.

UBU!    undo commands, without a query or an error

     Example:
     :ubu! :x-4

The keyword command :ubu! is the same as :ubu, but with related queries
suppressed appropriately, and with a guarantee that it is "error-free."
More precisely, the error triple returned by :ubu!  will always have a
first component of nil.  :Oops will undo the last :ubu!.  Also see
UBU, see UBT, and see U.

HONS-AND-MEMOIZATION    hash cons, function memoization, and applicative hash tables

Bob Boyer and Warren Hunt have developed a canonical representation for
ACL2 data objects and a function memoization mechanism to facilitate
reuse of previously computed results.  This facility includes
procedures to read and print ACL2 expressions in such a way that
repetition of some ACL2 objects is eliminated, thereby permitting a
kind of on-the-fly file compression.  The implementation does not alter
the semantics of ACL2 except to add a handful of definitions.

Much of the documentation for this topic is taken from the paper
"Function Memoization and Unique Object Representation for ACL2
Functions" by Robert S. Boyer and Warren A. Hunt, Jr., which has
appeared in the Sixth International Workshop on the ACL2 Theorem Prover
and Its Applications, ACM Digital Library, 2006.

You can build an experimental version of ACL2 that includes hash cons,
function memoization, and fast association lists (applicative hash
tables).  An easy way is to include the following with a make command:

     ACL2_HONS=h

So for example, to make an executable image and also documentation
(which will appear in subdirectories doc/EMACS and doc/HTML):

     make large DOC ACL2_HONS=h

hons-wash, whichever makes sense for the underlying Common Lisp.

of X with T, without duplication.

alist.

alists.

fast-alists.

produces normed, fast alists.

definition for hons-get.

the underlying Hons Space.

and which will be re-normed after any calls to hons-clear.

its arguments are normed.

its arguments are normed.

fast-alists.

tables that govern which ACL2 Objects are considered normed.

from an alist or to copy fast-alists.

that produces a normed result.

the current Hons Space.

objects (CCL Only).

certain sense.

sense of equal

In the implementation of the ACL2 logic, ACL2 data objects are
represented by Common Lisp objects of the same type, and the ACL2
pairing operation is internally implemented by the Common Lisp cons
function.  In Common Lisp, cons is guaranteed to provide a new pair,
distinct from any previously created pair.  We have defined a new ACL2
function HONS that is logically identical to the ACL2 cons function,
but whose implementation usually reuses an existing pair if its
components are identical to the components of an existing pair.  A
record of ACL2 HONS objects is kept, and when an ACL2 function calls
hons ACL2 searches for an existing identical pair before allocating a
new pair; this operation been called "hash consing".

It appears that hash consing was first conceived by A. P. Ershov in
1957, to speed up the recognition of common subexpressions.  Ershov
showed how to collapse trees to minimal DAGs by traversing trees bottom
up, and he used hashing to eliminate the re-evaluation of common
subexpressions.  Later, Eiichi Goto implemented a Lisp system with a
built-in hash consing operation: his h-CONS cells were rewrite
protected and free of duplicate copies, and Goto used this hash consing
operation to facilitate the implementation of a symbolic algebra system
he developed.

Memoizing functions also has a long history.  In 1967, Donald Michie
proposed using memoized functions to improve the performance of machine
learning.  Rote learning was improved by a learning function not
forgetting what it had previously learned; this information was stored
as memoized function values.

The use of hash consing has appeared many times.  For instance, Henry
Baker used hash consing to improve the performance of the well-known
Boyer rewriting benchmark.  Baker used both hash consing and function
memoization to improve the speed of the Takeuchi function, exactly in
the spirit of our implementation, but without the automated,
system-wide integration we report here.

The ACL2 implementation permits memoization of user-defined functions.
During execution a user may enable or disable function memoization on
an individual function basis, may clear memoization tables, and may
even keep a stack of memoization tables.  This facility takes advantage
of our implementation where we keep one copy of each distinct ACL2 data
object.  Due to the functional nature of ACL2, it is sufficient to have
at most one copy of any data structure; thus, a user may arrange to
keep data canonicalized.  This implementation extends to the entire
ACL2 system the benefits enjoyed by BDDs: canonicalization,
memoization, and fast equality check.

We have defined various algorithms using these features, and we have
observed, in some cases, substantial performance increases.  For
instance, we have implemented unordered set intersection and union
operations that operate in time roughly linear in the size of the sets.
Without using arrays, we defined a canonical representation for
Boolean functions using ACL2 objects.  We have investigated the
performance of rewriting and tree consensus algorithms to good effect,
and we believe function memoization offers interesting opportunities to
simplify algorithm definition while simultaneously providing
performance improvements.

We recommend that users focus at first on the logical definitions of
hons and other primitives rather than their underlying Common Lisp
implementations.  Integrated with this memoization system is a
performance monitoring system, which can provide real-time feedback on
the operation and usefulness of hons and function memoization.  For a
more detailed description of these tools, please see the ACL2 2006
workshop paper mentioned above.

The Fibonacci function is a small example that demonstrates the utility
of function memoization.  The following definition exhibits a runtime
that is exponential in its input argument.

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (mbe
        :logic
        (cond ((zp x) 0)
              ((= x 1) 1)
              (t (+ (fib (- x 1)) (fib (- x 2)))))
        :exec
        (if (< x 2)
            x
          (+ (fib (- x 1)) (fib (- x 2))))))

Below we show how the ACL2 time$ utility can measure the time to
execute a call to the fib function (with some editing to avoid noise
from the underlying Common Lisp implementation).  Memoize is actually
an ACL2 macro that expands to a call of the ACL2 function used to
identify a function for memoization; see MEMOIZE.  This
function also accepts a well-formed term that must be true in order for
the system to memoize a call of the memoized function; to ensure that
an instance of the term is safe for evaluation in Common Lisp, a check
is performed that if the guard of the memoized function is satisfied,
then this instance will execute without error.

     ACL2 !>(time$ (fib 40))

     ... took 2,641 milliseconds (2.641 seconds) to run with 8 available
     CPU cores.  During that period, 2,644 milliseconds (2.644 seconds)
     were spent in user mode 0 milliseconds (0.000 seconds) were spent in
     system mode 16 bytes of memory allocated.  102334155 ACL2 !>(memoize
     'fib)

     Summary
     Form:  ( TABLE MEMOIZE-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)

     Summary
     Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
     Rules: NIL
     Warnings:  None
     Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
      FIB
     ACL2 !>(time$ (fib 40))

     ... took 19 milliseconds (0.019 seconds) to run with 8 available CPU
     cores.  During that period, 20 milliseconds (0.020 seconds) were
     spent in user mode 0 milliseconds (0.000 seconds) were spent in
     system mode
      539,088 bytes of memory allocated.
      193 minor page faults, 0 major page faults, 0 swaps.
     102334155
     ACL2 !>(time$ (fib 100))

     ... took 0 milliseconds (0.000 seconds) to run with 8 available CPU
     cores.  During that period, 0 milliseconds (0.000 seconds) were
     spent in user mode 0 milliseconds (0.000 seconds) were spent in
     system mode
      5,760 bytes of memory allocated.
      3 minor page faults, 0 major page faults, 0 swaps.
     354224848179261915075
     ACL2 !>(unmemoize 'fib)

We see that once the function fib is identified as a function for which
function calls should be memoized, the execution times are
substantially reduced.  Finally, we can prevent fib from being further
memoized; in fact, unmemoize erases the previously memoized values.

The implementation of hash consing, memoization, and applicative hash
tables involves several facets: canonical representation of ACL2 data,
function memoization, and the use of Lisp hash tables to improve the
performance of association list operations.  We discuss each of these
in turn, and we mention some subtle interrelationships.  Although it is
not necessary to understand the discussion in this section, it may
permit some users to better use this implementation.  This discussion
may be confusing for some ACL2 users as it makes references to Lisp
implementation features.

The ACL2 system is actually implemented as a Lisp program that is
layered on top of a Common Lisp system implementation.  ACL2 data
constants are implemented with their corresponding counterparts in
Common Lisp; that is, ACL2 cons pairs, strings, characters, numbers,
and symbols are implemented with their specific Common Lisp
counterparts.  This choice permits a number of ACL2 primitive functions
to be implemented with their corresponding Common Lisp functions, but
there are indeed differences.  ACL2 is a logic, and as such, it does
not specify anything to do with physical storage or execution
performance.  When ACL2 is used, the knowledgeable user can write
functions to facilitate the reuse of some previously computed values.

Recall the three mechanisms under discussion: hash consing, function
memoization, and fast association list operations.  The function
memoization mechanism takes advantage of the canonical representation
of data objects provided by the hons operation as does the fast
association list operation mechanism.  Each time hons is invoked, its
arguments are themselves converted, if necessary, to uniquely
represented objects.

The ACL2 universe is recursively closed under the cons pairing
operation and the atoms.  Hash consing (hons) is logically identical to
cons, but a set of tables is used to record each hons pair.  When a
hons pair is requested, the implementation checks, in the current set
of tables, whether the requested pair already exists.  If not, a new
pair is created and a record of that pair is made; otherwise, a
reference to the previously created pair is returned.  Thus, any data
object created with hons has a unique representation, as does every
subcomponent.  We also arrange for strings to have a unique
representation -- only one copy of each different string is kept -- and
when any previously unseen string is an argument to hons, we add the
string to a unique table of strings.  A system-wide benefit of having a
canonical representation for data is that equality comparisons between
any two data objects can be done in constant time.

The definition of hons in no way changes the operation of cons -- hons
creates a cons pair.  When asked to create a hons, the implementation
checks to see if there is a cons with the same car and cdr as the hons
being requested.  Thus, the only difference between the results of a
hons call and a corresponding cons call is a notation in some invisible
(to the ACL2 logic) tables where we record which cons elements are also
hons elements.  Since a hons is nothing but a cons, the operation of
car and cdr is unchanged.  In fact, the implementation is designed so
that at any time it is safe to clear the table identifying which cons
elements are also considered hons elements.

User-defined functions with defined and verified guards can be
memoized.  When a function is memoized, a user-supplied condition
restricts the domain when memoization is attempted.  When the condition
is satisfied, memoization is attempted (assuming that memoization for
the function is presently enabled); otherwise, the function is just
evaluated.  Each memoized function has a hash table that is used to
keep track of a unique list of function arguments paired with their
values.  If appropriate, for each function the corresponding table is
checked to see if a previous call with exactly the same arguments
already exists in the table: if so, then the associated value is
returned; if not, then the function is evaluated and a new key-value
pair is added to the table of memoized values so that some future call
will benefit from the memoization.  With ACL2 user functions
memoization can be dynamically enabled and disabled.  There is an ACL2
function that clears a specific memoization table.  And finally, just
as with the hons table, a stack of these function memoization tables is
maintained; that is, it is possible to memoize a function, use it a
bit, set the memoized values aside, start a new table, use it, and then
return to the original table.

We next discuss the fast lookup operation for association lists.  When
a pair is added to an association list using the functions hons-acons
or hons-acons!, the system also records the key-value pair in an
associated hash table.  As long as a user only used these two functions
when placing key-value pairs on an association list, the key-value
pairs in the corresponding hash table will be synchronized with the
key-value pairs in the association list.  Later, if hons-get is used to
look up a key, then instead of performing a linear search of the
association list we consult the associated hash table.  If a user does
not strictly follow this discipline, then a linear search may be
required.  In some sense, these association lists are much like ACL2
arrays, but without the burden of explicitly naming the arrays.  The
ACL2 array compress1 function is analogous to the functions
hons-shrink-alist and hons-shrink-alist!.  There are user-level ACL2
functions that allow the associated hash tables to be cleared and
removed.

Finally, we would advise anyone who is using CCL in a research
environment to stay plugged into the "trunk" or "bleeding edge" of CCL
development.  This is very easy to do by typing a few commands to a
shell, for example standing above the target directory as follows,
provided one has svn working.

      For linux:

        rm -rf ccl
        svn co http://svn.clozure.com/publicsvn/openmcl/trunk/linuxx8664/ccl

      For an x86 Macintosh running the Darwin OS:

        svn co http://svn.clozure.com/publicsvn/openmcl/trunk/darwinx8664/ccl

      To keep up to date, you may find it sufficient to do:

        cd ccl
        svn update

REFERENCES

Baker, Henry G., The Boyer Benchmark at Warp Speed. ACM Lisp Pointers
V,3 (Jul-Sep 1992), pages 13-14.

Baker, Henry G., A Tachy 'TAK'.  ACM Lisp Pointers Volume 3,
July-September, 1992, pages 22-23.

Robert S. Boyer and Warren A. Hunt, Jr., Function Memoization and
Unique Object Representation for ACL2 Functions, in the Sixth
International Workshop on the ACL2 Theorem Prover and Its Applications,
ACM Digital Library, 2006.

A. P. Ershov.  On Programming of Arithmetic  Operations.  In the
Communications of the ACM, Volume 118, Number 3, August, 1958, pages
427-430.

Eiichi Goto, Monocopy and Associative Algorithms in Extended Lisp,
TR-74-03, University of Toyko, 1974.

Richard P. Gabriel.  Performance and Evaluation of Lisp Systems.  MIT
Press, 1985.

Donald Michie.  Memo functions: a Language Feature with Rote Learning
Properties.  Technical Report MIP-R-29, Department of Artificial
Intelligence, University of Edinburgh, Scotland, 1967.

Donald Michie.  Memo Functions and Machine Learning.  In Nature,
Volumne 218, 1968, pages 19-22.

*UNTROUBLESOME-CHARACTERS*    Some not so weird characters.

*UNTROUBLESOME-CHARACTERS* should not include single quote, whitespace
characters, control characters, or anything else weird for a file name.
Such characters should only be used in file names by experts at
quoting.

CLEAR-HASH-TABLES    Deprecated.  Calls clear-memoize-tables and then hons-clear or
hons-wash, whichever makes sense for the underlying Common Lisp.

CLEAR-MEMOIZE-TABLE    Forget values remembered for the function FN

A logical no-op.  The values memoized for fn are forgotten.

CLEAR-MEMOIZE-TABLES    Forget values remembered for all the memoized functions.

A logical no-op.  All memoized values are forgotten.

Returns NIL.  Invokes CLEAR-MEMOIZE-TABLE for each memoized function.

CONS-SUBTREES    (cons-subtrees x nil) builds a fast alist that associates each subtree
of X with T, without duplication.

FAST-ALIST-FREE    (fast-alist-free alist) throws away the hash table associated with a fast
alist.

Logically, this function is the identity; we leave it enabled and would
think it odd to ever prove a theorem about it.

Under the hood, fast-alist-free removes the hash table associated with
this alist, if one exists.  This effectively converts the alist into an
ordinary alist.

Because there is no automatic mechanism for freeing the hash tables
used in fast alists, to avoid memory leaks you should manually free any
alists that will no longer be used.  You may find fast-alist-summary
useful in tracking down alists that were not properly freed.

It is safe to call fast-alist-free on any argument, including fast
alists that have already been freed and objects which are not alists at
all.

FAST-ALIST-LEN    (fast-alist-len alist) counts the number of unique keys in a fast alist.

Logically this function counts how many elements would remain in the
alist were we to shrink it with hons-shrink-alist.

Good discipline requires that the alist is a fast alist.  Under the
hood, when the alist is a fast alist we can simply call the underlying
Common Lisp function hash-table-count on the associated hash table,
which is very fast and doesn't require us to actually shrink the alist.

FAST-ALIST-SUMMARY    (fast-alist-summary) prints some basic statistics about any current fast
alists.

Logically, fast-alist-summary just returns nil; we leave it enabled and
would think it odd to ever prove a theorem about it.

Under the hood, this function gathers and prints some basic statistics
about the current fast alists.  It may be useful for identifying fast
alists that should have been freed with fast-alist-free

FAST-ALISTS    Alists with hidden hash tables for faster execution.

The implementation of fast alists is, in many ways, similar to that of
ACL2 arrays.  Logically, hons-acons is just like acons, and hons-get is
similar to assoc-equal.  But under the hood, hash tables are associated
with these alists, and, when a certain *discipline* is followed, these
functions execute with hash table speeds.

What is this discipline?  Each hons-acons operation "steals" the hash
table associated with the alist that is being extended.  Because of
this, one must be very conscious of which object is the most recent
extension of an alist and use that extension exclusively.

The only penalty for a failure to keep track of the most recent
extension is a loss of execution speed, not of correctness, and perhaps
the annoyance of some slow-alist-warnings.

Maintaining discipline may require careful passing of a fast alist up
and down through function calls, as with any single threaded object in
an applicative setting, but there is *no syntactic enforcement* that
insists you only use the most recent extension of an alist as there is
for single threaded objects (stobjs).  Also, even with perfectly proper
code, discipline can sometimes be lost due to user interrupts and
aborts.

Performance Notes

The keys of fast alists are always normed.  Why?  In Common Lisp,
equal-based hashing is relatively slow, so to allow the use of
eql-based hash tables, hons-acons and hons-get always hons-copy the keys
involved.

Since alist keys are frequently atoms, this norming activity may often
be so fast that you do not need to think about it.  But if you are
going to use large structures as the keys for your fast alist, this
overhead can be significant, and you may want to ensure that your keys
are normed ahead of time.

There is no automatic mechanism for reclaiming the hash tables that are
associated with alists.  Because of this, to avoid memory leaks, you
should call fast-alist-free to remove the hash table associated with
alists that will no longer be used.

FLUSH-HONS-GET-HASH-TABLE-LINK    Deprecated.  Alias for fast-alist-free

HONS    (hons x y) returns a normed object equal to (cons x y).

In the logic, hons is just cons; we leave it enabled and would think it
odd to ever prove a theorem about it.

Under the hood, hons does whatever is necessary to ensure that its
result is normed.

What might this involve?

Since the car and cdr of any normed cons must be normed, we need to
hons-copy x and y.  This requires little work if x and y are already
normed, but can be expensive if x or y contain large, un-normed cons
structures.

After that, we need to check whether any normed cons equal to (x . y)
already exists.  If so, we return it; otherwise, we need to construct a
new cons for (x . y) and install it as the normed version of (x . y).

Generally speaking, these extra operations make hons much slower than
cons, even when given normed arguments.

HONS-ACONS    (hons-acons key val alist) is the main way to create or extend
fast-alists.

Logically, hons-acons is like acons except that its guard does not
require alistp; we leave it enabled and would think it odd to ever prove
a theorem about it.

Under the hood, two things are done differently.  First, the key is
copied with hons-copy; this lets us use EQL-based hash tables instead of
EQUAL-based hash tables for better performance.  Second, assuming there
is a valid hash table associated with this alist, we destructively
update the hash table by binding key to val.  The hash table will no
longer be associated with alist, but will instead be associated with
the new alist returned by hons-acons.

Hash Table Creation

A new hash table is created by hons-acons whenever alist is an atom.
Unlike ordinary acons, we do not require that alist be nil, and in fact
you may wish to use a non-nil value for one of two reasons.

1.  As a size hint

By default, the new hash table will be given a quite modest default
capacity of 60 elements.  As more elements are added, the table may
need to be resized to accommodate them, and this resizing has some
runtime cost.

When a natural number is used as a fast alist's name, we interpret it
as a size hint.  For example, (hons-acons 'foo 'bar 1000) instructs us
to use 1000 as the initial size for this hash table and binds 'foo to
'bar.  We ignore size hints that request fewer than 60 elements.

Because of hash collisions, hash tables typically need to have a larger
size than the actual number of elements they contain.  The hash tables
for fast alists are told to grow when they reach 70% full.  So, an easy
rule of thumb might be: multiply the expected number of elements you
need by 1.5 to keep your hash tables about 2/3 full.

2.  As an alist name

We also frequently use a symbol for alist, and think of this symbol as
the name of the new alist.  We have found that naming alists can be
valuable for two reasons:

First, the name can be helpful in identifying fast alists that should
have been freed, see fast-alist-summary.

Second, names can sometimes be used to avoid a subtle and insidious
table-stealing phenomenon that occurs when using fast-alists that are
themselves normed; see hons-acons!.

At the moment, there is no way to simultaneously name a fast alist and
also give it a size hint.  We may eventually allow strings to include
embedded name and size components, but for now we have not implemented
this capability.

HONS-ACONS!    (hons-acons! key val alist) is an alternative to ilc[hons-acons that
produces normed, fast alists.

Logically, hons-acons! is like acons except that its guard does not
require alistp; we leave it enabled and would think it odd to ever prove
a theorem about it.

Ordinarily, fast-alists are constructed with hons-acons instead of
hons-acons!.  In such alists, the keys are honsed, but the conses that
make up the "spine" of the alist itself are ordinary conses.  In other
words, it is basically correct to say:

      (hons-acons key val alist) == (cons (cons (hons-copy key) val) alist)

In contrast, when hons-acons! is used, the conses making up the alist
itself are also normed.  That is,

      (hons-acons! key val alist) == (hons (hons key val) alist)

Generally, you *should not use* hons-acons! unless you really know what
you're doing.

Drawback 1.  hons-acons! requires you to hons-copy all of the values
that are being stored in the fast alist.  If you are storing large
values, this may be expensive.

Drawback 2.  It can be more difficult to maintain the proper discipline
when using hons-acons!.  For instance, consider the following:

       (let ((al1 (hons-acons 1 'one (hons-acons 2 'two nil)))
             (al2 (hons-acons 1 'one (hons-acons 2 'two nil))))
          ...)

Here, both al1 and al2 are valid fast alists and they can be extended
independently without any trouble.  But if these alists had instead been
constructed with hons-acons!, then since both al1 and al2 are equal,
normed conses, they will literally be eq and hence will refer to
precisely the same hash table.  In other words, hons-acons! makes it
relatively easy to *inadvertently* steal the hash table associated with
some other fast alist.  This problem can be alleviated somewhat by
uniquely naming alists; see the discussion in hons-acons for details.

Despite these drawbacks, hons-acons! is the only way besides
hons-shrink-alist! to generate a fast alist that is normed.  It is not
adequate to hons-copy a fast alist that was generated by ordinary
hons-acons calls, because this would produce an EQUAL-but-not-EQ object,
and this new object would not be associated with the fast alist's hash
table.

HONS-ASSOC-EQUAL    (hons-assoc-equal key alist) is *not fast*; it serves as the logical
definition for hons-get.

The definition of hons-assoc-equal is similar to that of assoc-equal,
except that (1) it does not require alistp as a guard, and (2) it "skips
over" any non-conses when its alist argument is malformed.

We typically leave hons-get enabled and reason about hons-assoc-equal
instead.  One benefit of this approach is that it avoids certain "false"
discipline warnings that might arise from execution during theorem
proving.

HONS-CLEAR    (hons-clear gc) is a drastic garbage collection mechanism that clears out
the underlying Hons Space.

Logically, hons-clear just returns nil; we leave it enabled and would
think it odd to ever prove a theorem about it.

Under the hood, hons-clear brutally (1) clears all the tables that
govern which conses are normed, then (2) optionally garbage collects,
per the gc argument, then finally (3) re-norms the keys of fast-alists
and persistently normed conses; see hons-copy-persistent.

Note.  The hash tables making up the Hons Space retain their sizes
after being cleared.  If you want to shrink them, see hons-resize.

Note.  CCL users might prefer hons-wash, which is relatively efficient
and allows for the garbage collection of normed conses without
impacting their normed status.

Note.  It is not recommended to interrupt this function.  Doing so may
cause persistently normed conses and fast alist keys to become
un-normed, which might lead to less efficient re-norming and/or
violations of the fast-alist discipline.

HONS-COPY    (hons-copy x) returns a normed object that is equal to X.

In the logic, hons-copy is just the identity function; we leave it
enabled and would think it odd to ever prove a theorem about it.

Under the hood, hons-copy does whatever is necessary to produce a normed
version of X.

What might this involve?

If X is a symbol, character, or number, then it is already normed and
nothing is done.

If X is a string, we check if any normed version of X already exists.
If so, we return the already-normed version; otherwise, we install X as
the normed version for all strings that are equal to X.

If X is a cons, we must determine if there is a normed version of X, or
recursively construct and install one.  Norming large cons trees can
become expensive, but there are a couple of cheap cases.  In
particular, if X is already normed, or if large subtrees of X are
already normed, then not much needs to be done.  The slowest case is
norming some large ACL2 cons structure that has no subtrees which are
already normed.

Note that running hons-copy on an object that was created with cons is
often slower than just using hons directly when constructing the object.

HONS-COPY-PERSISTENT    (hons-copy-persistent x) returns a normed object that is equal to X
and which will be re-normed after any calls to hons-clear.

Logically hons-copy-persistent is the identity; we leave it enabled and
would think it odd to ever prove a theorem about it.

Under the hood, hons-copy-persistent is virtually identical to
hons-copy.

The only difference is that when hons-clear is used, any persistently
normed conses are automatically re-normed, and this re-norming can be
carried out more efficiently than, say, an ordinary hons-copy.

HONS-EQUAL    (hons-equal x y) is a recursive equality check that optimizes when parts of
its arguments are normed.

In the logic, hons-equal is just equal; we leave it enabled and would
think it odd to ever prove a theorem about it.

Under the hood, when hons-equal encounters two arguments that are both
normed, it becomes a mere eql check, and hence avoids the overhead of
recursively checking large cons structures for equality.

Note.  If hons-equal is given arguments that do not contain many normed
objects, it can actually be much slower than equal!  This is because it
checks to see whether its arguments are normed at each recursive step,
and so you are repeatedly paying the price of such checks.  See also
hons-equal-lite, which only checks at the top level whether its
arguments are normed.

HONS-EQUAL-LITE    (hons-equal-lite x y) is a non-recursive equality check that optimizes if
its arguments are normed.

In the logic, hons-equal-lite is just equal; we leave it enabled and
would think it odd to ever prove a theorem about it.

Under the hood, hons-equal-lite checks whether its arguments are normed,
and if so it effectively becomes a eql check.  Otherwise, it immediately
calls equal to determine if its arguments are equal.

The idea here is to strike a useful balance between equal and
hons-equal.  If both arguments happen to be normed, we get to use a very
fast equality comparison.  Otherwise, we just get out of the way and let
equal do its work, without the extra overhead of recursively checking
whether the subtrees of x and y are normed.

HONS-GET    (hons-get key alist) is the efficient lookup operation for
fast-alists.

Logically, hons-get is just an alias for hons-assoc-equal; we typically
leave it enabled and prefer to reason about hons-assoc-equal instead.
One benefit of this approach is that it helps to avoids "false"
discipline warnings that might arise from execution during theorem
proving.

Under the hood, when alist is a fast alist that is associated with a
valid hash table, hons-get first norms key using hons-copy, then
becomes a gethash operation on the hidden hash table.

HONS-RESIZE    (hons-resize ...) can be used to manually adjust the sizes of the hash
tables that govern which ACL2 Objects are considered normed.

General form:

      (hons-resize [:str-ht size]
                   [:nil-ht size]
                   [:cdr-ht size]
                   [:cdr-ht-eql size]
                   [:addr-ht size]
                   [:other-ht size]
                   [:sbits size]
                   [:fal-ht size]
                   [:persist-ht size])

Example:

      (hons-resize :str-ht 100000
                   :addr-ht (expt 2 27))

Logically, hons-resize just returns nil; we leave it enabled and would
think it odd to ever prove a theorem about it.

Under the hood, hons-resize can be used to change the sizes of certain
hash tables in the Hons Space.

All arguments are optional.  The size given to each argument should
either be nil (the default) or a natural number.  A natural number
indicates the newly desired size for the hash table, whereas nil means
"don't resize this table."  Any non-natural argument is regarded as nil.

You may wish to call this function for two reasons.

1.  Improving Performance by Resizing Up

Since the hash tables in the Hons Space automatically grow as new
objects are normed, hons-resize is unnecessary.  But automatic growth
can be slow because it is incremental: a particular hash table might be
grown dozens of times over the course of your application.  Using
hons-resize to pick a more appropriate initial size may help to reduce
this overhead.

2.  Reducing Memory Usage by Resizing Down

Resizing can also be used to shrink the hash tables.  This might
possibly be useful immediately after a hons-clear to free up memory
taken by the hash tables themselves.  (Of course, the tables will grow
again as you create new normed objects.)

Advice for using hons-resize.

Note that hash tables that are already close to the desired size, or
which have too many elements to fit into the desired size, will not
actually be resized.  This makes resizing relatively "safe."

Note that the hons-summary function can be used to see how large and how
full your hash tables are.  This may be useful in deciding what sizes
you want to give to hons-resize.

Note that hons-resize operates by (1) allocating new hash tables, then
(2) copying everything from the old hash table into the new table.
Because of this, for best performance you should ideally call it when
the hash tables involved are minimally populated, i.e., at the start of
your application, or soon after a hons-clear.

HONS-SHRINK-ALIST    (hons-shrink-alist alist ans) can be used to eliminate "shadowed pairs"
from an alist or to copy fast-alists.

Logically, hons-shrink-alist is defined as follows:

      (cond ((atom alist)
             ans)
            ((atom (car alist))
             (hons-shrink-alist (cdr alist) ans))
            ((hons-assoc-equal (car (car alist)) ans)
             (hons-shrink-alist (cdr alist) ans))
            (t
             (hons-shrink-alist (cdr alist) (cons (car alist) ans))))

The alist argument need not be a fast alist, and it is not modified by
the shrink.

Typically ans is set to nil or some other atom.  In this case, shrinking
produces a new, fast alist which is like alist except that (1) any
"malformed," atomic entries have been removed, (2) all "shadowed pairs"
have been removed, and (3) incidentally, the surviving elements have
been reversed.  This can be useful as a way to clean up any unnecessary
bindings in alist, or as a way to obtain a "deep copy" of a fast alist
that can extended independently from the original while maintaining
discipline.

When ans is not an atom, good discipline requires that it is a fast
alist.  In this case, hons-shrink-alist steals the hash table for ans
and extends it with all of the bindings in alist that are not in ans.
From the perspective of hons-assoc-equal, you can think of the
resulting alist as being basically similar to (append ans alist), but
in a different order.

HONS-SHRINK-ALIST!    (hons-shrink-alist! alist ans) is an alternative to hons-shrink-alist
that produces a normed result.

Logically this function is just hons-shrink-alist; we leave it enabled
and would think it odd to ever prove a theorem about it.

Under the hood, this is the same as hons-shrink-alist except that it
uses something like hons-acons! instead of hons-acons.  You generally
*should not use* this function unless you really know what you're doing
and understand the drawbacks discussed in hons-acons!.

HONS-SUMMARY    (hons-summary) prints basic information about the sizes of the tables in
the current Hons Space.

Logically, hons-summary just returns nil; we leave it enabled and would
think it odd to ever prove a theorem about it.

Under the hood, this function gathers and prints some basic information
about the sizes of the tables in the Hons Space.

This information may be useful for deciding if you want to garbage
collect using functions such as hons-clear or hons-wash.  It may also be
useful for determining good initial sizes for the Hons Space hash
tables for your particular computation; see hons-resize.

HONS-WASH    (hons-wash) is like gc$ but can also garbage collect normed
objects (CCL Only).

Logically, hons-wash just returns nil; we leave it enabled and would
think it odd to ever prove a theorem about it.

Under the hood, in CCL, hons-wash runs a garbage collection after taking
special measures to allow normed conses to be collected.  In Lisps
other than CCL, hons-wash does nothing.  This is because the efficient
implementation of hons-wash is specific to the "static honsing" scheme
which requires CCL-specific features.

Why is this function needed?  Ordinarily, it is not possible to garbage
collect any normed conses.  This is because the Hons Space includes
pointers to any normed conses, and hence Lisp's garbage collector
thinks these objects are live.  To correct for this, hons-wash (1)
clears out these pointers, (2) runs a garbage collection, then (3)
re-norms any previously-normed conses which have survived the garbage
collection.

Note.  It is not recommended to interrupt this function.  Doing so may
cause persistently normed conses and fast alist keys to become
un-normed, which might lead to less efficient re-norming and/or
violations of the fast-alist discipline.

NORMED    Normed objects are ACL2 Objects that are "canonical" or "unique" in a
certain sense.

In Common Lisp, we can tell whether an ACL2 object is *normed* or not,
but there is no way for an ordinary ACL2 function to see whether an
object is normed.  Hence, whether or not an object is normed is an
implementation-level concept.

The fundamental property of normed objects is that if A and B are both
normed, then (equal A B) holds if and only if (eql A B) holds.  For
strings and conses, (eql A B) holds only when (eq A B), so any normed
conses or strings are equal precisely when they are eq.  The potential
benefits of having normed objects include:  constant-time equality
comparisons, reduced memory usage, fast association lists, and function
memoization.

Note that in our implementation, all symbols, characters, and numbers
are automatically normed, and whenever a cons is normed its car and cdr
must also be normed.

The Meaning of Normed in Common Lisp.

Recall that the ACL2 Objects are certain "good" Common Lisp symbols,
characters, strings, and numbers, and the conses which can be
recursively formed from these good atoms.

Not all properties of these objects are visible in the ACL2 logic.  An
example of an invisible property is the pointer identity of an object.
For example, suppose we write the following.

      (defconst *x* (cons 1 2))
      (defconst *y* (cons 1 2))

In Common Lisp, cons is guaranteed to provide a new pair that is
distinct from any previously created pair, so we know that *x* and *y*
will be distinct objects and we will be able to tell them apart from
one another using eq.  But this difference is not visible in the ACL2
logic, and no ACL2 function can tell *x* apart from *y*.

The normed-ness of an object is a similarly invisible property.  In
Common Lisp, invisible to ACL2, we maintain a data structure called a
"Hons Space" that records which objects are normed.  So, being normed
is not an intrinsic property of an object, but instead is determined by
whether the object is mentioned in this Hons Space.

Notes about Garbage Collection.

The Hons Space includes tables with pointers to every normed cons and
string.  One consequence of this is that normed objects cannot be
reclaimed by Lisp's ordinary garbage collector, even after they have
become unreachable from the perspective of an ACL2 program.

For CCL users only, hons-wash is a special kind of garbage collection
that allows normed conses to be reclaimed.  For other Lisps, the only
option is to occasionally, manually clear out these Hons Space tables
with hons-clear.

NUMBER-SUBTREES    (number-subtrees x) returns the number of distinct subtrees of X, in the
sense of equal

In the logic, number-subtrees is defined as the length of cons-subtrees.

Under the hood, we first hons-copy X to obtain a normed version, then
count the number of unique conses in X using an EQ hash table.

SLOW-ALIST-WARNING    Warnings issued when fast-alists are used inefficiently.

Obtaining hash-table performance from hons-get requires one to follow a
certain discipline.  If this discipline is violated, you may see a "slow
alist warning".  This warning means that the alist you are extending or
accessing does not have a valid hash table associated with it, and
hence any accesses must be carried out with hons-assoc-equal instead of
gethash.

You can control whether or not you get a warning and, if so, whether or
not a break (an error from which you can continue) ensues.  For
instance:

      (set-slow-alist-action :warning)  ; warn on slow access (default)
      (set-slow-alist-action :break)    ; warn and also call break$
      (set-slow-alist-action nil)       ; do not warn or break

The above forms expand to table events, so they can be embedded in
encapsulates and books, wrapped in local, and so on.

IO    input/output facilities in ACL2

     Example:
     (mv-let
       (channel state)
       (open-input-channel "foo.lisp" :object state)
       (mv-let (eofp obj state)
               (read-object channel state)
               (.
                 .
                  (let ((state (close-input-channel channel state)))
                        (mv final-ans state))..)))

Also see FILE-READING-EXAMPLE.

For advanced ways to control printing, see PRINT-CONTROL.

For a discussion of formatted printing, see FMT.

To control ACL2 abbreviation ("evisceration") of objects before printing
them, see SET-EVISC-TUPLE, see WITHOUT-EVISC, and see
SET-IPRINT.

ACL2 supports input and output facilities equivalent to a subset of
those found in Common Lisp.  ACL2 does not support random access files
or bidirectional streams.  In Common Lisp, input and output are to or
from objects of type stream.  In ACL2, input and output are to or from
objects called "channels," which are actually symbols.  Although a
channel is a symbol, one may think of it intuitively as corresponding
to a Common Lisp stream.  Channels are in one of two ACL2 packages,
"ACL2-INPUT-CHANNEL" and "ACL2-OUTPUT-CHANNEL".  When one "opens" a
file one gets back a channel whose symbol-name is the file name passed
to "open," postfixed with -n, where n is a counter that is incremented
every time an open or close occurs.

There are three channels which are open from the beginning and which
cannot be closed:

       acl2-input-channel::standard-character-input-0
       acl2-input-channel::standard-object-input-0
       acl2-input-channel::standard-character-output-0

All three of these are really Common Lisp's *standard-input* or
*standard-output*, appropriately.

For convenience, three global variables are bound to these rather
tedious channel names:

       *standard-ci*
       *standard-oi*
       *standard-co*

Common Lisp permits one to open a stream for several different kinds of
io, e.g. character or byte.  ACL2 permits an additional type called
"object".  In ACL2 an "io-type" is a keyword, either :character, :byte,
or :object.  When one opens a file, one specifies a type, which
determines the kind of io operations that can be done on the channel
returned.  The types :character and :byte are familiar.  Type :object
is an abstraction not found in Common Lisp.  An :object file is a file
of Lisp objects.  One uses read-object to read from :object files and
print-object$ to print to :object files.  (The reading and printing are
really done with the Common Lisp read and print functions.  For those
familiar with read, we note that the recursive-p argument is nil.)

File-names are strings.  ACL2 does not support the Common Lisp type
pathname.  However, for the file-name argument of the output-related
functions listed below, ACL2 supports a special value, :STRING.  For
this value, the channel connects (by way of a Common Lisp output string
stream) to a string rather than to a file: as characters are written to
the channel they can be retrieved by using get-output-stream-string$.

Here are the names, formals and output descriptions of the ACL2 io
functions.

     Input Functions:
       (open-input-channel (file-name io-type state) (mv channel state))
       (open-input-channel-p (channel io-type state) boolean)
       (close-input-channel (channel state) state)
       (read-char$ (channel state) (mv char/nil state)) ; nil for EOF
       (peek-char$ (channel state) boolean)
       (read-byte$ (channel state) (mv byte/nil state)) ; nil for EOF
       (read-object (channel state) (mv eof-read-flg obj-read state))

     Output Functions:
       (open-output-channel  (file-name io-type state) (mv channel state))
       (open-output-channel! (file-name io-type state) (mv channel state))
       (open-output-channel-p (channel io-type state) boolean)
       (close-output-channel (channel state) state)
       (princ$ (obj channel state) state)
       (write-byte$ (byte channel state) state)
       (print-object$ (obj channel state) state)
       (fms  (string alist channel state evisc-tuple) state)
       (fms! (string alist channel state evisc-tuple) state)
       (fmt  (string alist channel state evisc-tuple) (mv col state))
       (fmt! (string alist channel state evisc-tuple) (mv col state))
       (fmt1 (string alist col channel state evisc-tuple) (mv col state))
       (fmt1! (string alist col channel state evisc-tuple) (mv col state))
       (cw (string arg0 arg1 ... argn) nil)
       (get-output-stream-string$ (channel state) (mv erp string state))

The "formatting" functions are particularly useful; see FMT and
see CW.  In particular, cw prints to a "comment window" and
does not involve the ACL2 state, so many may find it easier to use than
fmt and its variants.  The functions fms!, fmt!, and fmt1! are the same
as their respective functions without the "!," except that the "!"
functions are guaranteed to print forms that can be read back in (at a
slight readability cost).

When one enters ACL2 with (lp), input and output are taken from
*standard-oi* to *standard-co*.  Because these are synonyms for
*standard-input* and *standard-output*, one can drive ACL2 io off of
arbitrary Common Lisp streams, bound to *standard-input* and
*standard-output* before entry to ACL2.

The macro get-output-stream-string$ returns the string accumulated into
the given channel.  By default, a call of this macro closes the supplied
output channel.  However, a third argument is optional (default t), and
if its value is nil then the channel remains open.  The following
example illustrates.

     ACL2 !>
     (mv-let
        (channel state)
        (open-output-channel :string :object state)
        (pprogn (print-object$ 17 channel state)
                (print-object$ '(a b (c d)) channel state)
                (er-let*
                  ((str1 (get-output-stream-string$
                          channel state
                          nil))) ; keep the channel open
                  (pprogn (print-object$ 23 channel state)
                          (print-object$ '((e f)) channel state)
                          (er-let* ; close the channel
                            ((str2 (get-output-stream-string$ channel state)))
                            (value (cons str1 str2)))))))
      ("
     17
     (A B (C D))" . "
     23
     ((E F))")
     ACL2 !>

By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp.  See SET-PRINT-CASE
for how to get ACL2 to print symbols in lower case.

By default, numbers are printed in radix 10 (base 10).  See
SET-PRINT-BASE for how to get ACL2 to print numbers in radix 2, 8, or
16.

Comment for advanced users: Function open-output-channel! is identical
as a function to open-output-channel, except that the former may be
called even during make-event expansion and clause-processor hints, but
requires that there is an active trust tag (see DEFTTAG).

Finally, we note that the distributed book books/misc/file-io.lisp
contains useful file io functions whose definitions illustrate some of
the features described above.

EVISC-TUPLE    control suppression of details when printing

ACL2 output is generally printed in full.  However, ACL2 can be
directed to abbreviate, or "eviscerate", objects before printing them.
To "eviscerate" an object we replace certain substructures within it by
strings that are printed in their stead.  Such replacement is made
relative to a so-called "evisc-tuple", which has four components:
(evisc-tuple print-level print-length alist hiding-cars) is the same as
the value of (list alist print-level print-length hiding-cars), and the
components are used as follows (with priority order as discussed
below).  The alist component is used to replace any substructure
occurring as a key by the corresponding string.  The print-level and
print-length are analogous to Common Lisp variables *print-level* and
*print-length*, respectively, and cause replacement of substructures
deeper than print-level by `#' and those longer than print-length by
`...'.  Finally, any consp x that starts with one of the symbols in
hiding-cars is printed as <hidden>.

The following example illustrates the use of an evisc-tuple that limits
the print-level to 3 -- only three descents into list structures are
permitted before replacing a subexpression by `#' -- and limits the
print-length to 4 -- only the first four elements of any list structure
will be printed before replacing its tail by `...'.

     ACL2 !>(fms "~x0~%"
                 (list (cons #\0 '((a b ((c d)) e f g) u v w x y)))
                 *standard-co*
                 state
                 (evisc-tuple 3 4 nil nil))

     ((A B (#) E ...) U V W ...)
     <state>
     ACL2 !>

Notice that it is impossible to read the printed value back into ACL2,
since there is no way for the ACL2 reader to interpret `#' or `...'.  To
solve this problem, see SET-IPRINT.

In the above example we pass an evisc-tuple explicitly to a printing
function, in this case, fms (see FMT).  But ACL2 also does its
own printing, for example during a proof attempt.  There are global
evisc-tuples that control ACL2's printing; see SET-EVISC-TUPLE
and see WITHOUT-EVISC.

EVISCERATE-HIDE-TERMS    to print (hide ...) as <hidden>

     Example:
     (assign eviscerate-hide-terms t)
     (assign eviscerate-hide-terms nil)

Eviscerate-hide-terms is a state global variable whose value is either
t or nil.  The variable affects how terms are displayed by default (but
not if you have set the term-evisc-tuple to other than its default; see
SET-EVISC-TUPLE).  If t, terms of the form (hide ...)  are
printed as <hidden>.  Otherwise, they are printed normally.

IPRINT    See SET-IPRINT.

IPRINTING    See SET-IPRINT.

OPEN-OUTPUT-CHANNEL!    when trust tags are needed to open output channels

Use this function in place of open-output-channel if you want to open a
channel for output at times this would otherwise be prohibited, for
example during make-event expansion and clause-processor hints.  If
this functionality doesn't quite seem like what you need, take a look
at the definition of open-output-channel! in axioms.lisp, specifically
the binding of state global variable writes-okp.  The following
example, taken from books/hons-archive/hons-archive.lisp, illustrates
the latter approach.

     (defmacro har-zip! (x filename &key sortp)
       "See :doc hons-archive"
       `(mv-let (erp val state)
                (progn!
                 :state-global-bindings
                 ((temp-touchable-vars t set-temp-touchable-vars))
                 (state-global-let*
                  ((writes-okp t))
                  (let ((state (har-zip-fn ,x ,filename ,sortp state)))
                    (mv nil nil state))))
                (declare (ignore erp val))
                state))

The book below illustrates the soundness loophole plugged in ACL2
Version_3.2 related to file writes during book certification.

     ; The following example is adapted (with only very slight changes)
     ; from one written by Peter Dillinger.  It illustrates the prohibition
     ; against writing files enforced by with-output-channel during book
     ; certification (more specifically, during make-event expansion).

     ; This book certifies in ACL2 Version_3.1 before the fix discussed in the
     ; paragraph about it being ``possible to write files during book
     ; certification'' in :DOC NOTE-3-2.  The fix was actually made to ACL2
     ; function open-output-channel.

     ; After the fix, in order for certification to succeed one needs to do
     ; two things.  First, in raw lisp:
     ;   (push :after-writes-okp-fix *features*)
     ; Second, certify with this command:
     ;   (certify-book "writes-okp" 0 nil :ttags (:writes-okp))

     (in-package "ACL2")

     (local
      (defun write-objects-to-channel (obj-lst chan state)
        (declare (xargs :mode :program
                        :stobjs state
                        :guard (true-listp obj-lst)))
        (if (consp obj-lst)
            (pprogn (print-object$ (car obj-lst) chan state)
                    (write-objects-to-channel (cdr obj-lst) chan state)
                    state)
          state)))

     #+after-writes-okp-fix
     (defttag :writes-okp)

     (local
      (defun write-objects-to-file (obj-lst filename state)
        (declare (xargs :mode :program
                        :stobjs state
                        :guard (and (stringp filename)
                                    (true-listp obj-lst))))
        (mv-let (chan state)
                #-after-writes-okp-fix
                (open-output-channel filename :object state)
                #+after-writes-okp-fix
                (open-output-channel! filename :object state)
                (if chan
                    (pprogn (write-objects-to-channel obj-lst chan state)
                            (close-output-channel chan state)
                            (value :done))
                  (er soft 'write-object-to-file
                      "Could not open for writing: ~x0"
                      filename)))))

     (local
      (defconst *nil.lisp*
        '((in-package "ACL2")
          (defthm bad nil :rule-classes nil))))

     (local
      (defconst *nil.cert*
        '((IN-PACKAGE "ACL2")
          "ACL2 Version 3.1"
          :BEGIN-PORTCULLIS-CMDS
          :END-PORTCULLIS-CMDS
          NIL
          (("/home/peterd/test/nil.lisp" "nil" "nil"
            ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134094174))
          62589544
          )))

     (local
      (make-event (er-progn
                   (write-objects-to-file *nil.lisp* "nil.lisp" state)
                   (write-objects-to-file *nil.cert* "nil.cert" state)
                   (value '(value-triple :invisible)))))

     (local (include-book
             "nil" :load-compiled-file nil))

     (defthm bad nil :rule-classes nil)

PRINC$    print a string

Use princ$ to do basic printing of atoms (i.e., other than cons pairs).
In particular, princ$ prints a string without the surrounding
double-quotes and without escaping double-quote characters within the
string.  Note that princ is sensitive to the print-base and print-case;
see SET-PRINT-BASE and see SET-PRINT-CASE.  Princ$
returns state.

     Examples:
     ACL2 !>(princ$ "Howdy ho" (standard-co state) state)
     Howdy ho<state>
     ACL2 !>(pprogn (princ$ "Howdy ho" (standard-co state) state)
                    (newline (standard-co state) state))
     Howdy ho
     <state>
     ACL2 !>(princ$ "ab\"cd" *standard-co* state)
     ab"cd<state>
     ACL2 !>
     ACL2 !>(princ$ 17 *standard-co* state)
     17<state>
     ACL2 !>(set-print-base 16 state)
     <state>
     ACL2 !>(princ$ 17 *standard-co* state)
     11<state>
     ACL2 !>(princ$ 'xyz *standard-co* state)
     XYZ<state>
     ACL2 !>(set-print-case :downcase state)
     <state>
     ACL2 !>(princ$ 'xyz *standard-co* state)
     xyz<state>
     ACL2 !>

See FMT for more sophisticated printing routines, and see
IO for general information about input and output.

PRINT-CONTROL    advanced controls of ACL2 printing

See IO for a summary of printing in ACL2.  Here we document
some advanced ways to control what is printed by ACL2's primary
printing routines.

See SET-PRINT-BASE and see SET-PRINT-CASE for
discussions of the most common ways to control what is printed.
Indeed, these are the only ways to control the behavior of princ$ and
prin1$.

The rest of this topic is for advanced users of ACL2.  We refer to
Common Lisp behavior, as described in any good Common Lisp
documentation.

*Print-control variables*.  Set-print-base and set-print-case assign to
corresponding so-called "state global variables" 'print-base and
'print-case, which can be accessed using the expressions (@ print-base)
and (@ print-case), respectively; see ASSIGN.  Here is a table
showing all print-control variables, their setters, and their defaults.

     print-base          set-print-base          10
     print-case          set-print-case          :upcase
     print-circle        set-print-circle        nil
       [but see remark on print-circle-files, below]
     print-escape        set-print-escape        t
     print-length        set-print-length        nil
     print-level         set-print-level         nil
     print-lines         set-print-lines         nil
     print-pretty        set-print-pretty        nil
     print-radix         set-print-radix         nil
     print-readably      set-print-readably      nil
     print-right-margin  set-print-right-margin  nil

Each ACL2 print-control variable print-xxx can correspond in function to
Common Lisp variable *PRINT-XXX*.  Specifically, the evaluation of forms
(set-print-base t) and (set-print-case t) affects ACL2 printing
functions in much the same way that setting to t Common Lisp variables
*PRINT-BASE* and *PRINT-CASE*, respectively, affects Common Lisp
printing.  The same is true for print-escape, except that this does not
affect princ$ or prin1$, which correspond to Common Lisp functions
princ and prin1: princ treats *PRINT-ESCAPE* as nil while prin1 treats
*PRINT-ESCAPE* as t.  Moreover, all print-control variables not
mentioned in this paragraph are set to their defaults in princ$ and
prin1$, as indicated by ACL2 constant *print-control-defaults*, except
that print-readably is set to nil in princ$.

Fmt and its related functions are sensitive to state globals
'print-base, 'print-case, 'print-escape, and 'print-readably, in
analogy with Common Lisp functions that don't fix *PRINT-ESCAPE* or
*PRINT-READABLY*.  But the fmt functions do not respect settings of
other print-control variables; for example, they act as though
'print-circle is nil.  Since ACL2 output is produced using the same
underlying print routines as the fmt functions, it also is insensitive
to all print-control variables except for the four above.  To control
the print-level and print-length used for producing ACL2 output, see
SET-EVISC-TUPLE.

Print-object$ is sensitive to all of the print-control variables.

Remark on print-circle-files: ACL2 typically binds 'print-circle to t
before writing certificate files, or auxiliary files that are compiled
when make-event forms are present in a book, or files in support of
:comp commands.  This binding allows for structure sharing that can
keep these files from growing large.  However, this behavior is
defeated in GCL (Gnu Common Lisp), because of the small number of
indices n available by default (1024) for the #n= reader macro.  For the
files described above, what actually happens is that 'print-circle is
bound to the value of 'print-circle-files, which by default is t unless
the underlying Lisp is GCL, in which case it is set to nil.  See
ASSIGN for how to set state globals such as 'print-circle-files.  For
example, if you build GCL with a larger number of #n= indices
available, you may wish to restore the print-circle behavior for
certificate files by following these instructions from Camm Maguire:

     This can trivially be revised to any larger constant by editing the
     following line of read.d and recompiling:

     #ifndef SHARP_EQ_CONTEXT_SIZE
     #define SHARP_EQ_CONTEXT_SIZE 500
     #endif

End of Remark.

Evaluate (reset-print-control) to restore all print-control variables to
their original settings, as stored in constant *print-control-defaults*.

(Remark for those using ACL2 built on Gnu Common Lisp (GCL) versions
that are non-ANSI, which as of October 2008 is all GCL versions
recommended for ACL2: Note that Common Lisp variables *PRINT-LINES*,
*PRINT-MISER-WIDTH*, *PRINT-READABLY*, *PRINT-PPRINT-DISPATCH*, and
*PRINT-RIGHT-MARGIN* do not have any effect for such GCL versions.)

RESET-PRINT-CONTROL    See PRINT-CONTROL.

SET-EVISC-TUPLE    control suppression of details when printing

ACL2 output is generally printed in full.  However, ACL2 can be
directed to abbreviate, or "eviscerate", objects before printing them,
though the use of a so-called "evisc-tuple".  See EVISC-TUPLE
for a discussion of evisc-tuples.  The utility set-evisc-tuple modifies
certain global evisc-tuples, as explained below, to affect the extent
to which ACL2 eviscerates objects during printing, for example during
proof output or when printing top-level evaluation results.

     General Form:
     (set-evisc-tuple evisc-tuple ; a legal evisc-tuple, or :DEFAULT
                     :iprint val  ; one of *iprint-actions*
                     :sites sites ; either :ALL, or an element or a subset of the
                                  ;   list (:TERM :LD :TRACE :ABBREV)

where the value of :iprint is passed to set-iprint, :sites :all
abbreviates :sites '(:TERM :LD :TRACE :ABBREV), and other documentation
is provided below.  Note that all arguments are evaluated.

See WITHOUT-EVISC for how to avoid evisceration for ACL2 output.

The following example illustrates an invocation of set-evisc-tuple that
limits the print-level to 3 -- only three descents into list structures
are permitted before eviscerating a subterm -- and limits the
print-length to 4 -- only the first four elements of any list structure
will be printed.

     ACL2 !>(set-evisc-tuple (evisc-tuple 3   ; print-level
                                          4   ; print-length
                                          nil ; alist
                                          nil ; hiding-cars
                                          )
                             :iprint :same ; better yet, T
                             :sites :all)
      (:TERM :LD :TRACE :ABBREV)
     ACL2 !>'((a b ((c d)) e f g) u v w x y)
     ((A B (#) E ...) U V W ...)
     ACL2 !>

We recommend however using :iprint t so that eviscerated terms may be
read back in; see SET-IPRINT.  Indeed, the :iprint argument is
required as a reminder to the user to consider that issue, unless
iprinting has been enabled at least once.  If :sites or a required
:iprint argument is omitted, however, ACL2 will query the user for the
missing arguments rather than causing an error.

ACL2 eviscerates by default only in a few cases, primarily in
informational messages for errors, warnings, and queries (i.e., in the
:EVISC case below).  Users can modify the default behavior by supplying
a suitable argument to set-evisc-tuple.  The argument may be :default,
which denotes the evisceration provided when ACL2 starts up.  Otherwise
that argument is an evisc-tuple, which is either nil (no evisceration)
or as described above.  Moreover, there are four evisc-tuple
"evisceration contexts", each with its own evisceration control.  The
value returned by set-evisc-tuple indicates the evisceration contexts
whose evisc-tuple has been set.  The evisceration contexts are as
follows, all of which use a default value of nil for the hiding-cars.
Accessors are also shown for retrieving the corresponding evisc-tuple.

     o :TERM -- used for printing terms.  The accessor is
     (term-evisc-tuple flg state), where flg is ignored if
     set-evisc-tuple has been called for :term with value other than
     :default, and otherwise (hence initially): a flg of nil indicates
     an evisc-tuple of nil, and otherwise the term-evisc-tuple has a
     print-level of 3 and print-length of 4.

     o :ABBREV -- used for printing informational messages for errors,
     warnings, and queries.  Initially, the alist abbreviates the ACL2
     world, print-level is 5, and print-level is 7.  The accessor is
     (abbrev-evisc-tuple state).

     o :LD -- used by the ACL2 read-eval-print loop.  The accessor is
     (ld-evisc-tuple state).

     o :TRACE -- used for printing trace output.  No accessor is
     available (though in raw Lisp, (trace-evisc-tuple) returns the
     trace-evisc-tuple).

Each context ectx also has an updater, (set-ectx-evisc-tuple val
state), where val is a legal value for set-evisc-tuple as described
above: :default or an evisc-tuple (possibly nil).

Note that the break-rewrite commands and the proof-checker generally do
their printing using the term-evisc-tuple.

SET-FMT-HARD-RIGHT-MARGIN    set the hard right margin for formatted output

Fmt and related functions insert linebreaks when lines get too long.  A
linebreaks is inserted at an aesthetically appropriate points once the
column exceeds the value of state global fmt-soft-right-margin, i.e.,
the result of evaluating (@ fmt-soft-right-margin).  If however the
column exceeds the value of state global fmt-hard-right-margin, i.e.,
the result of evaluating (@ fmt-hard-right-margin), then a linebreak is
soon inserted.  Such a "hard" linebreak follows the insertion of a
backslash (\) character unless fmt!, fms!, or fmt1! is used, or state
global write-for-read is true.

SET-FMT-SOFT-RIGHT-MARGIN    set the soft right margin for formatted output

See SET-FMT-HARD-RIGHT-MARGIN for a discussion of the soft and
hard right margin for formatted output.

SET-IPRINT    control whether abbreviated output can be read back in

When ACL2 pretty-prints large expressions using formatted printing (see
FMT), it may save time and space by printing tokens `#' or
`...' in place of certain subexpressions.  By default this only happens
for a few settings such as error and warning messages; see
SET-EVISC-TUPLE for controlling such elision in general.  The full
expression is unavailable to the user when `#' or `...' is printed, but
that is easily solved by evaluating the form

       (set-iprint t)

to enable a mode called "iprinting".  Then, instead of printing `#' or
`...', ACL2 prints `#@i#' for i = 1,2,3,... -- all in base 10.  ACL2
can read back in such `#@i#' because under the hood, i is associated
with its corresponding elided form.  Thus the term "iprint" can be
viewed as suggesting "interactive print" or "index print".  We also
think of "iprint" as suggesting "i printing", to suggest the printing
of token `#@i#'.  We call i the "iprint index" of that token.

The following example should suffice to illustrate how to recover elided
subexpressions.  (Below this example we provide details that may be of
interest only to advanced users.)  Here we cause an error by defining a
macro of one argument and then calling it with two arguments.  By
default, error messages abbreviate subexpressions deeper than level 5
with `#' and past the 7th element of a list with `...'.  We see this
behavior below.

     ACL2 !>(defmacro foo (x) x)

     Summary
     Form:  ( DEFMACRO FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
      FOO
     ACL2 !>(foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n))

     ACL2 Error in macro expansion:  Wrong number of args in macro expansion
     of (FOO ARG1 (A (B (C (D #))) H I J K L ...)).  (See :DOC set-iprint
     to be able to see elided values in this message.)

     ACL2 !>(set-iprint t)

     ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
     ACL2 !>(foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n))

     ACL2 Error in macro expansion:  Wrong number of args in macro expansion
     of (FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)).

     ACL2 !>(acl2-count '(FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)))
     23
     ACL2 !>

Sometimes you may want to supply the abbreviated form not to compute
with it, as in the acl2-count example just above, but so that you can
see it.  The macro without-evisc eliminates elision during printing.
Below we show two ways to use this utility: first, we use it to print
the elided form, and then, we use it instead on the original input form
to print the entire error message.

     ACL2 !>(without-evisc '(FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)))
     (FOO ARG1
          (A (B (C (D (E (F (G))))))
             H I J K L M N))
     ACL2 !>(without-evisc (foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n)))

     ACL2 Error in macro expansion:  Wrong number of args in macro expansion
     of (FOO ARG1 (A (B (C (D (E (F (G)))))) H I J K L M N)).

     ACL2 !>

The documentation above probably suffices for most users.  For those
who want more details, below we detail all the ways to use the
set-iprint utility.

     Example Forms:
     (set-iprint t)   ; enable iprinting (elision with #@i@)
     (set-iprint nil) ; disable iprinting

     General Form:
     (set-iprint action        ; t, nil, :reset, :reset-enable, or :same
                 :soft-bound s ; initially  1000
                 :hard-bound h ; initially 10000)

where all arguments are optional, but ACL2 queries for action if it is
omitted.   We defer the explanations of :soft-bound and :hard-bound.
The values for action are as follows:

     T -- Enable iprinting.

     NIL -- Disable iprinting.

     :RESET -- Reset iprinting so that when enabled, the first index i
     for which `#@i# is printed will be 1.  Note that all stored
     information for existing iprint indices will be erased.

     :RESET-ENABLE -- Reset iprinting as with :reset, and then enable
     iprinting.

     :SAME -- Make no change to the iprinting state (other than setting
     the :soft-bound and/or :hard-bound if specified, as explained
     below).

Immediately after a top-level form is read, hence before it is
evaluated, a check is made for whether the latest iprint index exceeds
a certain bound, (iprint-soft-bound state) -- 1000, by default.  If so,
then the (iprint-last-index state) is set back to 0.  This soft bound
can be changed to any positive integer k by calling set-iprint with
:soft-bound k, typically (set-iprint :same :soft-bound k)].

The above "soft bound" is applied once for each top-level form, but you
may want finer control by applying a bound after the pretty-printing of
each individual form (since many forms may be pretty-printed between
successive evaluations of top-level forms).  That bound is
(iprint-hard-bound state), and can be set with the :hard-bound argument
in analogy to how :soft-bound is set, as described above.

A "rollover" is the detection that the soft or hard bound has been
exceeded, along with a state update so that the next iprint index will
be 1.  When a rollover occurs, any index beyond the latest iprint index
is no longer available for reading.  At the top level of the ACL2
read-eval-print loop, this works as follows: ACL2 reads the next
top-level form according to the current iprint state, then handles a
rollover if the latest iprint index exceeded the current soft bound.
The following log illustrates a rollover, which follows the description
above.

     ACL2 !>(set-iprint t :soft-bound 3)

     ACL2 Observation in SET-IPRINT:  The soft-bound for iprinting has been
     set to 3.

     ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
     ACL2 !>(set-evisc-tuple (evisc-tuple 2 3 nil nil) :sites :ld)
      (:LD)
     ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
     ((A B C . #@1#) (A B C . #@2#) (A B C . #@3#))
     ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
     ((A B C . #@4#) (A B C . #@5#) (A B C . #@6#))
     ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))
     ((A B C D E F G)
      (A B C D E F G)
      (A B C D E F G))
     ACL2 !>'(1 2 3 4 5)
     (1 2 3 . #@1#)
     ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
     ((A B C . #@2#) (A B C . #@3#) (A B C . #@4#))
     ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))
     ((A B C D E F G)
      (A B C D E F G)
      (A B C D E F G))
     ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))

     ***********************************************
     ************ ABORTING from raw Lisp ***********
     Error:  Out-of-bounds index in #@5#.  See :DOC set-iprint.
     ***********************************************

     If you didn't cause an explicit interrupt (Control-C),
     then the root cause may be call of a :program mode
     function that has the wrong guard specified, or even no
     guard specified (i.e., an implicit guard of t).
     See :DOC guards.

     To enable breaks into the debugger (also see :DOC acl2-customization):
     (SET-DEBUGGER-ENABLE T)
     ACL2 !>

We conclude by mentioning two cases where iprinting and evisc-tuples are
ignored.  (1) This is typically the case when printing results in raw
Lisp outside the ACL2 loop.  To use iprinting and evisc-tuples in raw
Lisp, use raw-mode; see SET-RAW-MODE.  In raw-mode, results
that are ACL2 objects will be printed in the same way that ACL2 would
print those results if not in raw-mode.  (2) Iprinting and evisc-tuples
are ignored by print-object$, which however is sensitive to many
settings that do not affect formatted (fmt etc.) printing; see
PRINT-CONTROL.

The reader interested in design and implementation issues considered
during the addition of iprinting to ACL2 is invited to read the paper
"Abbreviated Output for Input in ACL2: An Implementation Case Study";
see the proceedings of ACL2 Workshop 2009,
`http://www.cs.utexas.edu/users/sandip/acl2-09/'.

SET-PRINT-BASE    control radix in which number are printed

By default, integers and ratios are printed in base 10.  ACL2 also
supports printing in radix 2, 8, or 16 by calling set-print-base with
the desired radix (base).

       (set-print-base 10 state) ; Default printing
       (set-print-base 16 state) ; Print integers and ratios in hex, e.g., #x3A

Also see PRINT-CONTROL for other user-settable print controls.

Note: ACL2 events and some other top-level commands (for example, thm,
verify, and history commands such as :pe and :pbt) set the print base
to 10 during their evaluation.  So set-print-base has no effect while
these forms are being processed.

SET-PRINT-CASE    control whether symbols are printed in upper case or in lower case

By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp.  As with Common Lisp, ACL2
supports printing in a "downcase" mode, where symbols are printed in
lower case.  Many printing functions (some details below) print
characters in lower case for a symbol when the ACL2 state global
variable print-case has value :downcase and vertical bars are not
necessary for printing that symbol.  (Thus, this state global functions
in complete analogy to the Common Lisp global *print-case*.)  The value
print-case is returned by (print-case), and may be set using the
function set-print-case as follows.

       (set-print-case :upcase   state) ; Default printing
       (set-print-case :downcase state) ; Print symbols in lower case when
                                        ; vertical bars are not required

The ACL2 user can expect that the :downcase setting will have an effect
for formatted output (see FMT and see FMS) when the
directives are ~p, ~P, ~q, or ~Q, for built-in functions princ$ and
prin1$, and the ppr family of functions, and _not_ for built-in
function print-object$.  For other printing functions, the effect of
:downcase is unspecified.

Also see PRINT-CONTROL for other user-settable print controls.

SET-PRINT-CIRCLE    See PRINT-CONTROL.

SET-PRINT-ESCAPE    See PRINT-CONTROL.

SET-PRINT-LENGTH    See PRINT-CONTROL.

SET-PRINT-LEVEL    See PRINT-CONTROL.

SET-PRINT-LINES    See PRINT-CONTROL.

SET-PRINT-RADIX    See PRINT-CONTROL.

SET-PRINT-READABLY    See PRINT-CONTROL.

SET-PRINT-RIGHT-MARGIN    See PRINT-CONTROL.

WITHOUT-EVISC    print output in full

     General Form:
     (without-evisc form)

where form is any expression to evaluate.  The effect is to evaluate
form as though the without-evisc wrapper were absent, except that
expressions are printed in full for the ensuing output, regardless of
the current evisc-tuples (see SET-EVISC-TUPLE).  See
SET-IPRINT for an example.

More precisely, without-evisc binds the term-evisc-tuple,
ld-evisc-tuple, and abbrev-evisc-tuple to nil (see
SET-EVISC-TUPLE).  It does not modify the trace evisc-tuple, so trace
output is not modified by without-evisc.  Also note that calls of
printing functions such as fmt that include explicit evisc-tuples will
not have those evisc-tuples overridden.  The following example
illustrates this point.

     ACL2 !>(without-evisc
             (fms "~x0~%"
                  (list (cons #0 '((a b ((c d)) e f g) u v w x y)))
                  *standard-co*
                  state
                  (evisc-tuple 2 3 nil nil)))

     ((A B # ...) U V ...)
     <state>
     ACL2 !>

We conclude with two remarks.  (1) A call of without-evisc on expression
exp actually invokes a specialized call of ld on a one-element list
containing exp, which prints the value returned by evaluation of exp
but actually returns the useless value (mv nil :invisible state).  So do
not use without-evisc in programs; just use it at the top level of the
ACL2 read-eval-print loop, or at least the top level of ld.  (2) Even
when using without-evisc, if the ACL2 logical world is part of the value
returned, it will be printed in abbreviated form because the ACL2
read-eval-print loop always arranges for this to be the case,
regardless of the ld-evisc-tuple.  For example:

     ACL2 !>(without-evisc (w state))
     <world>
     ACL2 !>

An alternative to the use of without-evisc is to explore large objects
using the ACL2 function (walkabout object state).  Some brief
documentation is printed when you enter an interactive loop upon
evaluating a call of walkabout.  We may add documentation for walkabout
if that is requested.

MISCELLANEOUS    a miscellany of documented functions and concepts
               (often cited in more accessible documentation)

Perhaps as the system matures this section will become more structured.

A!    to return to the top-level of ACL2's command loop

When (a!) is evaluated inside of ACL2's command loop, the current
computation is aborted and control returns to the top of the command
loop, exactly as though the user had interrupted and aborted the current
computation.  (Note: Versions of ACL2 up to Version_3.4 provided `#.'
for this purpose, but no longer; see SHARP-DOT-READER.)

If you are at an ACL2 prompt (as opposed to a raw Lisp break), then you
may type :a! in place of (a!); see KEYWORD-COMMANDS.

For a related feature that only pops up one level, see P!.

Logically speaking, (a!) = nil.  But imagine that it is defined in such
a way that it causes a stack overflow or other resource exhaustion when
called.

ABORT!    to return to the top-level of ACL2's command loop

This is an alias for a!; see A!.  For a related feature that
only pops up one level, see P!.

ACKNOWLEDGMENTS    some contributors to the well-being of ACL2

The development of ACL2 was initially made possible by funding from the
U. S. Department of Defense, including ARPA and ONR.  We thank all the
organizations that have contributed support, including the following (in
alphabetical order).

     o AMD, for providing significant time over several years for Matt
     Kaufmann to carry out ACL2 research, support, and development
     o Computational Logic, Inc. and its president, Don Good, where the
     first eight years of ACL2 development occurred
     o Centaur Technology
     o DARPA
     o Digital Equipment Corporation
     o EDS, which provided some time for Matt Kaufmann's ACL2 work
     1998-1999
     o ForrestHunt and, more generally, Warren A. Hunt, Jr. (see below)
     o IBM
     o NSF
     o ONR
     o Rockwell Collins
     o SRC
     o Sun Microsystems
     o University of Texas at Austin (in particular support to J Moore
     through the Admiral B. R.  Inman Chair of Computing Theory)

We are especially grateful to Warren A. Hunt, Jr. for his unrivaled
efforts in securing support for the entire ACL2 research group at both
Computational Logic, Inc., and the University of Texas at Austin.
Without his efforts, we would have spent less time working on the
system and fewer students would have been funded to apply it.

ACL2 was started in August, 1989 by Boyer and Moore working together.
They co-authored the first versions of axioms.lisp and basis.lisp, with
Boyer taking the lead in the formalization of "state" and the most
primitive io functions.  Boyer also had a significant hand in the
development of the early versions of the files interface-raw.lisp and
translate.lisp.  For several years, Moore alone was responsible for
developing the ACL2 system code, though he consulted often with both
Boyer and Kaufmann.  In August, 1993, Kaufmann became jointly
responsible with Moore for developing the system.  Boyer has continued
to provide valuable consulting on an informal basis.

Bishop Brock was the heaviest early user of ACL2, and provided many
suggestions for improvements.  In particular, the :cases and :restrict
hints were his idea; he developed an early version of congruence-based
reasoning for Nqthm; and he helped in the development of some early
books about arithmetic.  In a demonstration of his courage and faith in
us, he pushed for Computational Logic, Inc., to agree to the Motorola
CAP contract - which required formalizing a commercial DSP in the
untested ACL2 - and moved to Scottsdale, AZ, to do the work with the
Motorola design team.  His demonstration of ACL2's utility was an
inspiration, even to those of us designing ACL2.

John Cowles also helped in the development of some early books about
arithmetic, and also provided valuable feedback and bug reports.

Other early users of ACL2 at Computational Logic, Inc. helped influence
its development.  In particular, Warren Hunt helped with the port to
Macintosh Common Lisp, and Art Flatau and Mike Smith provided useful
general feedback.

Mike Smith helped develop the Emacs portion of the implementation of
proof trees.

Bill Schelter made some enhancements to akcl (now gcl) that helped to
enhance ACL2 performance in that Common Lisp implementation, and more
generally, responded helpfully to our bug reports.  Camm Maguire has
since provided wonderful gcl support, and has created a Debian package
for ACL2 built on GCL.  We are also grateful to developers of other
Common Lisp implementations.

Kent Pitman helped in our interaction with the ANSI Common Lisp
standardization committee, X3J13.

John Cowles helped with the port to Windows (98) by answering questions
and running tests.

Ruben Gamboa created a modification of ACL2 to allow reasoning about
the real numbers using non-standard analysis.  His work has been
incorporated into the ACL2 distribution; see REAL.

Rob Sumners has made numerous useful suggestions.  In particular, he has
designed and implemented improvements for stobjs and been key in our
development of locally-bound stobjs; see NOTE-2-6.

Robert Krug has designed and implemented many changes in the vicinity
of the linear arithmetic package and its connection to type-set and
rewrite.  He was also instrumental in the development of
extended-metafunctions.

Pete Manolios has made numerous useful suggestions.  In particular, Pete
helped us to organize the first workshop and was a wonderful equal
partner with the two of us (Kaufmann and Moore) in producing the books
that arose from that workshop.  Pete and his student, Daron Vroon,
provided the current implementation of ordinals.

Jared Davis and Sol Swords have our gratitude for starting the
acl2-books repository, `http://acl2-books.googlecode.com/'.

We thank David L. Rager for contributing an initial version of the
support for parallelism in an experimental extension of ACL2.

Bob Boyer and Warren A. Hunt, Jr. developed a canonical representation
for ACL2 data objects and a function memoization mechanism to
facilitate reuse of previously computed results.  We thank them for
their extensive efforts for the corresponding experimental (as of 2008
and 2009) extension of ACL2; see HONS-AND-MEMOIZATION.

We also thank the contributors to the ACL2 workshops for some suggested
improvements and for the extensive collection of publicly distributed
benchmark problems.  And we thank participants at the ACL2 seminar at
the University of Texas for useful feedback.  More generally, we thank
the ACL2 community for feedback, contributed books, and their interest
in the ACL2 project.

_Regarding the documentation:_

     Bill Young wrote significant portions of the original acl2-tutorial
     section of the ACL2 documentation, including what is now called
     alternative-introduction.  This was an especially important task
     in the early years when there was no guide for how to use ACL2 and
     we are very grateful.  He, Bishop Brock, Rich Cohen, and Noah
     Friedman read over considerable amounts of the documentation, and
     made many useful comments.  Others, particularly Bill Bevier and
     John Cowles, have also made useful comments on the documentation.

     Art Flatau helped develop the ACL2 markup language and translators
     from that language to Texinfo and HTML.  Michael "Bogo" Bogomolny
     created a search engine, beginning with Version 2.6, and for that
     purpose modified the HTML translator to create one file per topic
     (a good idea in any case).

     Laura Lawless provided many hours of help in marking up
     appropriate parts of the documentation in typewriter font.

     Noah Friedman developed an Emacs tool that helped us insert
     "invisible links" into the documentation, which improve the
     usability of that documentation under HTML readers such as Mosaic.

     Richard Stallman contributed a texinfo patch, to be found in the
     file doc/texinfo.tex.

ACL2-COUNT    a commonly used measure for justifying recursion

(Acl2-count x) returns a nonnegative integer that indicates the "size"
of its argument x.

All characters and symbols have acl2-count 0.  The acl2-count of a
string is the number of characters in it, i.e., its length.  The
acl2-count of a cons is one greater than the sum of the acl2-counts of
the car and cdr.  The acl2-count of an integer is its absolute value.
The acl2-count of a rational is the sum of the acl2-counts of the
numerator and denominator.  The acl2-count of a complex rational is one
greater than the sum of the acl2-counts of the real and imaginary parts.

ACL2S    See ACL2-SEDAN.

APROPOS    searching the documentation online

The :docs command allows you to search the documentation at the
terminal.  See DOCS.

ARRAYS    an introduction to ACL2 arrays

Below we begin a detailed presentation of ACL2 arrays.  ACL2's
single-threaded objects (see STOBJ) provide a similar
functionality that is generally more efficient when there are updates
(writes), but is also more restrictive.

See ARRAYS-EXAMPLE for a brief introduction illustrating the use
of ACL2 arrays.

ACL2 provides relatively efficient 1- and 2-dimensional arrays.  Arrays
are awkward to provide efficiently in an applicative language because
the programmer rightly expects to be able to "modify" an array object
with the effect of changing the behavior of the element accessing
function on that object.  This, of course, does not make any sense in
an applicative setting.  The element accessing function is, after all,
a function, and its behavior on a given object is immutable.  To
"modify" an array object in an applicative setting we must actually
produce a new array object.  Arranging for this to be done efficiently
is a challenge to the implementors of the language.  In addition, the
programmer accustomed to the von Neumann view of arrays must learn how
to use immutable applicative arrays efficiently.

In this note we explain 1-dimensional arrays.  In particular, we
explain briefly how to create, access, and "modify" them, how they are
implemented, and how to program with them.  2-dimensional arrays are
dealt with by analogy.

_The Logical Description of ACL2 Arrays_

An ACL2 1-dimensional array is an object that associates arbitrary
objects with certain integers, called "indices." Every array has a
dimension, dim, which is a positive integer.  The indices of an array
are the consecutive integers from 0 through dim-1.  To obtain the
object associated with the index i in an array a, one uses (aref1 name
a i).  Name is a symbol that is irrelevant to the semantics of aref1
but affects the speed with which it computes.  We will talk more about
array "names" later.  To produce a new array object that is like a but
which associates val with index i, one uses (aset1 name a i val).

An ACL2 1-dimensional array is actually an alist.  There is no special
ACL2 function for creating arrays; they are generally built with the
standard list processing functions list and cons.  However, there is a
special ACL2 function, called compress1, for speeding up access to the
elements of such an alist.  We discuss compress1 later.

One element of the alist must be the "header" of the array.  The header
of a 1-dimensional array with dimension dim is of the form:

     (:HEADER :DIMENSIONS (dim)
              :MAXIMUM-LENGTH max
              :DEFAULT obj ; optional
              :NAME name   ; optional
              :ORDER order ; optional values are < (the default), >, or :none/nil
              ).

Obj may be any object and is called the "default value" of the array.
Max must be an integer greater than dim.  Name must be a symbol.  The
:default and :name entries are optional; if :default is omitted, the
default value is nil.  The function header, when given a name and a 1-
or 2-dimensional array, returns the header of the array.  The functions
dimensions, maximum-length, and default are similar and return the
corresponding fields of the header of the array.  The role of the
:dimensions field is obvious: it specifies the legal indices into the
array.  The roles played by the :maximum-length and :default fields are
described below.

Aside from the header, the other elements of the alist must each be of
the form (i . val), where i is an integer and 0 <= i < dim, and val is
an arbitrary object.

The :order field of the header is ignored for 2-dimensional arrays.  For
1-dimensional arrays, it specifies the order of keys (i, above) when the
array is compressed as with compress1, as described below.  An :order
of :none or nil specifies no reordering of the alist by compress1, and
an order of > specifies reordering by compress1 so that keys are in
descending order.  Otherwise, the alist is reordered by compress1 so
that keys are in ascending order.

(Aref1 name a i) is guarded so that name must be a symbol, a must be an
array and i must be an index into a.  The value of (aref1 name a i) is
either (cdr (assoc i a)) or else is the default value of a, depending
on whether there is a pair in a whose car is i.  Note that name is
irrelevant to the value of an aref1 expression.  You might :pe aref1 to
see how simple the definition is.

(Aset1 name a i val) is guarded analogously to the aref1 expression.
The value of the aset1 expression is essentially (cons (cons i val) a).
Again, name is irrelevant.  Note (aset1 name a i val) is an array, a',
with the property that (aref1 name a' i) is val and, except for index
i, all other indices into a' produce the same value as in a.  Note also
that if a is viewed as an alist (which it is) the pair "binding" i to
its old value is in a' but "covered up" by the new pair.  Thus, the
length of an array grows by one when aset1 is done.

Because aset1 covers old values with new ones, an array produced by a
sequence of aset1 calls may have many irrelevant pairs in it.  The
function compress1 can remove these irrelevant pairs.  Thus, (compress1
name a) returns an array that is equivalent (vis-a-vis aref1) to a but
which may be shorter.  For technical reasons, the alist returned by
compress1 may also list the pairs in a different order than listed in a.

To prevent arrays from growing excessively long due to repeated aset1
operations, aset1 actually calls compress1 on the new alist whenever
the length of the new alist exceeds the :maximum-length entry, max, in
the header of the array.  See the definition of aset1 (for example by
using :pe).  This is primarily just a mechanism for freeing up cons
space consumed while doing aset1 operations.  Note however that this
compress1 call is replaced by a hard error if the header specifies an
:order of :none or nil.

This completes the logical description of 1-dimensional arrays.
2-dimensional arrays are analogous.  The :dimensions entry of the
header of a 2-dimensional array should be (dim1 dim2).  A pair of
indices, i and j, is legal iff 0 <= i < dim1 and 0 <= j < dim2.  The
:maximum-length must be greater than dim1*dim2.  Aref2, aset2, and
compress2 are like their counterparts but take an additional index
argument.  Finally, the pairs in a 2-dimensional array are of the form
((i . j) . val).

_The Implementation of ACL2 Arrays_

Very informally speaking, the function compress1 "creates" an ACL2
array that provides fast access, while the function aref1 "maintains"
fast access.  We now describe this informal idea more carefully.

Aref1 is essentially assoc.  If aref1 were implemented naively the time
taken to access an array element would be linear in the dimension of
the array and the number of "assignments" to it (the number of aset1
calls done to create the array from the initial alist).  This is
intolerable; arrays are "supposed" to provide constant-time access and
change.

The apparently irrelevant names associated with ACL2 arrays allow us to
provide constant-time access and change when arrays are used in
"conventional" ways.  The implementation of arrays makes it clear what
we mean by "conventional."

Recall that array names are symbols.  Behind the scenes, ACL2
associates two objects with each ACL2 array name.  The first object is
called the "semantic value" of the name and is an alist.  The second
object is called the "raw lisp array" and is a Common Lisp array.

When (compress1 name alist) builds a new alist, a', it sets the
semantic value of name to that new alist.  Furthermore, it creates a
Common Lisp array and writes into it all of the index/value pairs of
a', initializing unassigned indices with the default value.  This array
becomes the raw lisp array of name.  Compress1 then returns a', the
semantic value, as its result, as required by the definition of
compress1.

When (aref1 name a i) is invoked, aref1 first determines whether the
semantic value of name is a (i.e., is eq to the alist a).  If so, aref1
can determine the ith element of a by invoking Common Lisp's aref
function on the raw lisp array associated with name.  Note that no
linear search of the alist a is required; the operation is done in
constant time and involves retrieval of two global variables, an eq
test and jump, and a raw lisp array access.  In fact, an ACL2 array
access of this sort is about 5 times slower than a C array access.  On
the other hand, if name has no semantic value or if it is different
from a, then aref1 determines the answer by linear search of a as
suggested by the assoc-like definition of aref1.  Thus, aref1 always
returns the axiomatically specified result.  It returns in constant
time if the array being accessed is the current semantic value of the
name used.  The ramifications of this are discussed after we deal with
aset1.

When (aset1 name a i val) is invoked, aset1 does two conses to create
the new array.  Call that array a'.  It will be returned as the answer.
(In this discussion we ignore the case in which aset1 does a
compress1.)  However, before returning, aset1 determines if name's
semantic value is a.  If so, it makes the new semantic value of name be
a' and it smashes the raw lisp array of name with val at index i,
before returning a' as the result.  Thus, after doing an aset1 and
obtaining a new semantic value a', all aref1s on that new array will be
fast.  Any aref1s on the old semantic value, a, will be slow.

To understand the performance implications of this design, consider the
chronological sequence in which ACL2 (Common Lisp) evaluates
expressions:  basically inner-most first, left-to-right, call-by-value.
An array use, such as (aref1 name a i), is "fast" (constant-time) if
the alist supplied, a, is the value returned by the most recently
executed compress1 or aset1 on the name supplied.  In the functional
expression of "conventional" array processing, all uses of an array are
fast.

The :name field of the header of an array is completely irrelevant.
Our convention is to store in that field the symbol we mean to use as
the name of the raw lisp array.  But no ACL2 function inspects :name
and its primary value is that it allows the user, by inspecting the
semantic value of the array -- the alist -- to recall the name of the
raw array that probably holds that value.  We say "probably" since
there is no enforcement that the alist was compressed under the name in
the header or that all asets used that name.  Such enforcement would be
inefficient.

_Some Programming Examples_

In the following examples we will use ACL2 "global variables" to hold
several arrays.  See @, and see ASSIGN.

Let the state global variable a be the 1-dimensional compressed array
of dimension 5 constructed below.

     ACL2 !>(assign a (compress1 'demo
                                 '((:header :dimensions (5)
                                            :maximum-length 15
                                            :default uninitialized
                                            :name demo)
                                   (0 . zero))))

Then (aref1 'demo (@ a) 0) is zero and (aref1 'demo (@ a) 1) is
uninitialized.

Now execute

     ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))

Then (aref1 'demo (@ b) 0) is zero and (aref1 'demo (@ b) 1) is one.

All of the aref1s done so far have been "fast."

Note that we now have two array objects, one in the global variable a
and one in the global variable b.  B was obtained by assigning to a.
That assignment does not affect the alist a because this is an
applicative language.  Thus, (aref1 'demo (@ a) 1) must *still* be
uninitialized.  And if you execute that expression in ACL2 you will see
that indeed it is.  However, a rather ugly comment is printed, namely
that this array access is "slow."  The reason it is slow is that the
raw lisp array associated with the name demo is the array we are
calling b.  To access the elements of a, aref1 must now do a linear
search.  Any reference to a as an array is now "unconventional;" in a
conventional language like Ada or Common Lisp it would simply be
impossible to refer to the value of the array before the assignment
that produced our b.

Now let us define a function that counts how many times a given object,
x, occurs in an array.  For simplicity, we will pass in the name and
highest index of the array:

     ACL2 !>(defun cnt (name a i x)
              (declare (xargs :guard
                              (and (array1p name a)
                                   (integerp i)
                                   (>= i -1)
                                   (< i (car (dimensions name a))))
                              :mode :logic
                              :measure (nfix (+ 1 i))))
              (cond ((zp (1+ i)) 0) ; return 0 if i is at most -1
                    ((equal x (aref1 name a i))
                     (1+ (cnt name a (1- i) x)))
                    (t (cnt name a (1- i) x))))

To determine how many times zero appears in (@ b) we can execute:

     ACL2 !>(cnt 'demo (@ b) 4 'zero)

The answer is 1.  How many times does uninitialized appear in (@ b)?

     ACL2 !>(cnt 'demo (@ b) 4 'uninitialized)

The answer is 3, because positions 2, 3 and 4 of the array contain that
default value.

Now imagine that we want to assign 'two to index 2 and then count how
many times the 2nd element of the array occurs in the array.  This
specification is actually ambiguous.  In assigning to b we produce a
new array, which we might call c.  Do we mean to count the occurrences
in c of the 2nd element of b or the 2nd element of c?  That is, do we
count the occurrences of uninitialized or the occurrences of two?  If
we mean the former the correct answer is 2 (positions 3 and 4 are
uninitialized in c); if we mean the latter, the correct answer is 1
(there is only one occurrence of two in c).

Below are ACL2 renderings of the two meanings, which we call [former]
and [latter].  (Warning:  Our description of these examples, and of an
example [fast former] that follows, assumes that only one of these
three examples is actually executed; for example, they are not executed
in sequence.  See "A Word of Warning" below for more about this issue.)

     (cnt 'demo (aset1 'demo (@ b) 2 'two) 4 (aref1 'demo (@ b) 2))  ; [former]

     (let ((c (aset1 'demo (@ b) 2 'two)))                           ; [latter]
       (cnt 'demo c 4 (aref1 'demo c 2)))

Note that in [former] we create c in the second argument of the call to
cnt (although we do not give it a name) and then refer to b in the
fourth argument.  This is unconventional because the second reference
to b in [former] is no longer the semantic value of demo.  While ACL2
computes the correct answer, namely 2, the execution of the aref1
expression in [former] is done slowly.

A conventional rendering with the same meaning is

     (let ((x (aref1 'demo (@ b) 2)))                           ; [fast former]
       (cnt 'demo (aset1 'demo (@ b) 2 'two) 4 x))

which fetches the 2nd element of b before creating c by assignment.  It
is important to understand that [former] and [fast former] mean exactly
the same thing: both count the number of occurrences of uninitialized
in c.  Both are legal ACL2 and both compute the same answer, 2.
Indeed, we can symbolically transform [fast former] into [former]
merely by substituting the binding of x for x in the body of the let.
But [fast former] can be evaluated faster than [former] because all of
the references to demo use the then-current semantic value of demo,
which is b in the first line and c throughout the execution of the cnt
in the second line.  [Fast former] is the preferred form, both because
of its execution speed and its clarity.  If you were writing in a
conventional language you would have to write something like [fast
former] because there is no way to refer to the 2nd element of the old
value of b after smashing b unless it had been saved first.

We turn now to [latter].  It is both clear and efficient.  It creates c
by assignment to b and then it fetches the 2nd element of c, two, and
proceeds to count the number of occurrences in c.  The answer is 1.
[Latter] is a good example of typical ACL2 array manipulation: after
the assignment to b that creates c, c is used throughout.

It takes a while to get used to this because most of us have grown
accustomed to the peculiar semantics of arrays in conventional
languages.  For example, in raw lisp we might have written something
like the following, treating b as a "global variable":

     (cnt 'demo (aset 'demo b 2 'two) 4 (aref 'demo b 2))

which sort of resembles [former] but actually has the semantics of
[latter] because the b from which aref fetches the 2nd element is not
the same b used in the aset!  The array b is destroyed by the aset and
b henceforth refers to the array produced by the aset, as written more
clearly in [latter].

A Word of Warning:  Users must exercise care when experimenting with
[former], [latter] and [fast former].  Suppose you have just created b
with the assignment shown above,

     ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))

If you then evaluate [former] in ACL2 it will complain that the aref1
is slow and compute the answer, as discussed.  Then suppose you
evaluate [latter] in ACL2.  From our discussion you might expect it to
execute fast -- i.e., issue no complaint.  But in fact you will find
that it complains repeatedly.  The problem is that the evaluation of
[former] changed the semantic value of demo so that it is no longer b.
To try the experiment correctly you must make b be the semantic value
of demo again before the next example is evaluated.  One way to do that
is to execute

     ACL2 !>(assign b (compress1 'demo (@ b)))

before each expression.  Because of issues like this it is often hard
to experiment with ACL2 arrays at the top-level.  We find it easier to
write functions that use arrays correctly and efficiently than to so
use them interactively.

This last assignment also illustrates a very common use of compress1.
While it was introduced as a means of removing irrelevant pairs from an
array built up by repeated assignments, it is actually most useful as a
way of insuring fast access to the elements of an array.

Many array processing tasks can be divided into two parts.  During the
first part the array is built.  During the second part the array is
used extensively but not modified.  If your programming task can be so
divided, it might be appropriate to construct the array entirely with
list processing, thereby saving the cost of maintaining the semantic
value of the name while few references are being made.  Once the alist
has stabilized, it might be worthwhile to treat it as an array by
calling compress1, thereby gaining constant time access to it.

ACL2's theorem prover uses this technique in connection with its
implementation of the notion of whether a rune is disabled or not.
Associated with every rune is a unique integer index, called its
"nume."  When each rule is stored, the corresponding nume is stored as
a component of the rule.  Theories are lists of runes and membership in
the "current theory" indicates that the corresponding rule is enabled.
But these lists are very long and membership is a linear-time
operation.  So just before a proof begins we map the list of runes in
the current theory into an alist that pairs the corresponding numes
with t.  Then we compress this alist into an array.  Thus, given a rule
we can obtain its nume (because it is a component) and then determine
in constant time whether it is enabled.  The array is never modified
during the proof, i.e., aset1 is never used in this example.  From the
logical perspective this code looks quite odd:  we have replaced a
linear-time membership test with an apparently linear-time assoc after
going to the trouble of mapping from a list of runes to an alist of
numes.  But because the alist of numes is an array, the "apparently
linear-time assoc" is more apparent than real; the operation is
constant-time.

AREF1    access the elements of a 1-dimensional array

     Example Form:
     (aref1 'delta1 a (+ i k))

     General Form:
     (aref1 name alist index)

where name is a symbol, alist is a 1-dimensional array and index is a
legal index into alist.  This function returns the value associated
with index in alist, or else the default value of the array.  See
ARRAYS for details.

This function executes in virtually constant time if alist is in fact
the "semantic value" associated with name (see ARRAYS).  When
it is not, aref1 must do a linear search through alist.  In that case
the correct answer is returned but a *slow array* comment is printed to
the comment window.  See SLOW-ARRAY-WARNING.

AREF2    access the elements of a 2-dimensional array

     Example Form:
     (aref2 'delta1 a i j)

     General Form:
     (aref2 name alist i j)

where name is a symbol, alist is a 2-dimensional array and i and j are
legal indices into alist.  This function returns the value associated
with (i . j) in alist, or else the default value of the array.  See
ARRAYS for details.

This function executes in virtually constant time if alist is in fact
the "semantic value" associated with name (see ARRAYS).  When
it is not, aref2 must do a linear search through alist.  In that case
the correct answer is returned but a *slow array* comment is printed to
the comment window.  See SLOW-ARRAY-WARNING.

ARRAY1P    recognize a 1-dimensional array

     Example Form:
     (array1p 'delta1 a)

     General Form:
     (array1p name alist)

where name and alist are arbitrary objects.  This function returns t if
alist is a 1-dimensional ACL2 array.  Otherwise it returns nil.  The
function operates in constant time if alist is the semantic value of
name.  See ARRAYS.

ARRAY2P    recognize a 2-dimensional array

     Example Form:
     (array2p 'delta1 a)

     General Form:
     (array2p name alist)

where name and alist are arbitrary objects.  This function returns t if
alist is a 2-dimensional ACL2 array.  Otherwise it returns nil.  The
function operates in constant time if alist is the semantic value of
name.  See ARRAYS.

ARRAYS-EXAMPLE    an example illustrating ACL2 arrays

The example below illustrates the use of ACL2 arrays.  It is not, of
course, a substitute for the detailed explanations provided elsewhere
(see ARRAYS, including subtopics).

     ACL2 !>(defun defarray (name size initial-element)
              (compress1 name
                         (cons (list :HEADER
                                     :DIMENSIONS (list size)
                                     :MAXIMUM-LENGTH (1+ size)
                                     :DEFAULT initial-element
                                     :NAME name)
                               nil)))

     Since DEFARRAY is non-recursive, its admission is trivial.  We observe
     that the type of DEFARRAY is described by the theorem
     (AND (CONSP (DEFARRAY NAME SIZE INITIAL-ELEMENT))
          (TRUE-LISTP (DEFARRAY NAME SIZE INITIAL-ELEMENT))).
     We used the :type-prescription rule COMPRESS1.

     Summary
     Form:  ( DEFUN DEFARRAY ...)
     Rules: ((:TYPE-PRESCRIPTION COMPRESS1))
     Warnings:  None
     Time:  0.02 seconds (prove: 0.00, print: 0.02, other: 0.00)
      DEFARRAY
     ACL2 !>(assign my-ar (defarray 'a1 5 17))
      ((:HEADER :DIMENSIONS (5)
                :MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
     ACL2 !>(aref1 'a1 (@ my-ar) 3)
     17
     ACL2 !>(aref1 'a1 (@ my-ar) 8)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol AREF1,
     which is
     (AND (ARRAY1P NAME L) (INTEGERP N) (>= N 0) (< N (CAR (DIMENSIONS NAME L)))),
     is violated by the arguments in the call (AREF1 'A1 '(#) 8).

     ACL2 !>(assign my-ar (aset1 'a1 (@ my-ar) 3 'xxx))
      ((3 . XXX)
       (:HEADER :DIMENSIONS (5)
                :MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
     ACL2 !>(aref1 'a1 (@ my-ar) 3)
     XXX
     ACL2 !>(aset1 'a1 (@ my-ar) 3 'yyy) ; BAD: (@ my-ar) now points to
                                         ;      an old copy of the array!
     ((3 . YYY)
      (3 . XXX)
      (:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
     ACL2 !>(aref1 'a1 (@ my-ar) 3) ; Because of "BAD" above, the array
                                    ; access is done using assoc rather
                                    ; than Lisp aref, hence is slower;
                                    ; but the answer is still correct,
                                    ; reflecting the value in (@ my-ar),
                                    ; which was not changed above.

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     A1 is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     XXX
     ACL2 !>

ASET1    set the elements of a 1-dimensional array

     Example Form:
     (aset1 'delta1 a (+ i k) 27)

     General Form:
     (aset1 name alist index val)

where name is a symbol, alist is a 1-dimensional array named name,
index is a legal index into alist, and val is an arbitrary object.  See
ARRAYS for details.  Roughly speaking this function "modifies"
alist so that the value associated with index is val.  More precisely,
it returns a new array, alist', of the same name and dimension as alist
that, under aref1, is everywhere equal to alist except at index where
the result is val.  That is, (aref1 name alist' i) is (aref1 name alist
i) for all legal indices i except index, where (aref1 name alist' i) is
val.

In order to "modify" alist, aset1 conses a new pair onto the front.  If
the length of the resulting alist exceeds the :maximum-length entry in
the array header, aset1 compresses the array as with compress1.

It is generally expected that the "semantic value" of name will be
alist (see ARRAYS).  This function operates in virtually
constant time whether this condition is true or not (unless the
compress1 operation is required).  But the value returned by this
function cannot be used efficiently by subsequent aset1 operations
unless alist is the semantic value of name when aset1 is executed.
Thus, if the condition is not true, aset1 prints a *slow array* warning
to the comment window.  See SLOW-ARRAY-WARNING.

ASET2    set the elements of a 2-dimensional array

     Example Form:
     (aset2 'delta1 a i j 27)

     General Form:
     (aset2 name alist i j val)

where name is a symbol, alist is a 2-dimensional array named name, i
and j are legal indices into alist, and val is an arbitrary object.
See ARRAYS for details.  Roughly speaking this function
"modifies" alist so that the value associated with (i . j) is val.
More precisely, it returns a new array, alist', of the same name and
dimension as alist that, under aref2, is everywhere equal to alist
except at (i . j) where the result is val.  That is, (aref2 name alist'
x y) is (aref2 name alist x y) for all legal indices x y except i and j
where (aref2 name alist' i j) is val.

In order to "modify" alist, aset2 conses a new pair onto the front.  If
the length of the resulting alist exceeds the :maximum-length entry in
the array header, aset2 compresses the array as with compress2.

It is generally expected that the "semantic value" of name will be
alist (see ARRAYS).  This function operates in virtually
constant time whether this condition is true or not (unless the
compress2 operation is required).  But the value returned by this
function cannot be used efficiently by subsequent aset2 operations
unless alist is the semantic value of name when aset2 is executed.
Thus, if the condition is not true, aset2 prints a *slow array* warning
to the comment window.  See SLOW-ARRAY-WARNING.

COMPRESS1    remove irrelevant pairs from a 1-dimensional array

     Example Form:
     (compress1 'delta1 a)

     General Form:
     (compress1 name alist)

where name is a symbol and alist is a 1-dimensional array, generally
named name.  See ARRAYS for details.  Logically speaking, this
function removes irrelevant pairs from alist, possibly shortening it.
The function returns a new array, alist', with the same header
(including name and dimension) as alist, that, under aref1, is
everywhere equal to alist.  That is, (aref1 name alist' i) is (aref1
name alist i), for all legal indices i.  Alist' may be shorter than
alist and the non-irrelevant pairs may occur in a different order than
in alist.

Practically speaking, this function plays an important role in the
efficient implementation of aref1.  In addition to creating the new
array, alist', compress1 makes that array the "semantic value" of name
and allocates a raw lisp array to name.  For each legal index, i, that
raw lisp array contains (aref1 name alist' i) in slot i.  Thus,
subsequent aref1 operations can be executed in virtually constant time
provided they are given name and the alist' returned by the most
recently executed compress1 or aset1 on name.  See ARRAYS.

In general, compress1 returns an alist whose cdr is an association list
whose keys are nonnegative integers in ascending order.  However, if the
header specifies an :order of > then the keys will occur in descending
order, and if the :order is :none or nil then the keys will not be
sorted, i.e., compress1 is logically the identity function (though it
still attaches an array under the hood).  Note however that a compress1
call is replaced by a hard error if the header specifies an :order of
:none or nil and the array's length exceeds the maximum-length field of
its header.

COMPRESS2    remove irrelevant pairs from a 2-dimensional array

     Example Form:
     (compress2 'delta1 a)

     General Form:
     (compress2 name alist)

where name is a symbol and alist is a 2-dimensional array, generally
named name.  See ARRAYS for details.  Logically speaking, this
function removes irrelevant pairs from alist, possibly shortening it.
The function returns a new array, alist', with the same header
(including name and dimension) as alist, that, under aref2, is
everywhere equal to alist.  That is, (aref2 name alist' i j) is (aref2
name alist i j), for all legal indices i and j.  Alist' may be shorter
than alist and the non-irrelevant pairs may occur in a different order
in alist' than in alist.

Practically speaking, this function plays an important role in the
efficient implementation of aref2.  In addition to creating the new
array, alist', compress2 makes that array the "semantic value" of name
and allocates a raw lisp array to name.  For all legal indices, i and
j, that raw lisp array contains (aref2 name alist' i j) in slot i,j.
Thus, subsequent aref2 operations can be executed in virtually constant
time provided they are given name and the alist' returned by the most
recently executed compress2 or aset2 on name.  See ARRAYS.

DEFAULT    return the :default from the header of a 1- or 2-dimensional array

     Example Form:
     (default 'delta1 a)

     General Form:
     (default name alist)

where name is an arbitrary object and alist is a 1- or 2-dimensional
array.  This function returns the contents of the :default field of the
header of alist.  When aref1 or aref2 is used to obtain a value for an
index (or index pair) not bound in alist, the default value is returned
instead.  Thus, the array alist may be thought of as having been
initialized with the default value.  default operates in virtually
constant time if alist is the semantic value of name.  See
ARRAYS.

DIMENSIONS    return the :dimensions from the header of a 1- or 2-dimensional array

     Example Form:
     (dimensions 'delta1 a)

     General Form:
     (dimensions name alist)

where name is arbitrary and alist is a 1- or 2-dimensional array.  This
function returns the dimensions list of the array alist.  That list
will either be of the form (dim1) or (dim1 dim2), depending on whether
alist is a 1- or 2-dimensional array.  Dim1 and dim2 will be integers
and each exceed by 1 the maximum legal corresponding index.  Thus, if
dimensions returns, say, '(100) for an array a named 'delta1, then
(aref1 'delta1 a 99) is legal but (aref1 'delta1 a 100) violates the
guards on aref1.  Dimensions operates in virtually constant time if
alist is the semantic value of name.  See ARRAYS.

FLUSH-COMPRESS    flush the under-the-hood array for the given name

     Example Form:
     (flush-compress 'my-array)

     General Form:
     (flush-compress name)

where name is a symbol.

Recall that (compress1 nm alist) associates an under-the-hood raw Lisp
one-dimensional array of name nm with the given association list,
alist, while (compress2 nm alist) is the analogous function for
two-dimensional arrays; see COMPRESS1 and see
COMPRESS2.  The only purpose of flush-compress, which always returns
nil, is to remove the association of any under-the-hood array with the
given name, thus eliminating slow array accesses (see
SLOW-ARRAY-WARNING).  It is not necessary if the return values of
compress1 and compress2 are always used as the "current" copy of the
named array, and thus flush-compress should rarely, if ever, be needed
in user applications.

Nevertheless, we provide the following contrived example to show how
flush-compress can be used to good effect.  Comments have been added to
this log to provide explanation.

     ACL2 !>(assign a (compress1 'demo
                                 '((:header :dimensions (5)
                                            :maximum-length 15
                                            :default uninitialized
                                            :name demo)
                                   (0 . zero)
                                   (1 . one))))
      ((:HEADER :DIMENSIONS (5)
                :MAXIMUM-LENGTH
                15 :DEFAULT UNINITIALIZED :NAME DEMO)
       (0 . ZERO)
       (1 . ONE))
     ACL2 !>(aref1 'demo (@ a) 0)
     ZERO
     ; As expected, the above evaluation did not cause a slow array warning.  Now
     ; we associate a different under-the-hood array with the name 'demo.
     ACL2 !>(compress1 'demo
                       '((:header :dimensions (5)
                                  :maximum-length 15
                                  :default uninitialized
                                  :name demo)
                         (0 . zero)))
     ((:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH
               15 :DEFAULT UNINITIALIZED :NAME DEMO)
      (0 . ZERO))
     ; The following array access produces a slow array warning because (@ a) is
     ; no longer associated under-the-hood with the array name 'demo.
     ACL2 !>(aref1 'demo (@ a) 0)

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     DEMO is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     ZERO
     ; Now we associate under-the-hood, with array name 'demo, an alist equal to
     ; (@ a).
     ACL2 !>(compress1 'demo
                       '((:header :dimensions (5)
                                  :maximum-length 15
                                  :default uninitialized
                                  :name demo)
                         (0 . zero)
                         (1 . one)))
     ((:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH
               15 :DEFAULT UNINITIALIZED :NAME DEMO)
      (0 . ZERO)
      (1 . ONE))
     ; The following array access is still slow, because the under-the-hood array
     ; is merely associated with a copy of (@ a), not with the actual object
     ; (@ a).
     ACL2 !>(aref1 'demo (@ a) 0)

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     DEMO is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     ZERO
     ; So we might try to fix the problem by recompressing. But this doesn't
     ; work.  It would work, by the way, if we re-assign a:
     ; (assign a (compress1 'demo (@ a))).  That is why we usually will not need
     ; flush-compress.
     ACL2 !>(compress1 'demo (@ a))
     ((:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH
               15 :DEFAULT UNINITIALIZED :NAME DEMO)
      (0 . ZERO)
      (1 . ONE))
     ACL2 !>(aref1 'demo (@ a) 0)

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     DEMO is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     ZERO
     ; Finally, we eliminate the warning by calling flush-compress before we call
     ; compress1.  The call of flush-compress removes any under-the-hood
     ; association of an array with the name 'demo.  Then the subsequent call of
     ; compress1 associates the object (@ a) with that name.  (Technical point:
     ; compress1 always associates the indicated name with the value that it
     ; returns.  in this case, what compress1 returns is (@ a), because (@ a) is
     ; already, logically speaking, a compressed array1p (starts with a :header
     ; and the natural number keys are ordered).
     ACL2 !>(flush-compress 'demo)
     NIL
     ACL2 !>(compress1 'demo (@ a))
     ((:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH
               15 :DEFAULT UNINITIALIZED :NAME DEMO)
      (0 . ZERO)
      (1 . ONE))
     ACL2 !>(aref1 'demo (@ a) 0)
     ZERO
     ACL2 !>

HEADER    return the header of a 1- or 2-dimensional array

     Example Form:
     (header 'delta1 a)

     General Form:
     (header name alist)

where name is arbitrary and alist is a 1- or 2-dimensional array.  This
function returns the header of the array alist.  The function operates
in virtually constant time if alist is the semantic value of name.  See
ARRAYS.

MAXIMUM-LENGTH    return the :maximum-length from the header of an array

     Example Form:
     (maximum-length 'delta1 a)

     General Form:
     (maximum-length name alist)

where name is an arbitrary object and alist is a 1- or 2-dimensional
array.  This function returns the contents of the :maximum-length field
of the header of alist.  Whenever an aset1 or aset2 would cause the
length of the alist to exceed its maximum length, a compress1 or
compress2 is done automatically to remove irrelevant pairs from the
array.  Maximum-length operates in virtually constant time if alist is
the semantic value of name.  See ARRAYS.

SLOW-ARRAY-WARNING    a warning or error issued when arrays are used inefficiently

If you use ACL2 arrays you may sometimes see a *slow array* warning.
We explain below what that warning means and some likely "mistakes" it
may signify.

First, we note that you can control whether or not you get a warning
and, if so, whether or not a break (error from which you can continue;
see BREAK$) ensues:

     (assign slow-array-action :warning) ; warn on slow array access (default)
     (assign slow-array-action :break)   ; warn as above, and then call break$
     (assign slow-array-action nil) ; do not warn or break on slow array access

If you are using ACL2 arrays, then you probably care about performance,
in which case is is probably best to avoid the nil setting.  Below we
assume the default behavior: a warning, but no break.

The discussion in the documentation for arrays defines what we mean by
the semantic value of a name.  As noted there, behind the scenes ACL2
maintains the invariant that with some names there is associated a pair
consisting of an ACL2 array alist, called the semantic value of the
name, and an equivalent raw lisp array.  Access to ACL2 array elements,
as in (aref1 name alist i), is executed in constant time when the array
alist is the semantic value of the name, because we can just use the
corresponding raw lisp array to obtain the answer.  Aset1 and compress1
modify the raw lisp array appropriately to maintain the invariant.

If aref1 is called on a name and alist, and the alist is not the
then-current semantic value of the name, the correct result is computed
but it requires linear time because the alist must be searched.  When
this happens, aref1 prints a *slow array* warning message to the
comment window.  Aset1 behaves similarly because the array it returns
will cause the *slow array* warning every time it is used.

From the purely logical perspective there is nothing "wrong" about such
use of arrays and it may be spurious to print a warning message.  But
because arrays are generally used to achieve efficiency, the *slow
array* warning often means the user's intentions are not being
realized.  Sometimes merely performance expectations are not met; but
the message may mean that the functional behavior of the program is
different than intended.

Here are some "mistakes" that might cause this behavior.  In the
following we suppose the message was printed by aset1 about an array
named name.  Suppose the alist supplied aset1 is alist.

(1) Compress1 was never called on name and alist.  That is, perhaps you
created an alist that is an array1p and then proceeded to access it
with aref1 but never gave ACL2 the chance to create a raw lisp array
for it.  After creating an alist that is intended for use as an array,
you must do (compress1 name alist) and pass the resulting alist' as the
array.

(2) Name is misspelled.  Perhaps the array was compressed under the
name 'delta-1 but accessed under 'delta1?

(3) An aset1 was done to modify alist, producing a new array, alist',
but you subsequently used alist as an array.  Inspect all (aset1 name
...) occurrences and make sure that the alist modified is never used
subsequently (either in that function or any other).  It is good
practice to adopt the following syntactic style.  Suppose the alist you
are manipulating is the value of the local variable alist.  Suppose at
some point in a function definition you wish to modify alist with
aset1.  Then write

     (let ((alist (aset1 name alist i val))) ...)

and make sure that the subsequent function body is entirely within the
scope of the let.  Any uses of alist subsequently will refer to the new
alist and it is impossible to refer to the old alist.  Note that if you
write

      (foo (let ((alist (aset1 name alist i val))) ...)  ; arg 1
           (bar alist))                                  ; arg 2

you have broken the rules, because in arg 1 you have modified alist but
in arg 2 you refer to the old value.  An appropriate rewriting is to
lift the let out:

      (let ((alist (aset1 name alist alist i val)))
        (foo ...                                         ; arg 1
             (bar alist)))                               ; arg 2

Of course, this may not mean the same thing.

(4) A function which takes alist as an argument and modifies it with
aset1 fails to return the modified version.  This is really the same as
(3) above, but focuses on function interfaces.  If a function takes an
array alist as an argument and the function uses aset1 (or a
subfunction uses aset1, etc.), then the function probably "ought" to
return the result produced by aset1.  The reasoning is as follows.  If
the array is passed into the function, then the caller is holding the
array.  After the function modifies it, the caller's version of the
array is obsolete.  If the caller is going to make further use of the
array, it must obtain the latest version, i.e., that produced by the
function.

BACKCHAIN-LIMIT    limiting the effort expended on relieving hypotheses

Before ACL2 can apply a rule with hypotheses, it must establish that the
hypotheses are true.  (We ignore the relaxing of this requirement
afforded by case-splits and forced hypotheses.)  ACL2 typically
establishes each hypothesis by backchaining -- instantiating the
hypothesis and then rewriting it recursively.  Here we describe how
ACL2 allows the user to limit backchaining.  At the end, below, we
describe the function backchain-limit.

Each hypothesis of a rewrite, meta, linear, or type-prescription rule
is assigned a backchain-limit when the rule is stored.  By default,
this limit is nil, denoting infinity (no limit).  However, the value
used for the default may be set to a non-negative integer (or to nil)
by the user; see SET-DEFAULT-BACKCHAIN-LIMIT.  The default is
overridden when a :backchain-limit-lst is supplied explicitly with the
rule; see RULE-CLASSES.  The number of recursive applications of
backchaining starting with the hypothesis of a rule is limited to the
backchain-limit associated with that hypothesis.

Moreover, the user may set global backchain-limits that limit the total
backchaining depth.  See SET-BACKCHAIN-LIMIT.  One limit is for
the use of rewrite, meta, and linear rules, while the other limit is
for so-called "type-set reasoning", which uses rules of class
type-prescription rules.  The two limits operate independently.  Below,
we discuss the first kind of backchain limits, i.e., for other than
type-prescription rules, except as otherwise indicated; but the
mechanism for those rules is similar.

Below we lay out the precise sense in which a global backchain-limit
interacts with the backchain-limits of individual rules in order to
limit backchaining.  But first we note that when further backchaining is
disallowed, ACL2 can still prove a hypothesis in a given context by
using that contextual information.  In fact, type-set reasoning may be
used (except that a weaker version of it is used in the second case
above, i.e., where we are already doing type-set reasoning).  Thus, the
relieving of hypotheses may be limited to the use of contextual
information (without backchaining, i.e., without recursively rewriting
hypotheses) by executing :set-backchain-limit 0.

Recall that there are two sorts of backchain limits: those applied to
hypotheses of individual rules, as assigned by their :rule-classes or
else taken from the default (see SET-DEFAULT-BACKCHAIN-LIMIT);
and the global limit, initially nil (no limit) but settable with
:set-backchain-limit.  Here is how these two types of limits interact
to limit backchaining, i.e., recursive rewriting of hypotheses.  ACL2
maintains a current backchain limit, which is the limit on the depth of
recursive calls to the rewriter, as well as a current backchain depth,
which is initially 0 and is incremented each time ACL2 backchains (and
is decremented when a backchain completes).  When ACL2 begins to
rewrite a literal (crudely, one of the "top-level" terms of the goal
currently being worked on), it sets the current backchain-limit to the
global value, which is initially nil but can be set using
:set-backchain-limit.  When ACL2 is preparing to relieve a hypothesis
by backchaining (hence, after it has already tried type-set reasoning),
it first makes sure that the current backchain limit is greater than
the current backchain depth.  If not, then it refuses to relieve that
hypothesis.  Otherwise, it increments the current backchain depth and
calculates a new current backchain-limit by taking the minimum of two
values: the existing current backchain-limit, and the sum of the
current backchain depth and the the backchain-limit associated with the
hypothesis.  Thus, ACL2 only modifies the current backchain-limit if it
is necessary to decrease that limit in order to respect the backchain
limit associated with the hypothesis.

We illustrate with the following examples.

     ; We stub out some functions so that we can reason about them.

     (defstub p0 (x) t)
     (defstub p1 (x) t)
     (defstub p2 (x) t)
     (defstub p3 (x) t)

     ; Initially, the default-backchain-limit is nil, or infinite.

     (defaxiom p2-implies-p1-limitless
       (implies (p2 x)
                (p1 x)))

     ; The following rule will have a backchain-limit of 0.

     (defaxiom p1-implies-p0-limit-0
       (implies (p1 x)
                (p0 x))
       :rule-classes ((:rewrite :backchain-limit-lst 0)))

     ; We have (p2 x) ==> (p1 x) ==> (p0 x).  We wish to establish that
     ; (p2 x) ==> (p0 x).  Normally, this would be no problem, but here
     ; we fail because ACL2 cannot establish (p0 x) by type-set reasoning
     ; alone.

     (thm
       (implies (p2 x)
                (p0 x)))

     ; We set the default-backchain-limit (for rewriting) to 1.

     :set-default-backchain-limit 1

     ; The following is more powerful than p1-implies-p0-limit-0
     ; because it can use rewrite rules to establish (p1 x).

     (defaxiom p1-implies-p0-limit-1
       (implies (p1 x)
                (p0 x)))

     ; This theorem will succeed:

     (thm
       (implies (p2 x)
                (p0 x)))

     ; We return the default-backchain-limit to its initial value.

     :set-default-backchain-limit nil

     ; Here is our last axiom.

     (defaxiom p3-implies-p2-limitless
       (implies (p3 x)
                (p2 x)))

     ; We now have (p3 x) ==> (p2 x) ==> (p1 x) ==> (p0 x).  However the
     ; rule p1-implies-p0-limit-1 has a backchain-limit of 1; hence we
     ; are not allowed to backchain far enough back to use
     ; p3-implies-p2-limitless.  We therefore lose.

     (defthm will-fail
       (implies (p3 x)
                (p0 x)))

Finally, we remark that to see the current global backchain-limits,
issue the following commands.

     (backchain-limit wrld :ts) ; backchain limit for type-set reasoning
     (backchain-limit wrld :rewrite) ; backchain limit for rewriting

BACKCHAIN-LIMIT-RW    hints keyword :BACKCHAIN-LIMIT-RW

See HINTS.

BACKTRACK    hints keyword :BACKTRACK

See HINTS.

BIBLIOGRAPHY    reports about ACL2

For a list of notes and reports about ACL2, see
`http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html'.

BIND-FREE    to bind free variables of a rewrite or linear rule

     Examples:
     (IMPLIES (AND (RATIONALP LHS)
                   (RATIONALP RHS)
                   (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
              (EQUAL (EQUAL LHS RHS)
                     (EQUAL (+ (- X) LHS) (+ (- X) RHS))))

     (IMPLIES (AND (BIND-FREE
                     (FIND-RATIONAL-MATCH-IN-TIMES-NESTS LHS RHS MFC STATE)
                     (X))
                   (RATIONALP X)
                   (CASE-SPLIT (NOT (EQUAL X 0))))
              (EQUAL (< LHS RHS)
                     (IF (< 0 X)
                         (< (* (/ X) LHS) (* (/ X) RHS))
                        (< (* (/ X) RHS) (* (/ X) LHS)))))

General Forms:

     (BIND-FREE term var-list)
     (BIND-FREE term t)
     (BIND-FREE term)

A rule which uses a bind-free hypothesis has similarities to both a
rule which uses a syntaxp hypothesis and to a :meta rule.  Bind-free is
like syntaxp, in that it logically always returns t but may affect the
application of a :rewrite or :linear rule when it is called at the
top-level of a hypothesis.  It is like a :meta rule, in that it allows
the user to perform transformations of terms under progammatic control.

Note that a bind-free hypothesis does not, in general, deal with the
meaning or semantics or values of the terms, but rather with their
syntactic forms.  Before attempting to write a rule which uses
bind-free, the user should be familiar with syntaxp and the internal
form that ACL2 uses for terms.  This internal form is similar to what
the user sees, but there are subtle and important differences.  Trans
can be used to view this internal form.

Just as for a syntaxp hypothesis, there are two types of bind-free
hypotheses.  The simpler type of bind-free hypothesis may be used as
the nth hypothesis in a :rewrite or :linear rule whose :corollary is
(implies (and hyp1 ... hypn ... hypk) (equiv lhs rhs)) provided term is
a term, term contains at least one variable, and every variable
occuring freely in term occurs freely in lhs or in some hypi, i<n.  In
addition, term must not use any stobjs.  (Later below we will describe
the second type, an _extended_ bind-free hypothesis, which may use
state.)

We begin our description of bind-free by examining the first example
above in some detail.

We wish to write a rule which will cancel "like" addends from both
sides of an equality.  Clearly, one could write a series of rules such
as

     (DEFTHM THE-HARD-WAY-2-1
        (EQUAL (EQUAL (+ A X B)
                      (+ X C))
               (EQUAL (+ A B)
                      (FIX C))))

with one rule for each combination of positions the matching addends
might be found in (if one knew before-hand the maximum number of
addends that would appear in a sum).  But there is a better way.  (In
what follows, we assume the presence of an appropriate set of rules for
simplifying sums.)

Consider the following definitions and theorem:

     (DEFUN INTERSECTION-EQUAL (X Y)
       (COND ((ENDP X)
              NIL)
             ((MEMBER-EQUAL (CAR X) Y)
              (CONS (CAR X) (INTERSECTION-EQUAL (CDR X) Y)))
             (T
              (INTERSECTION-EQUAL (CDR X) Y))))

     (DEFUN PLUS-LEAVES (TERM)
       (IF (EQ (FN-SYMB TERM) 'BINARY-+)
           (CONS (FARGN TERM 1)
                 (PLUS-LEAVES (FARGN TERM 2)))
         (LIST TERM)))

     (DEFUN FIND-MATCH-IN-PLUS-NESTS (LHS RHS)
       (IF (AND (EQ (FN-SYMB LHS) 'BINARY-+)
                (EQ (FN-SYMB RHS) 'BINARY-+))
           (LET ((COMMON-ADDENDS (INTERSECTION-EQUAL (PLUS-LEAVES LHS)
                                                     (PLUS-LEAVES RHS))))
             (IF COMMON-ADDENDS
                 (LIST (CONS 'X (CAR COMMON-ADDENDS)))
               NIL))
         NIL))

     (DEFTHM CANCEL-MATCHING-ADDENDS-EQUAL
       (IMPLIES (AND (RATIONALP LHS)
                     (RATIONALP RHS)
                     (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
                (EQUAL (EQUAL LHS RHS)
                       (EQUAL (+ (- X) LHS) (+ (- X) RHS)))))

How is this rule applied to the following term?

     (equal (+ 3 (expt a n) (foo a c))
            (+ (bar b) (expt a n)))

As mentioned above, the internal form of an ACL2 term is not always
what one sees printed out by ACL2.  In this case, by using :trans one
can see that the term is stored internally as

     (equal (binary-+ '3
                      (binary-+ (expt a n) (foo a c)))
            (binary-+ (bar b) (expt a n))).

When ACL2 attempts to apply cancel-matching-addends-equal to the term
under discussion, it first forms a substitution that instantiates the
left-hand side of the conclusion so that it is identical to the target
term.  This substitution is kept track of by the substitution alist:

     ((LHS . (binary-+ '3
                        (binary-+ (expt a n) (foo a c))))
      (RHS . (binary-+ (bar b) (expt a n)))).

ACL2 then attempts to relieve the hypotheses in the order they were
given. Ordinarily this means that we instantiate each hypothesis with
our substitution and then attempt to rewrite the resulting instance to
true.  Thus, in order to relieve the first hypothesis, we rewrite:

     (RATIONALP (binary-+ '3
                           (binary-+ (expt a n) (foo a c)))).

Let us assume that the first two hypotheses rewrite to t.  How do we
relieve the bind-free hypothesis?  Just as for a syntaxp hypothesis,
ACL2 evaluates (find-match-in-plus-nests lhs rhs) in an environment
where lhs and rhs are instantiated as determined by the substitution.
In this case we evaluate

     (FIND-MATCH-IN-PLUS-NESTS '(binary-+ '3
                                           (binary-+ (expt a n) (foo a c)))
                               '(binary-+ (bar b) (expt a n))).

Observe that, just as in the case of a syntaxp hypothesis, we
substitute the quotation of the variables bindings into the term to be
evaluated.  See SYNTAXP for the reasons for this.  The result
of this evaluation, ((X . (EXPT A N))), is then used to extend the
substitution alist:

     ((X . (EXPT A N))
      (LHS . (binary-+ '3
                        (binary-+ (expt a n) (foo a c))))
      (RHS . (binary-+ (bar b) (expt a n)))),

and this extended substitution determines
cancel-matching-addends-equal's result:

     (EQUAL (+ (- X) LHS) (+ (- X) RHS))
     ==>
     (EQUAL (+ (- (EXPT A N)) 3 (EXPT A N) (FOO A C))
            (+ (- (EXPT A N)) (BAR B) (EXPT A N))).

Question: What is the internal form of this result?
Hint: Use :trans.

When this rule fires, it adds the negation of a common term to both
sides of the equality by selecting a binding for the otherwise-free
variable x, under programmatic control.  Note that other mechanisms
such as the binding of free-variables may also extend the substitution
alist.

Just as for a syntaxp test, a bind-free form signals failure by
returning nil.  However, while a syntaxp test signals success by
returning true, a bind-free form signals success by returning an alist
which is used to extend the current substitution alist.  Because of
this use of the alist, there are several restrictions on it -- in
particular the alist must only bind variables, these variables must not
be already bound by the substitution alist, and the variables must be
bound to ACL2 terms.  If term returns an alist and the alist meets
these restrictions, we append the alist to the substitution alist and
use the result as the new current substitution alist.  This new current
substitution alist is then used when we attempt to relieve the next
hypothesis or, if there are no more, instantiate the right hand side of
the rule.

There is also a second, optional, var-list argument to a bind-free
hypothesis.  If provided, it must be either t or a list of variables.
If it is not provided, it defaults to t.  If it is a list of variables,
this second argument is used to place a further restriction on the
possible values of the alist to be returned by term: any variables
bound in the alist must be present in the list of variables.  We
strongly recommend the use of this list of variables, as it allows some
consistency checks to be performed at the time of the rule's admittance
which are not possible otherwise.

An extended bind-free hypothesis is similar to the simple type
described above, but it uses two additional variables, mfc and state,
which must not be bound by the left hand side or an earlier hypothesis
of the rule.  They must be the last two variables mentioned by term:
first mfc, then state.  These two variables give access to the
functions mfc-xxx; see EXTENDED-METAFUNCTIONS.  As described
there, mfc is bound to the so-called metafunction-context and state to
ACL2's state.  See BIND-FREE-EXAMPLES for examples of the use
of these extended bind-free hypotheses.

BIND-FREE-EXAMPLES    examples pertaining to bind-free hypotheses

See BIND-FREE for a basic discussion of the use of bind-free to
control rewriting.

We give examples of the use of bind-free hypotheses from the
perspective of a user interested in reasoning about arithmetic, but it
should be clear that bind-free can be used for many other purposes also.

EXAMPLE 1:  Cancel a common factor.

     (defun bind-divisor (a b)

     ; If a and b are polynomials with a common factor c, we return a
     ; binding for x.  We could imagine writing get-factor to compute the
     ; gcd, or simply to return a single non-invertible factor.

       (let ((c (get-factor a b)))
         (and c (list (cons 'x c)))))

     (defthm cancel-factor
       ;; We use case-split here to ensure that, once we have selected
       ;; a binding for x, the rest of the hypotheses will be relieved.
       (implies (and (acl2-numberp a)
                     (acl2-numberp b)
                     (bind-free (bind-divisor a b) (x))
                     (case-split (not (equal x 0)))
                     (case-split (acl2-numberp x)))
                (iff (equal a b)
                     (equal (/ a x) (/ b x)))))

EXAMPLE 2:  Pull integer summand out of floor.  Note:  This example has
an _extended_ bind-free hypothesis, which uses the term
(find-int-in-sum sum mfc state).

     (defun fl (x)
       ;; This function is defined, and used, in the IHS books.
       (floor x 1))

     (defun int-binding (term mfc state)
       ;; The call to mfc-ts returns the encoded type of term.
       ;; Thus, we are asking if term is known by type reasoning to
       ;; be an integer.
       (declare (xargs :stobjs (state) :mode :program))
       (if (ts-subsetp (mfc-ts term mfc state)
                       *ts-integer*)
             (list (cons 'int term))
       nil))

     (defun find-int-in-sum (sum mfc state)
       (declare (xargs :stobjs (state) :mode :program))
       (if (and (nvariablep sum)
                (not (fquotep sum))
                (eq (ffn-symb sum) 'binary-+))
           (or (int-binding (fargn sum 1) mfc state)
               (find-int-in-sum (fargn sum 2) mfc state))
         (int-binding sum mfc state)))

     ; Some additional work is required to prove the following.  So for
     ; purposes of illustration, we wrap skip-proofs around the defthm.

     (skip-proofs
      (defthm cancel-fl-int
       ;; The use of case-split is probably not needed, since we should
       ;; know that int is an integer by the way we selected it.  But this
       ;; is safer.
        (implies (and (acl2-numberp sum)
                      (bind-free (find-int-in-sum sum mfc state) (int))
                      (case-split (integerp int)))
                 (equal (fl sum)
                        (+ int (fl (- sum int)))))
        :rule-classes ((:rewrite :match-free :all)))
     )

     ; Arithmetic libraries will have this sort of lemma.
     (defthm hack (equal (+ (- x) x y) (fix y)))

     (in-theory (disable fl))

     (thm (implies (and (integerp x) (acl2-numberp y))
                   (equal (fl (+ x y)) (+ x (fl y)))))

EXAMPLE 3:  Simplify terms such as (equal (+ a (* a b)) 0)

     (defun factors (product)
       ;; We return a list of all the factors of product.  We do not
       ;; require that product actually be a product.
       (if (eq (fn-symb product) 'BINARY-*)
           (cons (fargn product 1)
                 (factors (fargn product 2)))
         (list product)))

     (defun make-product (factors)
       ;; Factors is assumed to be a list of ACL2 terms.  We return an
       ;; ACL2 term which is the product of all the ellements of the
       ;; list factors.
       (cond ((atom factors)
              ''1)
             ((null (cdr factors))
              (car factors))
             ((null (cddr factors))
              (list 'BINARY-* (car factors) (cadr factors)))
             (t
              (list 'BINARY-* (car factors) (make-product (cdr factors))))))

     (defun quotient (common-factors sum)
       ;; Common-factors is a list of ACL2 terms.   Sum is an ACL2 term each
       ;; of whose addends have common-factors as factors.  We return
       ;; (/ sum (make-product common-factors)).
       (if (eq (fn-symb sum) 'BINARY-+)
           (let ((first (make-product (set-difference-equal (factors (fargn sum 1))
                                                            common-factors))))
             (list 'BINARY-+ first (quotient common-factors (fargn sum 2))))
         (make-product (set-difference-equal (factors sum)
                                             common-factors))))

     (defun intersection-equal (x y)
       (cond ((endp x)
              nil)
             ((member-equal (car x) y)
              (cons (car x) (intersection-equal (cdr x) y)))
             (t
              (intersection-equal (cdr x) y))))

     (defun common-factors (factors sum)
       ;; Factors is a list of the factors common to all of the addends
       ;; examined so far.  On entry, factors is a list of the factors in
       ;; the first addend of the original sum, and sum is the rest of the
       ;; addends.  We sweep through sum, trying to find a set of factors
       ;; common to all the addends of sum.
       (declare (xargs :measure (acl2-count sum)))
       (cond ((null factors)
              nil)
             ((eq (fn-symb sum) 'BINARY-+)
              (common-factors (intersection-equal factors (factors (fargn sum 1)))
                              (fargn sum 2)))
             (t
              (intersection-equal factors (factors sum)))))

     (defun simplify-terms-such-as-a+ab-rel-0-fn (sum)
       ;; If we can find a set of factors common to all the addends of sum,
       ;; we return an alist binding common to the product of these common
       ;; factors and binding quotient to (/ sum common).
       (if (eq (fn-symb sum) 'BINARY-+)
           (let ((common-factors (common-factors (factors (fargn sum 1))
                                                 (fargn sum 2))))
             (if common-factors
                 (let ((common (make-product common-factors))
                       (quotient (quotient common-factors sum)))
                   (list (cons 'common common)
                         (cons 'quotient quotient)))
               nil))
         nil))

     (defthm simplify-terms-such-as-a+ab-=-0
       (implies (and (bind-free
                      (simplify-terms-such-as-a+ab-rel-0-fn sum)
                      (common quotient))
                     (case-split (acl2-numberp common))
                     (case-split (acl2-numberp quotient))
                     (case-split (equal sum
                                        (* common quotient))))
                (equal (equal sum 0)
                       (or (equal common 0)
                           (equal quotient 0)))))

     (thm (equal (equal (+ u (* u v)) 0)
           (or (equal u 0) (equal v -1))))

BREAKS    Common Lisp breaks

     Example:
     Broken at PROVE.  Type :H for Help.
     >>:Q

     ACL2 !>

You may interrupt the system by typing various control character
sequences.  The precise sequences are determined by the host Lisp and
operating system environment.  For example, in GCL and Allegro Common
Lisp, a console interrupt is caused by typing "ctrl-c".  If, however,
the GCL or Allegro is running in an Emacs shell buffer, one must type
"ctrl-c ctrl-c".

If a break occurs, for example because of a bug in ACL2 or a user
interrupt, the break will run a Common Lisp read-eval-print loop, not
an ACL2 read-eval-print loop.  This may not be obvious if the prompts
in the two loops are similar.  Because you are typing to a Common Lisp
evaluator, you must be careful.  It is possible to damage your ACL2
state in irreparable ways by executing non-ACL2 Common Lisp.  It is
even possible to disrupt and render inaccurate the interrupted
evaluation of a simple ACL2 expression.

For ACL2 built on most host Common Lisps, you will see the string [RAW
LISP] in the prompt at a break, to emphasize that one is inside a break
and hence should quit from the break.  For some host Common Lisps, the
top-level prompt also contains the string [RAW LISP].  See
PROMPT for how to control printing of that string.

The most reliable way to return to the ACL2 top level is by executing
the following command: (abort!).  Appropriate cleanup will then be
done, which should leave you in an appropriate state.

However, you may be able to quit from the break in the normal Lisp
manner (as with :q in GCL, :reset in Allegro CL, and q in CMU CL).  If
this attempt to quit is successful, it will return you to the innermost
ACL2 read-eval-print loop, with appropriate cleanup performed first.
Note that if you are within a brr environment when the break occurs,
quitting from the break will only return you to that environment, not
to the top of ACL2's read-eval-print loop.

BY    hints keyword :BY

See HINTS.

CANONICAL-PATHNAME    the true absolute filename, with soft links resolved

For the name fname of a file, the form (Canonical-pathname fname nil
state) evaluates to a Unix-style absolute filename representing the
same file as fname, but generally without any use of soft links in the
name.  (Below, we explain the qualifier "generally".)  If however the
file indicated by fname does not exist, (canonical-pathname fname nil
state) is nil.  Thus, canonical-pathname can be used as one would use
the raw Lisp function probe-file.

The specification of (Canonical-pathname fname dir-p state) when dir-p
is not nil is simlar, except that if the specified file exists but is
not a directory, then the result is nil.

The function canonical-pathname has a guard of t, though the second
argument must be the ACL2 state.  This function is introduced with the
following properties.

     (defthm canonical-pathname-is-idempotent
       (equal (canonical-pathname (canonical-pathname x dir-p state) dir-p state)
              (canonical-pathname x dir-p state)))
     (defthm canonical-pathname-type
       (or (equal (canonical-pathname x dir-p state) nil)
           (stringp (canonical-pathname x dir-p state)))
       :rule-classes :type-prescription)

We use the qualifier "generally", above, because there is no guarantee
that the filename will be canonical without soft links, though we
expect this to be true in practice.  ACL2 attempts to compute the
desired result and then checks that the input and result have the same
Common Lisp "truename".  This check is expected to succeed, but if it
fails then the input string is returned unchanged, and to be
conservative, the value returned is nil in this case if dir-p is true.

CASE-SPLIT    like force but immediately splits the top-level goal on the hypothesis

When a hypothesis of a conditional rule has the form (case-split hyp)
it is logically equivalent to hyp.  However it affects the application
of the rule generated as follows:  if ACL2 attempts to apply the rule
but cannot establish that the required instance of hyp holds in the
current context, it considers the hypothesis true anyhow, but (assuming
all hypotheses are seen to be true and the rule is applied) creates a
subgoal in which that instance of hyp is assumed false.  (There are
exceptions, noted below.)

For example, given the rule

     (defthm p1->p2
       (implies (case-split (p1 x))
                (p2 x)))

then an attempt to prove

     (implies (p3 x) (p2 (car x)))

can give rise to a single subgoal:

     (IMPLIES (AND (NOT (P1 (CAR X))) (P3 X))
              (P2 (CAR X))).

Unlike force, case-split does not delay the "false case" to a forcing
round but tackles it more or less immediately.

The special "split" treatment of case-split can be disabled by
disabling forcing:  see FORCE for a discussion of disabling
forcing, and also see DISABLE-FORCING.  Finally, we should
mention that the rewriter is never willing to split when there is an if
term present in the goal being simplified.  Since and terms and or
terms are merely abbreviations for if terms, they also prevent
splitting.  Note that if terms are ultimately eliminated using the
ordinary flow of the proof (but see
SET-CASE-SPLIT-LIMITATIONS), so case-split will ultimately function
as intended.

When in the proof checker, case-split behaves like force.

CASE-SPLIT-LIMITATIONS    a list of two "numbers" limiting the number of cases produced at once

     Examples:
     ACL2 !>(case-split-limitations (w state))
     (500 100)

With the setting above, clausify will not try subsumption/replacement
if more than 500 clauses are involved.  Furthermore, the simplifier, as
it sweeps over a clause, will inhibit further case splits when it has
accumulated 100 subgoals.  This inhibition is implemented by continuing
to rewrite subsequent literals but not splitting out their cases.  This
can produce literals containing IFs.

See SET-CASE-SPLIT-LIMITATIONS for a more general discussion.

CASES    hints keyword :CASES

See HINTS.

CHECK-SUM    assigning "often unique" integers to files and objects

A "check sum" is an integer in some fixed range computed from the
printed representation of an object, e.g., the sum, modulo 2**32, of
the ascii codes of all the characters in the printed representation.

Ideally, you would like the check sum of an object to be uniquely
associated with that object, like a fingerprint.  It could then be used
as a convenient way to recognize the object in the future: you could
remember the check sum (which is relatively small) and when an object
is presented to you and alleged to be the special one you could compute
its check sum and see if indeed it was.  Alas, there are many more
objects than check sums (after all, each check sum is an object, and
then there's t).  So you try to design a check sum algorithm that maps
similar looking objects far apart, in the hopes that corruptions and
counterfeits -- which appear to be similar to the object -- have
different check sums.  Nevertheless, the best you can do is a
many-to-one map.  If an object with a different check sum is presented,
you can be positive it is not the special object.  But if an object
with the same check sum is presented, you have no grounds for positive
identification.

The basic check sum algorithm in ACL2 is called check-sum-obj, which
computes the check sum of an ACL2 object.  Roughly speaking, we scan
the print representation of the object and, for each character
encountered, we multiply the ascii code of the character times its
position in the stream (modulo a certain prime) and then add (modulo a
certain prime) that into the running sum.  This is inaccurate in many
senses (for example, we don't always use the ascii code and we see
numbers as though they were printed in base 127) but indicates the
basic idea.

ACL2 uses check sums to increase security in the books mechanism; see
CERTIFICATE.