This is documentation for ACL2 Version 5.0
Copyright (C) 2012  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of Version 2 of the GNU General Public License as
published by the Free Software Foundation.

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.

WORLD    ACL2 property lists and the ACL2 logical data base

A "world" is a list of triples, each of the form (sym prop . val),
implementing the ACL2 notion of property lists.  ACL2 permits the
simultaneous existence of many property list worlds.  "The world" is
often used as a shorthand for "the ACL2 logical world" which is the
particular property list world used within the ACL2 system to maintain
the data base of rules.

Common Lisp provides the notion of "property lists" by which one can
attach "properties" and their corresponding "values" to symbols.  For
example, one can arrange for the 'color property of the symbol 'box-14
to be 'purple and the 'color property of the symbol 'triangle-7 to be
'yellow.  Access to property lists is given via the Common Lisp
function get.  Thus, (get 'box-14 'color) might return 'purple.
Property lists can be changed via the special form setf.  Thus, (setf
(get 'box-14 'color) 'blue) changes the Common Lisp property list
configuration so that (get 'box-14 'color) returns 'blue.  It should be
obvious that ACL2 cannot provide this facility, because Common Lisp's
get "function" is not a function of its argument, but instead a
function of some implicit state object representing the property list
settings for all symbols.

ACL2 provides the functions getprop and putprop which allow one to
mimic the Common Lisp property list facility.  However, ACL2's getprop
takes as one of its arguments a list that is a direct encoding of what
was above called the "state object representing the property list
settings for all symbols."  Because ACL2 already has a notion of
"state" that is quite distinct from that used here, we call this
property list object a "world."  A world is just a true list of
triples.  Each triple is of the form (sym prop . val).  This world can
be thought of as a slightly elaborated form of association list and
getprop is a slightly elaborated form of assoc that takes two keys.
When getprop is called on a symbol, s, property p, and world, w, it
scans w for the first triple whose sym is s and prop is p and returns
the corresponding val. Getprop has two additional arguments, one of
which that controls what it returns if no such sym and prop exist in w,
and other other of which allows an extremely efficient implementation.
To set some property's value for some symbol, ACL2 provides putprop.
(putprop sym prop val w) merely returns a new world, w', in which (sym
prop . val) has been consed onto the front of w, thus "overwriting" the
prop value of sym in w to val and leaving all other properties in w
unchanged.

One aspect of ACL2's property list arrangment is that it is possible to
have many different property list worlds.  For example, 'box-14 can
have 'color 'purple in one world and can have 'color 'yes in another,
and these two worlds can exist simultaneously because getprop is
explicitly provided the world from which the property value is to be
extracted.

The efficiency alluded to above stems from the fact that Common Lisp
provides property lists.  Using Common Lisp's provisions behind the
scenes, ACL2 can "install" the properties of a given world into the
Common Lisp property list state so as to make retrieval via getprop
very fast in the special case that the world provided to getprop has
been installed.  To permit more than one installed world, each of which
is permitted to be changed via putprop, ACL2 requires that worlds be
named and these names are used to distinquish installed versions of the
various worlds.  At the moment we do not further document getprop and
putprop.

However, the ACL2 system uses a property list world, named
'current-acl2-world, in which to store the succession of user commands
and their effects on the logic.  This world is often referred to in our
documentation as "the world" though it should be stressed that the user
is permitted to have worlds and ACL2's is in no way distinguished
except that the user is not permitted to modify it except via event
commands.  The ACL2 world is part of the ACL2 state and may be obtained
via (w state).

*Warning*: The ACL2 world is very large.  Its length as of this writing
(Version  2.5) is over 40,000 and it grows with each release.
Furthermore, some of the values stored in it are pointers to old
versions of itself.  Printing (w state) is something you should avoid
because you likely will not have the patience to await its completion.
For these practical reasons, the only thing you should do with (w
state) is provide it to getprop, as in the form

       (getprop sym prop default 'current-acl2-world (w state))

to inspect properties within it, or to pass it to ACL2 primitives, such
as theory functions, where it is expected.

Some ACL2 command forms, such as theory expressions (see
THEORIES) and the values to be stored in tables (see TABLE),
are permitted to use the variable symbol world freely with the
understanding that when these forms are evaluated that variable is
bound to (w state).  Theoretically, this gives those forms complete
knowledge of the current logical configuration of ACL2.  However, at
the moment, few world scanning functions have been documented for the
ACL2 user.  Instead, supposedly convenient macro forms have been
created and documented.  For example, (current-theory :here), which is
the theory expression which returns the currently enabled theory,
actually macroexpands to (current-theory-fn :here world).  When
evaluated with world bound to (w state), current-theory-fn scans the
current ACL2 world and computes the set of runes currently enabled in
it.

WORMHOLE    ld without state -- a short-cut to a parallel universe

     Example Form:
     ; The following form enters a recursive read-eval-print loop on a
     ; copy of the current state, allowing you to interact with that loop.
     ; Note that the form does not mention the ACL2 state variable!
     ; Evaluate the form below. Inside the resulting loop, define some function,
     ; e.g., with (defun foo (x) x).  Then exit with :q and observe,
     ; e.g., with :pe foo, that the external state did not change.

     (wormhole 'foo
               '(lambda (whs) (set-wormhole-entry-code whs :ENTER))
               nil
               '(list 'hello 'there))

     General Form:
     (wormhole name entry-lambda input form
       :current-package    ...  ; known package name
       :ld-skip-proofsp    ...  ; t, nil or 'include-book
       :ld-redefinition-action  ; nil or '(:a . :b)
       :ld-prompt          ...  ; nil, t, or some prompt printer fn
       :ld-keyword-aliases ...  ; an alist pairing keywords to parse info
       :ld-pre-eval-filter ...  ; :all, :query, or some new name
       :ld-pre-eval-print  ...  ; nil, t, or :never
       :ld-post-eval-print ...  ; nil, t, or :command-conventions
       :ld-evisc-tuple     ...  ; nil or '(alist level length hiding-cars)
       :ld-error-triples   ...  ; nil or t
       :ld-error-action    ...  ; :return!, :return, :continue, or :error
       :ld-query-control-alist  ; alist supplying default responses
       :ld-verbose         ...) ; nil or t

The keyword arguments above are exactly those of ld (see LD)
except that three of ld's keyword arguments are missing: the three that
specify the channels standard-oi, standard-co and proofs-co, which
default in wormhole to ACL2's comment window.

There are two ways to create and enter a wormhole:  wormhole as
described here and the simpler wormhole-eval.  We recommend you read
this full account of wormholes before using wormhole-eval.

Ignoring the use of entry-lambda, wormhole manufactures a named
"wormhole state" and calls the general-purpose ACL2 read-eval-print
loop ld on it.  However, when ld exits, the wormhole evaporates and the
function wormhole returns nil.  The manufactured state is like the
"current" ACL2 state except for two things.  First, some information
from the last wormhole state of this name is transferred into the new
state; this allows a wormhole to maintain some state from one call to
the next.  Second, some information from the wormhole call itself is
transferred into the new state; this allows the wormhole to be
sensitive to context.  These two changes to the current state are
reflected in the settings (@ wormhole-status) and (@ wormhole-input)
discussed in detail below.

Note that wormhole may be called from environments in which state is
not bound.  It is still applicative because it always returns nil.

There are some restrictions about what can be done inside a wormhole.
As you may imagine, we really do not "copy the current state" but
rather just keep track of how we modified it and undo those
modifications upon exit.  An error is signalled if you try to modify
state in an unsupported way.  For this same reason, wormholes do not
allow updating of any user-defined single-threaded objects.  See
STOBJ.

One example wormhole is the implementation of the ACL2
accumulated-persistence facility for tracking the frequency with which
rules are tried.  To implement this feature directly the theorem prover
would have to take the tracking data as an argument and pass it around
so that updates could be accumulated.  This would greatly clutter the
code.  Instead, the tracking data is maintained in a wormhole.  The
theorem prover enters the wormhole to update the data as rules are
tried.  When you request a display of the data,
show-accumulated-persistence enters the wormhole and prints the data.
But the data is never available outside that wormhole.  The ACL2 system
uses a second wormhole to implement the brr facility, allowing the user
to interact with the rewriter as rules are applied.

We now specify the arguments and behavior of wormhole.

The name argument must be a quoted constant and is typically a symbol.
It will be the "name" of the wormhole.  A wormhole of that name will be
created the first time either wormhole or wormhole-eval is called.

Every wormhole name has a "status."  The status of a wormhole is stored
outside of ACL2; it is inaccessible to the ACL2 user except when in the
named wormhole.  But the status of a wormhole may be set by the user
from within the wormhole.

Upon the first call of wormhole or wormhole-eval on a name, the status
of that name is nil.  But in general you should arrange for the status
to be a cons.  The status is set by the quoted lambda every time
wormhole is called; but it may also be set in the form argument (the
first form evaluated in the interactive loop) by assigning to the state
global variable wormhole-status, as with

     (assign wormhole-status ...)

or even by the user interacting with the loop if you do not exit the
loop with the first form.  The car of the cons should be either :ENTER
or :SKIP and is called the wormhole's "entry code."  The entry code of
nil or an unexpectedly shaped status is :ENTER.  The cdr of the cons is
arbitrary data maintained by you.

When wormhole is invoked, the status of the specified name is
incorporated into the manufactured wormhole state.  In particular,
inside the wormhole, the status is the value of the state global
variable wormhole-status.  That is, inside the wormhole, the status may
be accessed by (@ wormhole-status) and set by (assign wormhole-status
...), f-get-global and f-put-global.  When ld exits - typically because
the form :q was read by ld - the then-current value of wormhole-status
is hidden away so that it can be restored when this wormhole is entered
again.  The rest of the wormhole state is lost.

This allows a sequence of entries and exits to a wormhole to maintain
some history in the status and this information can be manipulated by
ACL2 functions executing inside the wormhole.

The second argument to wormhole must be a quoted lambda expression.  We
explain it later.

The third argument, input, may be any term.  The value of the term is
passed into the manufactured wormhole state, allowing you to pass in
information about the calling context.  Inside the wormhole, the input
is available via (@ wormhole-input).  It could be reassigned via
(assign wormhole-input ...), but there is no reason to do that.

The fourth argument, form, may be any term; when ld is called on the
manufactured wormhole state, the first form evaluated by ld will be the
value of form.  Note that form will be translated by ld.  Errors,
including guard violations, in the translation or execution of that
first form will leave you in the interactive loop of the wormhole state.

When used properly, the first form allows you to greet your user before
reading the first interactive command or simply to do whatever
computation you want to do inside the wormhole and exit silently.  We
give examples below.

Manufacturing a wormhole state is relatively expensive; in addition, the
forms executed by ld must be read, translated, and interpreted as with
any user type-in.  The entry-lambda offers a way to avoid this or, at
least, to decide whether to incur that expense.

Before the wormhole state is manufactured and entered, the entry-lambda
is applied to the current wormhole status with wormhole-eval.  That
lambda application must produce a new wormhole status, which is stored
as the wormhole's status.  The entry code for the new status determines
whether wormhole actually manufactures a wormhole state and calls ld.

If the entry code for that new status is :ENTER the wormhole state is
manufactured and entered; otherwise, the new status is simply saved as
the most recent status but the wormhole state is not manufactured or
entered.  Note therefore that the entry-lambda may be used to perform
two functions: (a) to determine if it is really necessary to
manufacture a state and (b) to update the data in the wormhole status
as a function of the old status without invoking ld.

The entry-lambda must be a quoted lambda expression of at most one
argument.  Thus, the argument must be either

     '(lambda (whs) <body>)

or

     '(lambda () <body>)

Note the quote.  If a formal, e.g., whs, is provided, it must be used as
a variable in the lambda body.  The lambda-expression may contain free
variables, that is, the body may mention variables other than the
lambda formal.  These free variables are understood in the caller's
environment.  These conventions allow us to compile the entry-lambda
application very efficiently when the guard has been verified.

The guard on a call of wormhole is the conjunction of the guards on the
arguments conjoined with the guard on the body of the entry-lambda.
See WORMHOLE-EVAL for a discussion of the guard on the
lambda-expression.

The functions wormhole-statusp, wormhole-entry-code, wormhole-data,
set-wormhole-entry-code, set-wormhole-data, and make-wormhole-status
may be useful in manipulating entry codes and data in the entry-lambda.

Note that you access and manipulate the wormhole's status in two
different ways depending on whether you're "outside" of the wormhole
applying the quoted lambda or "inside" the read-eval-print loop of the
wormhole.

OUTSIDE (wormhole-eval): access via the value of the lambda formal and
set by returning the new status as the value of the lambda body.

INSIDE (ld phase of wormhole): access via (@ wormhole-status), and set
via (assign wormhole-status ...).

Pragmatic Advice on Designing a Wormhole: Suppose you are using
wormholes to implement some extra-logical utility.  You must
contemplate how you will use your wormhole's status to store hidden
information.  You might be tempted to exploit the entry code as part of
the status.  For example, you may think of :ENTER as indicating that
your utility is "turned on" and :SKIP as indicating that your utility
is "turned off."  We advise against such a design.  We recommend you
base your decisions on the wormhole data.  We recommend that you set
but not read the wormhole entry code to signal whether you wish to
enter a full-fledged wormhole.  To use the entry code as a flag
overloads it and invites confusion when your facility is "turned off"
but you have to enter the wormhole for some reason.

For a behind-the-scenes description of how wormholes work, See
WORMHOLE-IMPLEMENTATION.

Here are some sample situations handled by wormhole-eval and wormhole.
Let the wormhole in question be named DEMO.  Initially its status is
NIL.  The functions below all maintain the convention that the status
is either nil or of the form (:key . lst), where :key is either :SKIP
or :ENTER and lst is a true-list of arbitrary objects.  But since there
is no way to prevent the user from entering the DEMO wormhole
interactively and doing something to the status, this convention cannot
be enforced.  Thus, the functions below do what we say they do, e.g.,
remember all the values of x ever seen, only if they're the only
functions messing with the DEMO status.  On the other hand, the guards
of all the functions below can be verified.  We have explicitly
declared that the guards on the functions below are to be verified, to
confirm that they can be.  Guard verification is optional but wormholes
(and wormhole-eval in particular) are more efficient when guards have
been verified.  All of the functions defined below return nil.

The examples below build on each other.  If you really want to
understand wormholes we recommend that you evaluate each of the forms
below, in the order they are discussed.

Q. How do I create a wormhole that prints its status to the comment
window?

     (defun demo-status ()
       (declare (xargs :verify-guards t))
       (wormhole-eval 'demo
                      '(lambda (whs)
                         (prog2$ (cw "DEMO status:~%~x0~%" whs)
                                 whs))
                      nil))

Note above that after printing the status to the comment window we
return the new (unchanged) status whs.  Had we just written the call of
cw, which returns nil, the function would print the status and then set
it to nil!

Q.  How do I use a wormhole to collect every symbol, x, passed to the
function?

     (defun demo-collect (x)
       (declare (xargs :verify-guards t))
       (wormhole-eval 'demo
                      '(lambda (whs)
                         (make-wormhole-status whs
                                               (wormhole-entry-code whs)
                                               (if (symbolp x)
                                                   (cons x (wormhole-data whs))
                                                   (wormhole-data whs))))
                      nil))

We could have also defined this function this way:

     (defun demo-collect (x)
       (declare (xargs :verify-guards t))
       (if (symbolp x)
           (wormhole-eval 'demo
                          '(lambda (whs)
                             (set-wormhole-data whs
                                                (cons x (wormhole-data whs))))
                          nil)
           nil))

Both versions always return nil and both versions collect into the
wormhole data field just the symbols x upon which demo-collect is
called.

Q.  How do I use demo-collect?  Below is a function that maps over a
list and computes its length.  But it has been annotated with a call to
demo-collect on every element.

      (defun my-len (lst)
        (if (endp lst)
            0
            (+ 1
               (prog2$ (demo-collect (car lst))
                       (my-len (cdr lst))))))

Thus, for example:

     ACL2 !>(my-len '(4 temp car "Hi" rfix))
     5
     ACL2 !>(demo-status)
     DEMO status:
     (:ENTER RFIX CAR TEMP)
     NIL
     ACL2 !>

Q.  How do I set the entry code to :ENTER or :SKIP according to whether
name is a member-equal of the list of things seen so far?  Note that we
cannot check this condition outside the wormhole, because it depends on
the list of things collected so far.  We make the decision inside the
lambda-expression.  Note that we explicitly check that the guard of
member-equal is satisfied by the current wormhole status, since we
cannot rely on the invariant that no other function interferes with the
status of the DEMO wormhole.  In the case that the status is
"unexpected" we act like the status is nil and set it to (:SKIP . NIL).

     (defun demo-set-entry-code (name)
       (declare (xargs :verify-guards t))
       (wormhole-eval 'demo
                      '(lambda (whs)
                         (if (true-listp (wormhole-data whs))
                             (set-wormhole-entry-code
                              whs
                              (if (member-equal name (wormhole-data whs))
                                  :ENTER
                                  :SKIP))
                             '(:SKIP . NIL)))
                      nil))

Thus

     ACL2 !>(demo-set-entry-code 'monday)
     NIL
     ACL2 !>(demo-status)
     DEMO status:
     (:SKIP RFIX CAR TEMP)
     NIL
     ACL2 !>(demo-set-entry-code 'rfix)
     NIL
     ACL2 !>(demo-status)
     DEMO status:
     (:ENTER RFIX CAR TEMP)
     NIL
     ACL2 !>

Q.  Suppose I want to collect every symbol and then, if the symbol has
an ABSOLUTE-EVENT-NUMBER property in the ACL2 logical world, print the
defining event with :pe and then enter an interactive loop; but if the
symbol does not have an ABSOLUTE-EVENT-NUMBER, don't print anything and
don't enter an interactive loop.

Here it is not important to know what ABSOLUTE-EVENT-NUMBER is; this
example just shows that we can use a wormhole to access the ACL2 logical
world, even in a function that does not take the state as an argument.

In the code below, we use wormhole instead of wormhole-eval, because we
might have to access the logical world and enter an interactive loop.
But for efficiency we do as much as we can inside the entry lambda,
where we can check whether x is symbol and collect it into the data
field of the wormhole status.  Note that if we collect x, we also set
the entry code to :ENTER.  If we don't collect x, we set the entry code
to :SKIP.

     (defun collect-symbols-and-print-events (x)
       (declare (xargs :guard t))
       (wormhole 'demo
                 '(lambda (whs)
                    (if (symbolp x)
                        (make-wormhole-status whs
                                              :ENTER
                                              (cons x (wormhole-data whs)))
                        (set-wormhole-entry-code whs :SKIP)))

     ; The wormhole will not get past here is unless the entry code is
     ; :ENTER.  If we get past here, we manufacture a state, put
     ; x into (@ wormhole-input) and call ld in such a way that the
     ; first form executed is the quoted if-expression below.

                 x
                 '(if (getprop (@ wormhole-input)
                               'absolute-event-number
                               nil
                               'CURRENT-ACL2-WORLD (w state))
                      (er-progn
                       (mv-let (col state)
                               (fmt "~%Entering a wormhole on the event name ~x0~%"
                                    (list (cons #\0 (@ wormhole-input)))
                                    *standard-co* state nil)
                               (declare (ignore col))
                               (value nil))
                       (pe (@ wormhole-input))
                       (set-ld-prompt 'wormhole-prompt state)
                       (value :invisible))
                      (value :q))
                 :ld-verbose nil
                 :ld-prompt nil))

The "first form" (the if) asks whether the wormhole-input (i.e., x) has
an ABSOLUTE-EVENT-NUMBER property.  If so, it enters an er-progn to
perform a sequence of commands, each of which returns an ACL2 error
triple (see PROGRAMMING-WITH-STATE).  The first form uses fmt
to print a greeting.  Since fmt returns (mv col state) and we must
return an error triple, we embed the fmt term in an (mv-let (col state)
... (value nil)).  The macro value takes an object and returns a
"normal return" error triple.  The second form in the er-progn uses the
ACL2 history macro pe (see PE) to print the defining event for
a name.  The third form sets the prompt of this read-eval-print loop to
the standard function for printing the wormhole prompt.  We silenced
the printing of the prompt when we called ld, thanks to the :ld-prompt
nil keyword option.  More on this below.  The fourth form returns the
error triple value :invisible as the value of the first form.  This
prevents ld from printing the value of the first form.  Since we have
not exited ld, that function just continues by reading the next form
from the comment window.  The user perceives this as entering a
read-eval-print loop.  We continue in the loop until the user types :q.

On the other branch of the if, if the symbol has no
ABSOLUTE-EVENT-NUMBER property, we execute the form (value :q), which
is the programming equivalent of typing :q.  That causes the ld to exit.

The ld special variables set in the call to wormhole and further
manipulated inside the first form to ld may require explanation.  By
setting :ld-verbose to nil, we prevent ld from printing the familiar
ACL2 banner when ld is called.  If :ld-verbose nil is deleted, then you
would see something like

     ACL2 Version  4.0.  Level 2.
     ...
     Type (good-bye) to quit completely out of ACL2.

before the first form is read and evaluated.

By setting :ld-prompt to nil we prevent ld from printing the prompt
before reading and evaluating the first form.

As this example shows, to use full-blown wormholes you must understand
the protocol for using wormhole status to control whether a wormhole
state is manufactured for ld and you must also understand programming
with state and the effects of the various ld "special variables."

From the discussion above we see that wormholes can be used to create
formatted output without passing in the ACL2 state.  For examples see
CW, in particular the discussion at the end of that
documentation topic.

WORMHOLE-DATA    determines the wormhole data object from a wormhole status object

     General Form:  (wormhole-data whs)

See WORMHOLE.  Returns the wormhole data from a well-formed
wormhole status whs.  If whs is nil or not well-formed, the data is nil.

WORMHOLE-ENTRY-CODE    determines the wormhole entry code from a wormhole status object

     General Form:  (wormhole-entry-code whs)

See WORMHOLE.  Returns :ENTER or :SKIP given a well-formed
wormhole status whs.  If whs is nil or not well-formed, the entry code
is :ENTER.

WORMHOLE-EVAL    state-saving without state -- a short-cut to a parallel universe

     Example Form:
     (wormhole-eval 'demo
        '(lambda (whs)
           (set-wormhole-data whs
                              (cons (cons name info)
                                    (wormhole-data whs))))
        (prog2$ info name))

     General Form:
     (wormhole-eval name lambda varterm)

where name must be a quoted wormhole name and lambda must be a quoted
lambda-expression.  The lambda-expression must have at most one formal
parameter but the body of the lambda-expression may contain other
variables.  Note that in the example form given above, the lambda has
one formal, whs, and uses name and info freely.  Note that the lambda
is quoted.  The third argument of wormhole-eval, varterm, is an
arbitrary term that should mention all of the free variables in the
lambda-expression.  That term establishes your "right" to refer to
those free variables in the environment in which the wormhole-eval
expression occurs.  The value of varterm is irrelevant and if you
provide nil ACL2 will automatically provide a suitable term, namely a
prog2$ form like the one shown in the example above.

See WORMHOLE for a full explanation of wormholes.  Most
relevant here is that every wormhole has a name and a status.  The
status is generally a cons pair whose car is the keyword :ENTER or the
keyword :SKIP and whose cdr is an arbitrary object used to store
information from one wormhole call to the next.

Here is a succinct summary of wormhole-eval.  If the lambda-expression
has a local variable, wormhole-eval applies the lambda-expression to
the wormhole status of the named wormhole and remembers the value as
the new wormhole status.  If the lambda has no formal parameter, the
lambda is applied to no arguments and the value is the new status.
Wormhole-eval returns nil.  Thus, the formal parameter of the
lambda-expression, if provided, denotes the wormhole's hidden status
information; the value of the lambda is the new status and is hidden
away.

The guard of a wormhole-eval call is the guard of the body of the
lambda-expression, with a fresh variable symbol used in place of the
formal so that no assumptions are possible about the hidden wormhole
status.  If the guard of a wormhole-eval is verified, the call is
macroexpanded inline to the evaluation of the body in a suitable
environment.  Thus, it can be a very fast way to access and change
hidden state information, but the results must remain hidden.  To do
arbitrary computations on the hidden state (i.e., to access the ACL2
state or logical world or to interact with the user) see
WORMHOLE.

Functions that are probably useful in the body of the lambda or the
guard of a function using wormhole-eval include the following:
wormhole-statusp, wormhole-entry-code, wormhole-data,
set-wormhole-entry-code, set-wormhole-data, and make-wormhole-status.

See WORMHOLE for a series of example uses of wormhole-eval and
wormhole.

For a behind-the-scenes description of how wormholes work, See
WORMHOLE-IMPLEMENTATION.

WORMHOLE-IMPLEMENTATION    notes on how wormholes are implemented

What happens when you call wormhole?  Recall that a typical call of the
function looks like this:

     (wormhole 'name
               '(lambda (whs) ...)
               input
               form
               :ld-verbose ...
               ...)

A brief recap of the advertised semantics for wormhole establishes our
terminology: When the above wormhole is evaluated, the
lambda-expression is applied to the wormhole's status and the result is
stored as the new status.  Then, if the entry-code of the new status is
:ENTER, ld is invoked on a copy of the "current state" with the
specified ld- "special variables;" output is directed to the comment
window.  In that copy of the state, the state-global variable
wormhole-input is set to the value of input and the state-global
variable wormhole-status is set to the (new) status computed by the
lambda-expression.  Thus, inside the wormhole, (@ wormhole-input)
returns the list of inputs, (@ wormhole-status) returns the current
status, and (assign wormhole-status ...) sets the wormhole's status.
The first form executed by the ld is the value of form and unless that
form returns (value :q), causing the ld to quit, the ld proceeds to
take subsequent input from the comment window.  Upon exiting from ld,
the wormhole state "evaporates."  The wormhole's status upon exit is
remembered and restored the next time the wormhole is entered.

Here is what really happens.

Each wormhole's status is recorded in an alist stored in a Common Lisp
global variable named *wormhole-status-alist*.  This variable is not
part of the ACL2 state.  If you exit the ACL2 loop with :q you can
inspect the value of *wormhole-status-alist*.  When the
lambda-expression is evaluated it is applied to the value associated
with name in the alist and the result is stored back into that alist.
This step is performed by wormhole-eval.  To make things more
efficient, wormhole-eval is just a macro that expands into a let that
binds the lambda formal to the current status and whose body is the
lambda body.  Guard clauses are generated from the body, with one
exception:  the lambda formal is replaced by a new variable so that no
prior assumptions are available about the value of the the wormhole
status.

If the newly computed status has an entry code of :ENTER ld will be
invoked.  But we don't really copy state, of course.  Instead we will
invoke ld on the live state, which is always available in the von
Neumann world in which ACL2 is implemented.  To give the illusion of
copying state, we will undo changes to the state upon exiting.  To
support this, we do two things just before invoking ld: we bind a
Common Lisp special variable is to t to record that ACL2 is in a
wormhole, and we initialize an accumulator that will be used to record
state changes made while in the wormhole.

Then ld is invoked, with first argument, standard-oi, being set to
(cons form *standard-oi*).  According to the standard semantics of ld,
this reads and evaluates form and then the forms in the specified
channel.  The standard channels are directed to and from the terminal,
which is the physical realization of the comment window.

All state modifying functions of ACL2 are sensitive to the special
variable that indicates that evaluation is in a wormhole.  Some ACL2
state-modifying functions (e.g., those that modify the file system like
write-byte$) are made to cause an error if invoked inside a wormhole on
a file other than the terminal.  Others, like f-put-global (the
function behind such features as assign and maintenance of the ACL2
logical world by such events as defun and defthm) are made to record
the old value of the state component being changed; these records are
kept in the accumulator initialized above.

Upon exit from ld for any reason, the final value of (@ wormhole-status)
is stored in *wormhole-status-alist* and then the accumulator is used to
"undo" all the state changes.

Wormhole always returns nil.

WORMHOLE-P    predicate to determine if you are inside a wormhole

See WORMHOLE for a discussion of wormholes.  (Wormhole-p state)
returns (mv nil t state) when evaluated inside a wormhole, else (mv nil
nil state).

WORMHOLE-STATUSP    predicate recognizing well-formed wormhole status object

     General Form:  (wormhole-statusp whs)

See WORMHOLE.  This predicate is useful in guards for
wormholes.  It checks whether whs is either nil or a cons whose car is
:ENTER or :SKIP.

XARGS    giving hints to defun

Common Lisp's defun function does not easily allow one to pass extra
arguments such as "hints".  ACL2 therefore supports a peculiar new
declaration (see DECLARE) designed explicitly for passing
additional arguments to defun via a keyword-like syntax.

The following declaration is nonsensical but does illustrate all of the
xargs keywords (which are the members of the list *xargs-keywords*).

     (declare (xargs :guard (symbolp x)
                     :guard-hints (("Goal" :in-theory (theory batch1)))
                     :guard-debug t
                     :hints (("Goal" :in-theory (theory batch1)))
                     :measure (- i j)
                     :ruler-extenders :basic
                     :mode :logic
                     :non-executable t
                     :normalize nil
                     :otf-flg t
                     :stobjs ($s)
                     :verify-guards t
                     :well-founded-relation my-wfr))

     General Form:
     (xargs :key1 val1 ... :keyn valn)

where the keywords and their respective values are as shown below.
Note that once "inside" the xargs form, the "extra arguments" to defun
are passed exactly as though they were keyword arguments.

:GUARD
Value is a term involving only the formals of the function being
defined.  The actual guard used for the definition is the conjunction
of all the guards and types (see DECLARE) declared.

:GUARD-HINTS
Value:  hints (see HINTS), to be used during the guard
verification proofs as opposed to the termination proofs of the defun.

:GUARD-DEBUG
Value:  nil by default, else directs ACL2 to decorate each guard proof
obligation with hypotheses indicating its sources.  See
GUARD-DEBUG.

:HINTS
Value:  hints (see HINTS), to be used during the termination
proofs as opposed to the guard verification proofs of the defun.

:MEASURE
Value is a term involving only the formals of the function being
defined.  This term is indicates what is getting smaller in the
recursion.  The well-founded relation with which successive measures
are compared is o<.  Also allowed is a special case, (:? v1 ... vk),
where (v1 ... vk) enumerates a subset of the formal parameters such
that some valid measure involves only those formal parameters.
However, this special case is only allowed for definitions that are
redundant (see REDUNDANT-EVENTS) or are executed when skipping
proofs (see SKIP-PROOFS).

:RULER-EXTENDERS
For recursive definitions (possibly mutually recursive), value controls
termination analysis and the resulting stored induction scheme.  See
RULER-EXTENDERS for a discussion of legal values and their
effects.

:MODE
Value is :program or :logic, indicating the defun mode of the function
introduced.  See DEFUN-MODE.  If unspecified, the defun mode
defaults to the default defun mode of the current world.  To convert a
function from :program mode to :logic mode, see
VERIFY-TERMINATION.

:NON-EXECUTABLE
Value is normally t or nil (the default).  Rather than stating
:non-executable t directly, which requires :logic mode and that the
definitional body has a certain form, we suggest using the macro
defun-nx or defund-nx; see DEFUN-NX.  A third value of
:non-executable for advanced users is :program, which is generated by
expansion of defproxy forms; see DEFPROXY.  For another way to
deal with non-executability, see NON-EXEC.

:NORMALIZE
Value is a flag telling defun whether to propagate if tests upward.
Since the default is to do so, the value supplied is only of interest
when it is nil.  (See DEFUN).

:OTF-FLG
Value is a flag indicating "onward through the fog" (see
OTF-FLG).

:STOBJS
Value is either a single stobj name or a true list of stobj names (see
STOBJ and see DEFSTOBJ, and perhaps see
DEFABSSTOBJ).  Every stobj name among the formals of the function
must be listed, if the corresponding actual is to be treated as a
stobj.  That is, if a function uses a stobj name as a formal parameter
but the name is not declared among the :stobjs then the corresponding
argument is treated as ordinary.  The only exception to this rule is
state: whether you include it or not, state is always treated as a
single-threaded object.  This declaration has two effects.  One is to
enforce the syntactic restrictions on single-threaded objects.  The
other is to strengthen the guard of the function being defined so that
it includes conjuncts specifying that each declared single-threaded
object argument satisfies the recognizer for the corresponding
single-threaded object.

:VERIFY-GUARDS
Value is t or nil, indicating whether or not guards are to be verified
upon completion of the termination proof.  This flag should only be t
if the :mode is unspecified but the default defun mode is :logic, or
else the :mode is :logic.

:WELL-FOUNDED-RELATION
Value is a function symbol that is known to be a well-founded relation
in the sense that a rule of class :well-founded-relation has been
proved about it.  See WELL-FOUNDED-RELATION.

OTHER    other commonly used top-level functions

Related topics other than immediate subtopics:

This section contains an assortment of top-level functions that fit
into none of the other categories and yet are suffiently useful as to
merit "advertisement" in the :help command.

ACCUMULATED-PERSISTENCE    to get statistics on which runes are being tried

     Useful Forms:
     (accumulated-persistence t)              ; Activate statistics gathering.
     (accumulated-persistence :all)           ; As above, ``enhanced'' (see below)

     (show-accumulated-persistence :frames)   ; Display statistics ordered by
     (show-accumulated-persistence :tries)    ; frames built, times tried,
     (show-accumulated-persistence :ratio)    ; or their ratio.

     (accumulated-persistence nil)            ; Deactivate.

     Advanced forms:
     (show-accumulated-persistence :frames-s) ; The `s', `f', and `a' suffixes
     (show-accumulated-persistence :frames-f) ; stand for `success' (`useful'),
     (show-accumulated-persistence :frames-a) ; `failure' (`useless'), and `all',
     (show-accumulated-persistence :tries-s)  ; respectively.  The only effect of
     (show-accumulated-persistence :tries-f)  ; the `s' and `f' versions is to
     (show-accumulated-persistence :tries-a)  ; sort first by useful or useless
                                              ; applications, respectively (see
                                              ; below).  The `a' versions avoid
                                              ; showing the useful/useless
                                              ; breakdown.

     (show-accumulated-persistence :runes)    ; Just show runes alphabetically.

Related topics other than immediate subtopics:

Note: set-accumulated-persistence is equivalent to
accumulated-persistence.

See the end of this item for a discussion of "enhanced statistics
gathering," which can be useful for more fine-grained proof debugging.

Generally speaking, the more ACL2 knows, the slower it runs.  That is
because the search space grows with the number of alternative rules.
Often, the system tries to apply rules that you have forgotten were
even there, if you knew about them in the first place!
"Accumulated-persistence" is a statistic (originally developed for
Nqthm) that helps you identify the rules that are causing ACL2's search
space to explode.

For other proof debugging utilities, see BREAK-REWRITE and see
DMR.

Accumulated persistence tracking can be turned on or off.  It is
generally off.  When on, proofs may take perhaps 50% more time than
otherwise!  But some useful numbers are collected.  When it is turned
on, by

     ACL2 !>(accumulated-persistence t)

an accumulation site is initialized and henceforth data about which
rules are being tried is accumulated into that site.  That accumulated
data can be displayed with show-accumulated-persistence, as described
in detail below.  When accumulated persistence is turned off, with
(accumulated-persistence nil), the accumulation site is wiped out and
the data in it is lost.

The "accumulated persistence" of a rune is the number of runes the
system has attempted to apply (since accumulated persistence was last
activated) while the given rune was being tried.

Consider a :rewrite rule named rune.  For simplicity, let us imagine
that rune is tried only once in the period during which accumulated
persistence is being monitored.  Recall that to apply a rewrite rule we
must match the left-hand side of the conclusion to some term we are
trying to rewrite, establish the hypotheses of rune by rewriting, and,
if successful, then rewrite the right-hand side of the conclusion.  We
say rune is "being tried" from the time we have matched its left-hand
side to the time we have either abandoned the attempt or finished
rewriting its right-hand side.  (By "match" we mean to include any
loop-stopper requirement; see LOOP-STOPPER.)  During that
period of time other rules might be tried, e.g., to establish the
hypotheses.  The rules tried while rune is being tried are "billed" to
rune in the sense that they are being considered here only because of
the demands of rune.  Thus, if no other rules are tried during that
period, the accumulated persistence of rune is 1 -- we "bill" rune once
for its own application attempt.  If, on the other hand, we tried 10
rules on behalf of that application of rune, then rune's accumulated
persistence would be 11.

One way to envision accumulated persistence is to imagine that every
time a rune is tried it is pushed onto a stack.  The rules tried on
behalf of a given application of a rune are thus pushed and popped on
the stack above that rune.  A lot of work might be done on its behalf
-- the stack above the rune grows and shrinks repeatedly as the search
continues for a way to use the rune.  All the while, the rune itself
"persists" in the stack, until we finish with the attempt to apply it,
at which time we pop it off.  The accumulated persistence of a rune
application is thus the number of stack frames built while that rune
was on the stack.

Note that accumulated persistence is tallied whether or not the attempt
to apply a rune is successful.  Each of the rules tried on its behalf
might have failed and the attempt to apply the rune might have also
failed.  The ACL2 proof script would make no mention of the rune or the
rules tried on its behalf because they did not contribute to the proof.
But time was spent pursuing the possible application of the rune and
accumulated persistence is a measure of that time.

A high accumulated persistence might come about in two extreme ways.
One is that the rule causes a great deal of work every time it is
tried.  The other is that the rule is "cheap" but is tried very often.
We therefore keep track of the number of times each rule is tried as
well as its persistence.  The ratio between the two is the average
amount of work done on behalf of the rule each time it is tried.

When the accumulated persistence totals are displayed by the function
show-accumulated-persistence we sort them so that the most expensive
runes are shown first.  We can sort according to one of three basic
keys:

     :frames - the number of frames built on behalf of the rune
     :tries  - the number of times the rune was tried
     :ratio  - frames built per try

The key simply determines the order in which the information is
presented.  If no argument is supplied to show-accumulated-persistence,
:frames is used.

The display breaks each total into "useful" and "useless" subtotals.  A
"useful" rule try is one that is viewed as contributing to the progress
of the proof, and the rest are "useless" rule applications.  For
example, if a :rewrite rule is tried but its hypotheses are not
successfully relieved, then that rule application and all work done on
behalf of those hypotheses is "useless" work.  In general, an attempt
to apply a rune is viewed as "useful" unless the attempt fails or the
attempt is on the stack (as described above) for a rune application
that ultimately fails.  A large number of "useless" :frames or :tries
along with correspondingly small "useful" counts may suggest runes to
consider disabling (see DISABLE and see IN-THEORY).
Thus, here is a more complete list of the arguments that may be
supplied to show-accumulated-persistence.  Suffixes "s", "f", and "a"
are intended to suggest "success" ("useful"), "failure" ("useless"), and
"all".

     :frames     - sort by the number of frames built on behalf of the rune
        :frames-s -   as above, but sort by useful applications
        :frames-f -   as above, but sort by useless applications
        :frames-a -   as above, but inhibit display of ``useful'' and
                      ``useless'' subtotals
     :tries      - sort by the number of times the rune was tried
        :tries-s  -   as above, but sort by useful applications
        :tries-f  -   as above, but sort by useless applications
        :tries-a  -   as above, but inhibit display of ``useful'' and
                      ``useless'' subtotals
     :ratio      - sort by frames built per try
     :useless    - show only the runes tried whose tries were all ``useless''

For a given line of the report, every frame credited to a "useful"
(respectively, "useless") rule application is considered "useful"
(respectively, "useless").  We illustrate with the following example.

     (progn
       (defstub hyp (x) t)
       (defstub concl (x) t)
       (defstub bad (x) t)
       (defstub good (x) t)
       (defaxiom good-ax
         (implies (good x) (hyp x)))
       (defaxiom bad-ax
         (implies (bad x) (hyp x)))
       (defaxiom hyp-implies-concl
         (implies (hyp x) (concl x)))
       )
     (accumulated-persistence t)
     (thm (implies (good x) (concl x)))
     (show-accumulated-persistence)

To prove the thm form, ACL2 attempts to rewrite (concl x) to true by
applying rule hyp-implies-concl.  It then attempts to establish (hyp x)
first by trying rule bad-ax, which fails, and second by trying rule
good-ax, which succeeds.  As expected, the report labels as "useless"
the failure of the attempt to establish the hypothesis, (bad x).

        --------------------------------
              1        1 (    1.00) (:REWRITE BAD-AX)
              0        0    [useful]
              1        1    [useless]
        --------------------------------

Now consider the top-level application of rule hyp-implies-concl.  Even
though the above report shows the application of bad-ax as "useless",
note that this rule was applied on behalf of the successful ("useful")
application of hyp-implies-concl, and hence is incorporated into the
"useful" line for hyp-implies-concl, as follows.

        --------------------------------
              3        1 (    3.00) (:REWRITE HYP-IMPLIES-CONCL)
              3        1    [useful]
              0        0    [useless]
        --------------------------------

In summary: categorization of :frames as "useful" or "useless" is based
on whether they support "useful" or "useless" :tries.

Note that a rune with high accumulated persistence may not actually be
the "culprit."  For example, suppose rune1 is reported to have a :ratio
of 101, meaning that on the average a hundred and one frames were built
each time rune1 was tried.  Suppose rune2 has a :ratio of 100.  It
could be that the attempt to apply rune1 resulted in the attempted
application of rune2 and no other rune.  Thus, in some sense, rune1 is
"cheap" and rune2 is the "culprit" even though it costs less than rune1.

If a proof is aborted, then in general, show-accumulated-persistence
will only display totals for runes whose attempted application is
complete: that is, if the rewriter was in the process of relieving
hypotheses for a rule, then information for that rule will not be
included in the tally.  We say "in general" because, as indicated near
the top of the output from show-accumulated-persistence when such
incomplete information is omitted, you can get this information by
using argument :frames-a or :tries-a.

There are other subtleties in how rune applications are tallied,
documented elsewhere:  see ACCUMULATED-PERSISTENCE-SUBTLETIES.

We conclude with a discussion of "enhanced" statistics gathering, which
is enabled by supplying accumulated-persistence the argument :ALL:

     (accumulated-persistence :all)

At some additional performance expense (but probably well under a
factor of 2 altogether), ACL2 then gathers additional statistics for
individual hypotheses of rules as well as their conclusions.  To
understand how this works, suppose rn is a rune.  Then we prepend the
keyword :CONC to rn to form what we call its "conclusion xrune", and
for its I-th hypothesis we prepend :HYP I to rn to form its I-th
"hypothesis xrune."  Here, "xrune" is pronounced "ex rune", and is
mnemonic for "extended rune."  For example, if (REWRiTE FOO) is a rune
then (:CONC REWRiTE FOO) is its conclusion xrune, and (:HYP 2 REWRiTE
FOO) is a hypothesis xrune corresponding to the second hypothesis of the
corresponding rewrite rule.

With (accumulated-persistence :all), we instruct ACL2 to track not only
runes but also xrunes.  Then, (show-accumulated-persistence) will
display information for all xrunes in a format that we consider to be
"raw", in the sense that data for xrunes are displayed just as for
runes.  But a "merged" format is also available.  Here is a summary of
display commands, followed below by further discussion.

       (show-accumulated-persistence :frames t) ; t is optional, i.e., the default
          ; Display enhanced statistics sorted by frames, in a ``raw'' format.
       (show-accumulated-persistence :frames :merge)
          ; Display enhanced statistics sorted by frames, in a ``merged'' format.
       (show-accumulated-persistence :frames nil)
          ; Display regular statistics sorted by frames, without the enhancements.

       ; More generally, the descriptions just above apply for any legal first
       ; argument:

       (show-accumulated-persistence KEY t)
       (show-accumulated-persistence KEY :merge)
       (show-accumulated-persistence KEY nil)

       ; Note also these alternate forms, equivalent to the first of the two forms
       ; just above, i.e., the form with second argument of t:
       (show-accumulated-persistence KEY :raw)
       (show-accumulated-persistence KEY)

There is a significant difference between how runes are tracked and how
ACL2 tracks hypothesis and conclusion xrunes: unlike regular runes,
these xrunes do not contribute to the accumulated :frames counts.
Rather, they serve as accumulation sites without contributing their
:tries to any accumulation.  Consider for example the snippet below,
taken from a report created with the :merge option (to be discussed
further below), i.e., by evaluating the form
(show-accumulated-persistence :frames :merge).

        :frames   :tries    :ratio  rune
        --------------------------------
            462      211 (    2.18) (:REWRITE PERM-MEM)
             13        6    [useful]
            449      205    [useless]
           .............................
            251       47 (    5.34) (:HYP 2 :REWRITE PERM-MEM)
              6        6    [useful]
            245       41    [useless]
           .............................
              0      211 (    0.00) (:HYP 1 :REWRITE PERM-MEM)
              0        6    [useful]
              0      205    [useless]
           .............................
              0        7 (    0.00) (:CONC :REWRITE PERM-MEM)
              0        6    [useful]
              0        1    [useless]
        --------------------------------

Notice that while :tries are recorded for the xrune (:HYP 1 :REWRITE
PERM-MEM), no :frames are recorded.  This is because no stack frames
were built for runes while this xrune was on the stack -- only for the
xrune itself, which as we explained above is not accumulated into the
total :frames counts.  As it turns out, this lack of stack frames is
explained by the fact that the rewrite rule PERM-MEM has a free
variable in the first hypothesis.

     ACL2 !>:pe perm-mem
              18  (DEFTHM PERM-MEM
                          (IMPLIES (AND (PERM X Y) (MEM A X))
                                   (MEM A Y))
                          :RULE-CLASSES ((:REWRITE :MATCH-FREE :ONCE)))
     ACL2 !>

The second hypothesis, however, does cause additional rewriting in
order to rewrite it to true, resulting in 251 stack frames for runes.
We see that the conclusion does not lead to creation any rune stack
frames, which might seem to suggest that only 251 stack frames for
runes were created on behalf of this rule application -- yet, we see
that 462 frames were actually created.  The difference is the 211
frames created for the rewrite rule itself.  Even if the total had been
a bit more than 462, one need not be surprised, as there could be some
work recorded during application of the rewrite rule, such as
type-prescription reasoning, that is not done during rewriting of a
hypothesis or the conclusion.

Now suppose we have executed (accumulated-persistence :all) and
attempted some proofs, and now we are ready to see statistics.  The form
(show-accumulated-persistence) displays statistics exactly as described
above, treating these extra xrunes just as though they are runes;
similarly for the form (show-accumulated-persistence KEY), for any
legal KEY.  A second optional argument may however be supplied to
show-accumulated-persistence.  The default for that second argument is
t, and a second argument of :raw is treated the same as t; thus, these
arguments provide the behavior just described, where data for xrunes
are displayed just as for runes.  You may restrict output to runes,
ignoring hypothesis and conclusion xrunes, by giving a second argument
of nil.  (This gives the same behavior as if we had started with the
command (accumulated-persistence t) instead of the command
(accumulated-persistence :all).)  Finally, you may give a second
argument of :merge, in which case output will be sorted and displayed
as though only runes were tracked (not the extra xrunes), but each data
item for a non-rune xrune will be merged so that it is displayed in
suitable order just below its corresponding rune, as in the PERM-MEM
example displayeda above.

We close by mentioning two aspect of enhanced statistics display for
:CONC xrunes that have potential to be confusing.  First consider the
following example.

          :frames   :tries    :ratio  rune
        --------------------------------
             14        4 (    3.50) (:REWRITE DEFAULT-+-2)
              0        0    [useful]
             14        4    [useless]
           .............................
             10        4 (    2.50) (:HYP 1 :REWRITE DEFAULT-+-2)
              0        0    [useful]
             10        4    [useless]
        --------------------------------

It may be surprising that no data is displayed for the corresponding
:CONC xrune.  The explanation, however, is simple: the hypothesis never
rewrote to true, so the conclusion was never rewritten.  This is
consistent with the marking as "useless" of all :frames and :tries for
the rune and the hypothesis xrune.  Note by the way, once again, that
the hypothesis xrune does not contribute to any :frames count.

Another reason not to see data displayed for a :CONC xrune is that if a
rule has no hypotheses, then no such data is collected.  This decision
was made because in the case of no hypotheses, we expect it to be very
rare that information for the :CONC xrune will add any useful insight.

On a final note: (show-accumulated-persistence :runes) may be used
simply to see a list of all runes (or xrunes) displayed alphabetically.

Users are encouraged to think about other meters we could install in
ACL2 to help diagnose performance problems.

ACCUMULATED-PERSISTENCE-SUBTLETIES    some subtle aspects of the counting done by accumulated-persistence

In this topic we cover the overcounting of "useful" and of recursive
rune application attempts, and we describe how "useless" rune
application attempts can actually be critical for a proof's success.

_Overcounting of "useful" and of recursive rune application attempts._
Not every rune application may be necessary for a proof's success.
Consider for example:

     (thm (equal (car (cons a (cdr (cons b x))))
                 a))

Then show-accumulated-persistence will tell us that :rewrite rules
car-cons and cdr-cons each had one useful application.  However, the
rule cdr-cons is used to simplify (cdr (cons b x)) to x, and this
simplification is unecessary for the proof.  Indeed, the proof succeeds
even when preceded by the event: (in-theory (disable cdr-cons)).  We
thus see that a rune application labeled as "useful" may be simplifying
a term that is not relevant to the proof.

As of this writing, we consider every :forward-chaining rule
application to be "useful", for simplicity of the implementation.
Moreover, our counting of these rules is such that a single rule may be
counted more than once.

Next we show how recursive rule applications are overcounted.  Consider
the following example.

     (defun mem (a x)
       (if (atom x)
           nil
         (or (equal a (car x)) (mem a (cdr x)))))

Now suppose we consider the sequence of theorems (mem a (list a)), (mem
a (list 1 a)), (mem a (list 1 2 a)), (mem a (list 1 2 3 a)), and so on.
We will see that the :frames reported for each increases quadratically,
even though the :tries increases linearly; so in this case the :tries
statistics are more appropriate.  Each time the definition of mem is
applied, a new stack frame is pushed (see
ACCUMULATED-PERSISTENCE), and all subsequent applications of that
definition are accumulated into the :frames count for that stack frame.
The final :frames count will be the sum of the counts for those
individual frames, which form a linear sequence whose sum is therefore
quadratic in the number of applications of the definition of mem.

_How "useless" attempts can be critical for a proof's success._  The
command (accumulated-persistence :useless)] will list rules that did not
contribute directly to the proof (see ACCUMULATED-PERSISTENCE,
in particular the discussion of "useless" there).  However, a "useless"
rule can on rare occasions be critical to the success of a proof.  In
the following example, we have a "bad" rule that can take the proof in
the wrong direction, but a "useless" rule does a rewrite that prevents
the succesful relieving of a hypothesis of the "bad" rule.  In summary:

     ; Assume p0.  We want to prove p1.

     ; Key rule:
     p0 -> p1 = t

     ; Bad rule that could ruin the proof:
     p3 -> p1 = p2

     ; But unfortunately, we know p3:
     p0 -> p3

     ; Important ``useless'' rule, preventing ``bad rule'' above from firing:
     p3 = p4

The following event captures the rules described above.

     (encapsulate
      ((p0 (x) t)
       (p1 (x) t)
       (p2 (x) t)
       (p3 (x) t)
       (p4 (x) t))
      (local (defun p0 (x) x))
      (local (defun p1 (x) x))
      (local (defun p2 (x) x))
      (local (defun p3 (x) x))
      (local (defun p4 (x) x))

     ; Key rule:
      (defthm p0-implies-p1
        (implies (p0 x)
                 (p1 x)))

     ; Bad rule that could ruin the proof:
      (defthm p3-implies-p1-is-p2
        (implies (p3 x)
                 (equal (p1 x) (p2 x))))

     ; But unfortunately, we know p3:
      (defthm p0-implies-p3
        (implies (p0 x)
                 (p3 x)))

     ; Important ``useless'' rule, preventing p3-implies-p1-is-p2 from firing:
      (defthm p3-is-p4
        (equal (p3 x) (p4 x))))

Now we can see that p3-is-p4 is labeled as "useless", by evaluating
these commands.

     (accumulated-persistence t)
     (thm (implies (p0 x) (p1 x)))
     (show-accumulated-persistence)

If instead we first evaluate (in-theory (disable p3-is-p4)) before the
thm above, then the proof fails, even though p3-is-p4 was labeled as
"useless"!

Nevertheless, in general it is probably safe to disable rules reported
as "useless" by (show-accumulated-persistence :useless), and doing so
may speed up a proof considerably.

Remark. The example above suggests a surprising fact: on rare
occasions, a proof may fail when you give an :in-theory hint consisting
of exactly the runes reported in a proof that succeeds.  For, imagine a
rule R that is needed in part of the proof but is "bad" in a second
part, and that some other, "useless" rule prevents the application of R
in that second part.  The example above suggests that disabling this
"useless" rule can allow the second application of R, thus preventing
the proof.

ACL2-DEFAULTS-TABLE    a table specifying certain defaults, e.g., the default defun-mode

     Example Forms:
     (table acl2-defaults-table :defun-mode) ; current default defun-mode
     (table acl2-defaults-table :defun-mode :program)
                ; set default defun-mode to :program

See TABLE for a discussion of tables in general.  The legal
keys for this table are shown below.  They may be accessed and changed
via the general mechanisms provided by tables.  However, there are
often more convenient ways to access and/or change the defaults.  (See
also the note below.)

     :defun-mode

the default defun-mode, which must be :program or :logic.  See
DEFUN-MODE for a general discussion of defun-modes.  The :defun-mode
key may be conveniently set by keyword commands naming the new
defun-mode, :program and :logic.  See PROGRAM and see
LOGIC.

     :enforce-redundancy

if t, cause ACL2 to insist that most events are redundant (see
REDUNDANT-EVENTS); if :warn, cause a warning instead of an error for
such non-redundant events; else, nil.  See
SET-ENFORCE-REDUNDANCY.

     :ignore-doc-string-error

if t, cause ACL2 to ignore ill-formed documentation strings rather than
causing an error; if :warn, cause a warning instead of an error in such
cases; else, nil (the default).  See
SET-IGNORE-DOC-STRING-ERROR.

     :verify-guards-eagerness

an integer between 0 and 2 indicating how eager the system is to verify
the guards of a defun event.  See SET-VERIFY-GUARDS-EAGERNESS.

     :compile-fns

When this key's value is t, functions are compiled when they are
defun'd; otherwise, the value is nil.  (Except, this key's value is
ignored when explicit compilation is suppressed; see
COMPILATION.)  To set the flag, see SET-COMPILE-FNS.

     :measure-function

the default measure function used by defun when no :measure is supplied
in xargs.  The default measure function must be a function symbol of
one argument. Let mfn be the default measure function and suppose no
:measure is supplied with some recursive function definition.  Then
defun finds the first formal, var, that is tested along every branch
and changed in each recursive call.  The system then "guesses" that
(mfn var) is the :measure for that defun.

     :well-founded-relation

the default well-founded relation used by defun when no
:well-founded-relation is supplied in xargs.  The default well-founded
relation must be a function symbol, rel, of two arguments about which a
:well-founded-relation rule has been proved.  See
WELL-FOUNDED-RELATION.

     :bogus-defun-hints-ok

When this key's value is t, ACL2 allows :hints for nonrecursive
function definitions.  Otherwise, the value is the nil (the default) or
:warn (which makes the check but merely warns when the check fails).
See SET-BOGUS-DEFUN-HINTS-OK.

     :bogus-mutual-recursion-ok

When this key's value is t, ACL2 skips the check that every function in
a mutual-recursion (or defuns) "clique" calls at least one other
function in that "clique."  Otherwise, the value is nil (the default)
or :warn (which makes the check but merely warns when the check fails).
See SET-BOGUS-MUTUAL-RECURSION-OK.

     :irrelevant-formals-ok

When this key's value is t, the check for irrelevant formals is
bypassed; otherwise, the value is the keyword nil (the default) or
:warn (which makes the check but merely warns when the check fails).
See IRRELEVANT-FORMALS and see
SET-IRRELEVANT-FORMALS-OK.

     :ignore-ok

When this key's value is t, the check for ignored variables is
bypassed; otherwise, the value is the keyword nil (the default) or
:warn (which makes the check but merely warns when the check fails).
See SET-IGNORE-OK.

     :inhibit-warnings

ACL2 prints warnings that may, from time to time, seem excessive to
experienced users.  Each warning is "labeled" with a string identifying
the type of warning.  Consider for example

     ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE ....

Here, the label is "Use".  The value of the key :inhibit-warnings is a
list of such labels, where case is ignored.  Any warning whose label is
a member of this list (where again, case is ignored) is suppressed.
See SET-INHIBIT-WARNINGS and also see
SET-INHIBIT-OUTPUT-LST.

     :bdd-constructors

This key's value is a list of function symbols used to define the
notion of "BDD normal form."  See BDD-ALGORITHM and see
HINTS.

     :ttag

This key's value, when non-nil, allows certain operations that extend
the trusted code base beyond what is provided by ACL2.  See
DEFTTAG.  See DEFTTAG.

     :state-ok

This key's value is either t or nil and indicates whether the user is
aware of the syntactic restrictions on the variable symbol STATE.  See
SET-STATE-OK.

     :backchain-limit

This key's value is a list of two "numbers."  Either "number" may
optionally be nil, which is treated like positive infinity.  The
numbers control backchaining through hypotheses during type-set
reasoning and rewriting.  See BACKCHAIN-LIMIT.

     :default-backchain-limit

This key's value is a list of two "numbers."  Either "number" may
optionally be nil, which is treated like positive infinity.  The
numbers are used respectively to set the backchain limit of a rule if
one has not been specified. See BACKCHAIN-LIMIT.

     :step-limit

This key's value is either nil or a natural number not exceeding the
value of *default-step-limit*.  If the value is nil or the value of
*default-step-limit*, there is no limit on the number of "steps" that
ACL2 counts during a proof: currently, the number of top-level rewriting
calls.  Otherwise, the value is the maximum number of such calls allowed
during evaluation of any event.  See SET-PROVER-STEP-LIMIT.

     :rewrite-stack-limit

This key's value is a nonnegative integer less than (expt 2 28).  It is
used to limit the depth of calls of ACL2 rewriter functions.  See
REWRITE-STACK-LIMIT.

     :let*-abstractionp

This key affects how the system displays subgoals.  The value is either
t or nil.  When t, let* expressions are introduced before printing to
eliminate common subexpressions.  The actual goal being worked on is
unchanged.

     :nu-rewriter-mode

This key's value is nil, t, or :literals.  When the value is non-nil,
the rewriter gives special treatment to expressions and functions
defined in terms of nth and update-nth.  See set-nu-rewriter-mode.

     :case-split-limitations

This key's value is a list of two "numbers."  Either "number" may
optionally be nil, which is treated like positive infinity.  The
numbers control how the system handles case splits in the simplifier.
See SET-CASE-SPLIT-LIMITATIONS.

     :include-book-dir-alist

This key's value is used by include-book's :DIR argument to associate a
directory with a keyword.  An exception is the keyword :SYSTEM for the
distributed ACL2 books/ directory; see INCLUDE-BOOK, in
particular the section on "Books Directory."

     :match-free-default

This key's value is either :all, :once, or nil.  See
SET-MATCH-FREE-DEFAULT.

     :match-free-override

This key's value is a list of runes.  See
ADD-MATCH-FREE-OVERRIDE.

     :match-free-override-nume

This key's value is an integer used in the implementation of
add-match-free-override, so that only existing runes are affected by
that event.

     :non-linearp

This key's value is either t or nil and indicates whether the user
wishes ACL2 to extend the linear arithmetic decision procedure to
include non-linear reasoning.  See NON-LINEAR-ARITHMETIC.

     :tau-auto-modep

This key's value is either t or nil and indicates whether the user
wishes ACL2 to look for opportunities to create :tau-system rules from
all suitable defuns and from all suitable defthms (with non-nil
:rule-classes).  See SET-TAU-AUTO-MODE.

     :ruler-extenders

This key's value may be a list of symbols, indicating those function
symbols that are not to block the collection of rulers; see
DEFUN.  Otherwise the value is :all to indicate all function symbols,
i.e., so that no function symbol blocks the collection of rulers.  If a
list is specified (rather than :all), then it may contain the keyword
:lambdas, which has the special role of specifying all lambda
applications.  No other keyword is permitted in the list.  See
RULER-EXTENDERS.

     :memoize-ideal-okp

This key is only legal in an experimental hons version (see
HONS-AND-MEMOIZATION).  Its value must be either t, nil, or :warn.
If the value is nil or not present, then it is illegal by default to
memoize a :logic mode function that has not been guard-verified (see
VERIFY-GUARDS), sometimes called an "ideal-mode" function.
This illegality is the default because such calls of such functions in
the ACL2 loop are generally evaluated in the logic (using so-called
"executable counterpart" definitions), rather than directly by
executing calls of the corresponding (memoized) raw Lisp function.
However, such a raw Lisp call can be made when the function is called
by a :program mode function, so we allow you to override the default
behavior by associating the value t or :warn with the key
:memoize-ideal-okp, where with :warn you get a suitable warning.  Note
that you can also allow memoization of ideal-mode functions by supplying
argument :ideal-okp to your memoization event (see MEMOIZE), in
which case the value of :memoize-ideal-okp in the acl2-defaults-table is
irrelevant.

Note: Unlike all other tables, acl2-defaults-table can affect the
soundness of the system.  The table mechanism therefore enforces on it
a restriction not imposed on other tables: when table is used to update
the acl2-defaults-table, the key and value must be variable-free forms.
Thus, while

     (table acl2-defaults-table :defun-mode :program),

     (table acl2-defaults-table :defun-mode ':program), and

     (table acl2-defaults-table :defun-mode (compute-mode *my-data*))

are all examples of legal events (assuming compute-mode is a function
of one non-state argument that produces a defun-mode as its single
value),

     (table acl2-defaults-table :defun-mode (compute-mode (w state)))

is not legal because the value form is state-sensitive.

Consider for example the following three events which one might make
into the text of a book.

     (in-package "ACL2")

     (table acl2-defaults-table
       :defun-mode
       (if (ld-skip-proofsp state) :logic :program))

     (defun crash-and-burn (x) (car x))

The second event is illegal because its value form is state-sensitive.
If it were not illegal, then it would set the :defun-mode to :program
when the book was being certified but would set the defun-mode to
:logic when the book was being loaded by include-book.  That is because
during certification, ld-skip-proofsp is nil (proof obligations are
generated and proved), but during book inclusion ld-skip-proofsp is
non-nil (those obligations are assumed to have been satisfied.)  Thus,
the above book, when loaded, would create a function in :logic mode that
does not actually meet the conditions for such status.

For similar reasons, table events affecting acl2-defaults-table are
illegal within the scope of local forms.  That is, the text

     (in-package "ACL2")

     (local (table acl2-defaults-table :defun-mode :program))

     (defun crash-and-burn (x) (car x))

is illegal because acl2-defaults-table is changed locally.  If this
text were acceptable as a book, then when the book was certified,
crash-and-burn would be processed in :program mode, but when the
certified book was included later, crash-and-burn would have :logic
mode because the local event would be skipped.

The text

     (in-package "ACL2")

     (program) ;which is (table acl2-defaults-table :defun-mode :program)

     (defun crash-and-burn (x) (car x))

is acceptable and defines crash-and-burn in :program mode, both during
certification and subsequent inclusion.

We conclude with an important observation about the relation between
acl2-defaults-table and include-book, certify-book, and encapsulate.
Including or certifying a book never has an effect on the
acl2-defaults-table, nor does executing an encapsulate event; we always
restore the value of this table as a final act.  (Also see
INCLUDE-BOOK, see ENCAPSULATE, and see CERTIFY-BOOK.)
That is, no matter how a book fiddles with the acl2-defaults-table, its
value immediately after including that book is the same as immediately
before including that book.  If you want to set the acl2-defaults-table
in a way that persists, you need to do so using commands that are not
inside books.  It may be useful to set your favorite defaults in your
acl2-customization file; see ACL2-CUSTOMIZATION.

ACL2-HELP    the acl2-help mailing list

You can email questions about ACL2 usage to the acl2-help mailing list:
acl2-help@utlists.utexas.edu.  If you have more general questions about
ACL2, for example, about projects completed using ACL2, you may prefer
the acl2 mailing list, acl2@utlists.utexas.edu, which tends to have
wider distribution.

CERTIFY-BOOK!    a variant of certify-book

     Examples:
     (certify-book! "my-arith" 3)     ;Certify in a world with 3
                                        ; commands, starting in a world
                                        ; with at least 3 commands.
     (certify-book! "my-arith")       ;Certify in the initial world.

     General Form:
     (certify-book! book-name k compile-flg)

where book-name is a book name (see BOOK-NAME), k is a
nonnegative integer used to indicate the "certification world," and
compile-flg indicates whether you wish to compile the (functions in
the) book.

This command is identical to certify-book, except that the second
argument k may not be t in certify-book! and if k exceeds the current
command number, then an appropriate ubt! will be executed first.  See
CERTIFY-BOOK and see UBT!.

CW-GSTACK    debug a rewriting loop or stack overflow

     Example Forms:
     (cw-gstack)
     (cw-gstack :frames 10)       ; show only the top 10 frames
     (cw-gstack :frames '(1 10))  ; same as above:  show only frames 1 through 10
     (cw-gstack :frames '(10 20)) ; show only frames 10 through 20
     (cw-gstack :evisc-tuple (evisc-tuple 3 4 nil nil))
                                  ; print with print-level 3 and print-length 4
     (cw-gstack :evisc-tuple nil) ; print using default ``evisceration'',
                                  ;   essentially the same as just above
     (cw-gstack :evisc-tuple '(nil 3 4 (hide)))
                                  ; same as just above

     General Form:
     (cw-gstack :frames frames :evisc-tuple evisc-tuple)

where :frames and :evisc-tuple are optional, but if they are supplied,
their values are evaluated.  The value of frames should be either a
natural number or a list of two natural numbers, the first less than
the second; and the value of evisc-tuple should be an evisc-tuple (see
EVISC-TUPLE).  If :evisc-tuple is omitted, then substructures
deeper than 3 are replaced by "#" and those longer than 4 are replaced
by "...", and terms of the form (hide ...) are printed as <hidden>.
Also see SET-IPRINT for an alternative to printing "#" and
"...".

Stack overflows may occur, perhaps caused by looping rewrite rules.  In
some Lisps, especially GCL, stack overflows often manifest themselves as
segmentation faults, causing the entire ACL2 image to crash.  Finding
looping rewrite rules can be tricky, especially if you are using books
supplied by other people.  (However, see
SET-REWRITE-STACK-LIMIT for a way to avoid stack overflows caused by
rewriter loops.)

A wonderful trick is the following.  When there is a stack overflow
during a proof, abort and then try it again after turning on rewrite
stack monitoring with :brr t.  When the stack overflows again, exit to
raw Lisp.  How you exit to raw Lisp depends on which Lisp you are
using.  In Allegro Common Lisp, for example, the stack overflow will
leave you in an interactive break.  It is often a good idea to exit the
break immediately (e.g., using :pop if you use Allegro Common Lisp, or
:q using GCL), which will leave you in the top-level ACL2 command loop,
after which it is recommended to leave that loop using :q.  That will
leave you in raw Lisp.  Then, execute

     (cw-gstack)

If the loop is in the rewriter, it will probably be evident!  You can
re-enter the ACL2 loop now with (lp).

If you are in GCL the stack overflow may cause a segmentation fault and
abort the Lisp job.  This makes it harder to debug but here is what you
do.  First, re-create the situation just prior to submitting the form
that will cause the stack overflow.  You can do this without suffering
through all the proofs by using the :ld-skip-proofsp option of ld to
reload your scripts.  Before you submit the form that causes the stack
overflow, exit the ACL2 command loop with :q.  In raw GCL type:

     (si::use-fast-links nil)

This will slow GCL down but make it detect and signal stack overflows
rather than overwrite the system memory.  Now reenter the ACL2 command
loop with (lp).

Now carry on as described above, turning on rewrite stack monitoring
with :brr t and provoking the stack overflow.  When it occurs, you will
be in an interactive break.  Exit to raw Lisp with two successive :q's,
one to get out of the error break and the next to get out of the
top-level ACL2 command loop.  Then in raw GCL execute (cw-gstack).

Suggestion: Once you have found the loop and fixed it, you should
execute the ACL2 command :brr nil, so that you don't slow down
subsequent proof attempts.  If you are in GCL, you should also get into
raw Lisp and execute (si::use-fast-links t).

DEAD-EVENTS    using proof supporters to identify dead code and unused theorems

Below, when we talk about "an event A", we mean an event whose name is
A.

When event A is used in a proof performed to admit event B that you
submit to ACL2, we say that A is a "proof-supporter" of B.  ACL2 stores
an association list such that for every event B with at least one
proof-supporter, B is associated with a list of all of its
proof-supporters, sorted by symbol-<.  The following form evaluates to
that alist, which is called the "proof-supporters-alist".

     (global-val 'proof-supporters-alist (w state))

By "used in a proof" above, we mean: applied as a rule or supplied
explicitly via hints of type :use, :by, or :clause-processor.  That is,
the events "used in a proof" for admitting an event E are those listed
in the summary printed at the conclusion of admitting E.

Note that if proofs are skipped when admitting event E, say because the
last admission of E was done by include-book (or certify-book, which
ends with an include-book), then there will be no entry in that alist
for E.  (An exception is made however for encapsulate events, where
proof-supporters are remembered from the first pass; see below.)  So if
you want the proof-supporters-alist to include supporters for events in
a book, use ld rather than include-book or certify-book to process the
events in that book.  If however you are interested in the
proof-supporters FROM a book that support a later event, then it is
fine to include that book.

The case for encapsulate is slightly tricky.  Consider an example of
the following form.

     A ; event preceding the encapsulate
     (encapsulate
      ()
      B
      (local C) ; uses A and B in a proof
      D ; uses C in a proof
      )

At the conclusion of this encapsulate event, the proof-supporters-alist
associates D with A and B, but not C (which has disappeared, since it
is local).

Note that this sort of "transitive closure" operation is only performed
when necessary due to the disappearance of local events.  For example,
if we replace (local C) above by just C, then D is associated in the
proof-supporters-alist only with C, not with A or B.  If you want the
transitive closure of the relation computed by the
proof-supporters-alist, you have to compute it yourself. (This was a
deliberate design decision, in order to avoid slowing down event
processing.)  However, there is help available on how to do such a
computation:

A distributed book, books/misc/dead-events.lisp, does such a transitive
closure, and moreover uses that information to find "dead events"
relative to a list of "desired" events.  For example, suppose you use
LD to process the events, with proofs, in a book intended to prove
theorems MAIN-1 and MAIN-2.  (Remember, certify-book will not save such
information.)  Suppose furthermore that the book begins with some
include-book forms followed by (deflabel book-start).  You could
evaluate this form:

     (dead-events '(main-1 main-2) :start 'book-start)

The result is a list of events that you probably can delete from the
book without causing any proofs to fail.  See the dead-events.lisp book
for further documentation.

You might also find the code in the above book to be helpful for
writing your own utilities based on the proof-supporters-alist.

DISASSEMBLE$    disassemble a function

The macro disassemble$ provides a convenient interface to the underlying
disassemble utility of the host Common Lisp implementation, which prints
assembly code for a given function symbol at the terminal.  It works by
including the distributed book books/misc/disassemble.lisp, which
defines the supporting function disassemble$-fn, and then by calling
that function.  Note that the arguments to disassemble$ are evaluated.
Also note that disassemble$ is intended as a top-level utility for the
ACL2 loop, not to be called in code; for such a purpose, include the
above book and call disassemble$-fn directly.

     Example Forms:

     (disassemble$ 'foo)
     (disassemble$ 'foo :recompile t)

     General Forms:
     (disassemble$ form)
     (disassemble$ form :recompile flg)

where form evaluates to a function symbol and flg evaluates to any
value.  If flg is nil, then the existing definition of that function
symbol is disassembled.  But if flg is supplied and has a value other
than nil or :default, and if that function symbol is defined in the
ACL2 loop (not merely in raw Lisp; for example, see
SET-RAW-MODE), then the disassembly will be based on a recompilation
of that ACL2 definition.  Normally this recompilation is not necessary,
but for some host Lisps, it may be useful; in particular, for CCL the
above book arranges that source code information is saved, so that the
output is annotated with such information.  When recompilation takes
place, the previous definition is restored after disassembly is
complete.  Finally, if flg is omitted or has the value :default --
i.e., in the default case -- then recompilation may take place or not,
depending on the host Lisp.  The values of (@ host-lisp) for which
recompilation takes place by default may be found by looking at the
above book, or by including it and evaluating the constant
*host-lisps-that-recompile-by-default*.  As of this writing, CCL is the
only such Lisp (because that is the one for which we can obtain source
annotation in the output by recompiling).

DMR    dynamically monitor rewrites and other prover activity

In addition to utilities that allow you to set breakpoints or print
rewriting information to the screen -- see BREAK-REWRITE --
ACL2 provides a utility for watching the activity of the rewriter and
some other proof processes, in real time.  This utility is called
"dmr", which is an acronym for "dynamically monitor rewrites".  The
utility comes in two parts: an ACL2 component that frequently writes a
file (the "dmr file") containing the relevant information, and an Emacs
component that frequently displays the contents of that file in an
Emacs buffer (the "dmr buffer").  Other editors could, in principle, be
programmed to display that file; anyone developing such a capability is
invited to contribute it to the ACL2 community.

The dmr utility can be extremely helpful for expensive proofs,
especially when ACL2 is not providing any output.  The break-rewrite and
accumulated-persistence utilities may be a bit easier to use, so you
might want to try those first.  But the dmr utility can be a very
helpful debugging aide, as it can visually give you a sense of where
ACL2 is spending its time.

The Emacs portion of this utility is already loaded if you load the
distributed Emacs file emacs/emacs-acl2.el.  Otherwise, invoke the
following Emacs command, say by typing Control-X Control-E after the
right parenthesis, where DIR is the directory of your ACL2 distribution.

     (load "<DIR>/emacs/monitor.el") ; absolute pathnames might work best

You only need to do that once.  Then each time you want to observe the
rewriter in action, invoke the following to see it displayed in a
buffer, which we call the "dmr buffer":

     Control-t 1

But first you will need to enable monitoring at the ACL2 level:

     (dmr-start)

Monitoring has some cost.  So if you have started it, then at some
point you may want to turn it off when not using it.  Any time the dmr
buffer (generally called "acl2-dmr-<user_name>") is not visible, Emacs
monitoring is turned off.  You can also turn off Emacs monitoring
explicitly, with:

     Control-t 2

At the ACL2 level you can disable monitoring as follows:

     (dmr-stop)

_Interpreting the dmr buffer display._

We explain the dmr buffer display by way of the following example.  It
is a snapshot of a dmr buffer taken from one of the distributed
workshop books,
books/workshops/2004/legato/support/proof-by-generalization-mult.lisp.

      0. (DEFTHM . WP-ZCOEF-G-MULTIPLIES)
      1. SIMPLIFY-CLAUSE
        2. Rewriting (to simplify) the atom of literal 18; argument(s) 1
        4. Rewriting (to simplify) the expansion; argument(s) 3|2
        7. Applying (:DEFINITION WP-ZCOEF-G)
     *  8. Rewriting (to simplify) the rewritten body; argument(s) 2|1|2|2
     *  13. Applying (:REWRITE MOD-ZERO . 2)
     *    14. Rewriting (to establish) the atom of hypothesis 4
     *    15. Applying (:META META-INTEGERP-CORRECT)

Each line indicates an ACL2 activity that leads to the activity shown
on the line just below it.  Moreover, lines are sometimes collapsed to
make the display more compact.  Consider for example the first few
lines.  Above, we are proving a theorem named WP-ZCOEF-G-MULTIPLIES.
Lines 1 and 2 show the clause simplification process invokes the
rewriter on the 18th literal.  (Recall that a clause is a disjunction
of literals; for example the clause {(NOT A), (NOT B), C} would be
displayed as (IMPLIES (AND A B) C).)  This 18th literal mentioned on
line 2 is a function call (f arg1 ...), and "argument(s) 1" indicates
that the rewriter, which works inside-out, is considering the first
argument ("arg1").  Thus the display could instead have shown the
following.

        2. Rewriting (to simplify) the atom of literal 18
        3. Rewriting (to simplify) the first argument
        4. Rewriting (to simplify) the expansion; argument(s) 3|2

But it saved space to combine lines 2 and 3.  Line 4 suggests that the
above arg1 is a function call that has been opened up because of an
:expand hint or, perhaps, an expansion directed explicitly by the
prover (as can happen during induction).  The annotation "argument(s)
3|2" then indicates that the rewriter is diving into the third argument
of the expansion, and then into the second argument of that.  Let us
call the result term7 (since it is the one to be considered on line 7).

Now consider the next two lines:

        7. Applying (:DEFINITION WP-ZCOEF-G)
     *  8. Rewriting (to simplify) the rewritten body; argument(s) 2|1|2|2

Line 7 is saying that term7 (defined above) is modified by applying the
definition of WP-ZCOEF-G to it.  Line 8 then says that the body of this
definition has been rewritten (with its formals bound to the actuals
from term7) and the rewriter is diving into the subterms of that
rewritten body, as indicated.  Notice also that line 8 is the first
line marked with an asterisk ("*") in the margin.  This line is the
first that is different from what was shown the previous time the
display was updated (about 1/10 second earlier, by default).  When a
line is marked with an asterisk, so are all the lines below it; so the
lines without an asterisk are those that have been stable since the
last display.  In this example we may see line 7 marked without an
asterisk for a while, which suggests that the rule (:DEFINITION
WP-ZCOEF-G) is expensive.  (Also see ACCUMULATED-PERSISTENCE.)
In general, a line that persists for awhile without a leading asterisk
can suggest why the proof is taking a long time.

Finally, note the indentation of line 14 relative to line 13.  Extra
indentation occurs when an attempt is being made to relieve a hypothesis
(i.e., rewrite it to t).  In particular, rewrites that will be
incorporated directly into a (top-level) literal are all indented just
two spaces, starting with the first rewrite directly under a process
such as SIMPLIFY-CLAUSE (shown line 1 above).  If the indentation is at
least the value of raw Lisp variable *dmr-indent-max* (by default, 20),
then indenttion is restricted to that column, but ACL2 prints {n} where
n is the column that would have been used for indentation if there were
no maximum.

You can move the cursor around in the dmr buffer even while it is being
updated.  But emacs will attempt to keep the cursor no later than the
first asterisk ("*") in the margin.  Thus, you can move the cursor
around in the stable part of the display, and emacs will keep the
cursor in that stable part.

WARNING: Things could go terribly wrong if the same user runs two
different ACL2 sessions with dmr active, because the same file will be
written by two different ACL2 processes.

WARNING: For dmr to work, emacs and ACL2 need to be run on the same
machine because the file used to communicate between ACL2 and emacs is
under /tmp.  Except, you can probably hack around that restriction by
changing *dmr-file-name* in ACL2 (in raw Lisp) and correspondingly in
Emacs file monitor.el.

More generally, advanced users are welcome to search for the string

     User-settable dmr variables

in ACL2 files interface-raw.lisp and emacs/monitor.el in order to
customize their dmr environments.

In order to update the dmr file with the latest stack information,
interrupt ACL2 and then evaluate: (dmr-flush).  In order to support
resumption of the interrupted proof (assuming your host Common Lisp
supports resumption), evaluation of (dmr-start) automatically causes
evaluation of the form (set-debugger-enable t); see
SET-DEBUGGER-ENABLE.

Note for users of the experimental extension ACL2(p) (see
PARALLELISM): when waterfall-parallelism has been set to a non-nil
value (see SET-WATERFALL-PARALLELISM), statistics about
parallel execution are printed instead of the usual information.

DYNAMICALLY-MONITOR-REWRITES    See DMR.

EXIT    quit entirely out of Lisp

Same as good-bye.

GOOD-BYE    quit entirely out of Lisp

     Examples:
     ACL2 !>(good-bye)
     ; [ACL2 is exited]

     ACL2 !>(good-bye 3)
     ; [ACL2 is exited with Unix exit status 3]

Note:  Your entire session will disappear forever when you evaluate
(good-bye).

The command (good-bye) quits not only out of the ACL2 command loop, but
in fact quits entirely out of the underlying Lisp.  Thus, there is no
going back!  You will *not* be able to re-enter the command loop after
typing (good-bye)!  All your work will be lost!!!

This command may not work in some underlying Common Lisp
implementations.  In such cases, there is no harm in trying; ACL2 will
let you know how to proceed if it cannot exit.

In some systems, typing control-d at the top-level ACL2 prompt
(control-c control-d if inside emacs) will call this function.

If you give good-bye an argument, it should be a natural number, and it
indicates the Unix (Linux) exit status.

If you merely want to exit the ACL2 command loop, use :q instead (see
Q).

GUARD-OBLIGATION    the guard proof obligation

See VERIFY-GUARDS, and see GUARD for a discussion of
guards.  Also see VERIFY-GUARDS-FORMULA for a utility provided
for viewing the guard proof obligation, without proof.
Guard-obligation is a lower level function for use in system programs,
not typically appropriate for most ACL2 users.  If you simply want to
see the guard proof obligations, see VERIFY-GUARDS-FORMULA.

     Example Form:
     (guard-obligation 'foo nil 'top-level state)
     (guard-obligation '(if (consp x) (foo (car x)) t) nil 'my-function state)

     General Forms:
     (guard-obligation name guard-debug ctx state)
     (guard-obligation term guard-debug ctx state)

where the first argument is either the name of a function or theorem or
is a non-variable term that may be in untranslated form; guard-debug is
typically nil but may be t (see GUARD-DEBUG); ctx is a context
(typically, a symbol used in error and warning messages); and state
references the ACL2 state.

If you want to obtain the formula but you don't care about the so-called
"tag tree":

     (mv-let (erp val state)
             (guard-obligation x guard-debug 'top-level state)
             (if erp
                ( .. code for handling error case, e.g., name is undefined .. )
               (let ((cl-set (cadr val))) ; to be proved for guard verification
                 ( .. code using cl-set, which is a list of clauses,
                      implicitly conjoined, each of which is viewed as
                      a disjunction .. ))))

The form (guard-obligation x guard-debug ctx state) evaluates to a
triple (mv erp val state), where erp is nil unless there is an error,
and state is the ACL2 state.  Suppose erp is nil.  Then val is the
keyword :redundant if the corresponding verify-guards event would be
redundant; see REDUNDANT-EVENTS.  Otherwise, val is a tuple
(list* names cl-set ttree), where: names is (cons :term xt) if x is not
a variable, where xt is the translated form of x; and otherwise is a
list containing x along with, if x is defined in a mutual-recursion,
any other functions defined in the same mutual-recursion nest; cl-set
is a list of lists of terms, viewed as a conjunction of clauses (each
viewed (as a disjunction); and ttree is an assumption-free tag-tree
that justifies cl-set.  (The notion of "tag-tree" may probably be
ignored except for system developers.)

Guard-obligation is typically used for function names or non-variable
terms, but as for verify-guards, it may also be applied to theorem
names.

See the source code for verify-guards-formula for an example of how to
use guard-obligation.

IN-PACKAGE    select current package

     Example:
     (in-package "MY-PKG")

     General Form:
     (in-package str)

where str is a string that names an existing ACL2 package, i.e., one of
the initial packages such as "KEYWORD" or "ACL2" or a package
introduced with defpkg.  For a complete list of the known packages
created with defpkg, evaluate

     (strip-cars (known-package-alist state)).

See DEFPKG.  An ACL2 book (see BOOKS) must contain a
single in-package form, which must be the first form in that book.

LD    the ACL2 read-eval-print loop, file loader, and command processor

     Examples:
     (LD "foo.lisp")              ; read and evaluate each form in file
                                  ; "foo.lisp", in order
     (LD "foo.lisp" :ld-pre-eval-print t)
                                  ; as above, but print each form to standard
                                  ; character output just before it is evaluated

     General Form:
     (LD standard-oi                  ; open obj in channel, stringp file name
                                      ; to open and close, or list of forms

     * Menu:

     * CALLING-LD-IN-BAD-CONTEXTS:: errors caused by calling ld in inappropriate contexts

     ; Optional keyword arguments:
         :dir                ...      ; use this add-include-book-dir directory
         :standard-co        ...      ; open char out or file to open and close
         :proofs-co          ...      ; open char out or file to open and close
         :current-package    ...      ; known package name
         :ld-skip-proofsp    ...      ; nil, 'include-book, or t
                                      ;   (see LD-SKIP-PROOFSP)
         :ld-redefinition-action ...  ; nil or '(:a . :b)
         :ld-prompt          ...      ; nil, t, or some prompt printer fn
         :ld-keyword-aliases ...      ; an alist pairing keywords to parse info
         :ld-pre-eval-filter ...      ; :all, :query, or some new name
         :ld-pre-eval-print  ...      ; nil, t, or :never
         :ld-post-eval-print ...      ; nil, t, or :command-conventions
         :ld-evisc-tuple     ...      ; nil or '(alist nil nil level length)
         :ld-error-triples   ...      ; nil or t
         :ld-error-action    ...      ; :return!, :return, :continue or :error
         :ld-query-control-alist ...  ; alist supplying default responses
         :ld-verbose         ...)     ; nil or t

Ld is the top-level ACL2 read-eval-print loop.  (When you call lp, a
little initialization is done in raw Common Lisp and then ld is
called.)  Ld is also a general-purpose ACL2 file loader and a command
interpreter.  Ld is actually a macro that expands to a function call
involving state.  Ld returns an "error triple" (mv erp val state) as
explained below.  (For much more on error triples, see
PROGRAMMING-WITH-STATE.)

See REBUILD for a variant of ld that skips proofs.  See
OUTPUT-TO-FILE for examples showing how to redirect output to a file.

The arguments to ld, except for :dir, all happen to be global variables
in state (see STATE and see PROGRAMMING-WITH-STATE).
For example, 'current-package and 'ld-verbose are global variables,
which may be accessed via (@ current-package) and (@ ld-verbose).  When
ld is called, it "binds" these variables.  By "binds" we actually mean
the variables are globally set but restored to their old values on
exit.  Because ld provides the illusion of state global variables being
bound, they are called "ld specials" (after the Lisp convention of
calling a variable "special" if it is referenced freely after having
been bound).

Note that all arguments but the first are passed via keyword.  Any
variable not explicitly given a value in a call retains its pre-call
value, with the exception of :ld-error-action, which defaults to
:return! if not explicitly specified.

Just as an example to drive the point home: If current-package is
"ACL2" and you typed

     (ld *standard-oi* :current-package "MY-PKG")

you would find yourself in (an inner) read-eval-print loop in which the
current-package was "MY-PKG".  You could operate there as long as you
wished, changing the current package at will.  But when you typed :q
you would return to the outer read-eval-print loop where the current
package would still be "ACL2".

Roughly speaking, ld repeatedly reads a form from standard-oi,
evaluates it, and prints its result to standard-co.  It does this until
the form is :q or evaluates to an error triple whose value component is
:q, or until the input channel or list is emptied.  However, ld has
many bells and whistles controlled by the ld specials.  Each such
special is documented individually.  For example, see the documentation
for standard-oi, current-package, ld-pre-eval-print, etc.

A more precise description of ld is as follows.  In the description
below we use the ld specials as variables, e.g., we say "a form is read
from standard-oi."  By this usage we refer to the current value of the
named state global variable, e.g., we mean "a form is read from the
current value of 'standard-oi." This technicality has an important
implication: If while interacting with ld you change the value of one of
the ld specials, e.g., 'standard-oi, you will change the behavior of
ld, e.g., subsequent input will be taken from the new value.

Three ld specials are treated as channels: standard-oi is treated as an
object input channel and is the source of forms evaluated by ld;
standard-co and proofs-co are treated as character output channels and
various flavors of output are printed to them.  However, the supplied
values of these specials need not actually be channels; several special
cases are recognized.

If the supplied value of one of these is in fact an open channel of the
appropriate type, that channel is used and is not closed by ld.  If the
supplied value of one of these specials is a string, the string is
treated as a file name in (essentially) Unix syntax (see
PATHNAME) and a channel of the appropriate type is opened to/from
that file.  Any channel opened by ld during the binding of the ld
specials is automatically closed by ld upon termination.  If
standard-co and proofs-co are equal strings, only one channel to that
file is opened and is used for both.

As a special convenience, when standard-oi is a string and the :dir
argument provided and not nil, we look up :dir in the table of
directories maintained by add-include-book-dir, and prepend this
directory to standard-oi to create the filename.  (In this case,
however, we require that standard-oi is a relative pathname, not an
absolute pathname.)  For example, one can write (ld
"arithmetic/top-with-meta.lisp" :dir :system) to ld that particular
system library.  (Of course, you should almost always load books like
arithmetic/top-with-meta using include-book instead of ld.)  If :dir is
not specified, then a relative pathname is resolved using the connected
book directory; see CBD.

Several other alternatives are allowed for standard-oi.  If standard-oi
is a true list then it is taken as the list of forms to be processed.
If standard-oi is a list ending in an open channel, then ld processes
the forms in the list and then reads and processes the forms from the
channel.  Analogously, if standard-oi is a list ending a string, an
object channel from the named file is opened and ld processes the forms
in the list followed by the forms in the file.  That channel is closed
upon termination of ld.

The remaining ld specials are handled more simply and generally have to
be bound to one of a finite number of tokens described in the :doc
entries for each ld special.  Should any ld special be supplied an
inappropriate value, an error message is printed.

Next, if ld-verbose is t, ld prints the message "ACL2 loading name"
where name names the file or channel from which forms are being read.
At the conclusion of ld, it will print "Finished loading name" if
ld-verbose is t.

Finally, ld repeatedly executes the ACL2 read-eval-print step, which may
be described as follows.  A prompt is printed to standard-co if
ld-prompt is non-nil.  The format of the prompt is determined by
ld-prompt.  If it is t, the default ACL2 prompt is used.  If it is any
other non-nil value then it is treated as an ACL2 function that will
print the desired prompt.  See LD-PROMPT.  In the exceptional
case where ld's input is coming from the terminal (*standard-oi*) but
its output is going to a different sink (i.e., standard-co is not
*standard-co*), we also print the prompt to the terminal.

Ld then reads a form from standard-oi.  If the object read is a
keyword, ld constructs a "keyword command form" by possibly reading
several more objects.  See KEYWORD-COMMANDS.  This construction
process is sensitive to the value of ld-keyword-aliases.  See
LD-KEYWORD-ALIASES.  Otherwise, the object read is treated as the
command form.

Ld next decides whether to evaluate or skip this form, depending on
ld-pre-eval-filter.  Initially, the filter must be either :all, :query,
or a new name.  If it is :all, it means all forms are evaluated.  If it
is :query, it means each form that is read is displayed and the user is
queried.  Otherwise, the filter is a name and each form that is read is
evaluated as long as the name remains new, but if the name is ever
introduced then no more forms are read and ld terminates.  See
LD-PRE-EVAL-FILTER.

If the form is to be evaluated, then ld first prints the form to
standard-co, if ld-pre-eval-print is t.  With this feature, ld can
process an input file or form list and construct a script of the
session that appears as though each form was typed in.  See
LD-PRE-EVAL-PRINT.

Ld then evaluates the form, with state bound to the current state.  The
result is some list of (multiple) values.  If a state is among the
values, then ld uses that state as the subsequent current state.

Depending on ld-error-triples, ld may interpret the result as an
"error."  See LD-ERROR-TRIPLES.  We first discuss ld's behavior
if no error signal is detected (either because none was sent or because
ld is ignoring them because ld-error-triples is nil).

In the case of a non-erroneous result, ld does two things: First, if the
logical world in the now current state is different than the world
before execution of the form, ld adds to the world a "command landmark"
containing the form evaluated.  See COMMAND-DESCRIPTOR.
Second, ld prints the result to standard-co, but only if
ld-post-eval-print is not nil.  The result is printed as a list of
(multiple) values unless ld-post-eval-print is :command-conventions,
ld-error-triples is t, and the result is an "error triple", i.e., of
the form (mv * * state).  In that case, only the non-erroneous "value"
component of the result is printed.  See LD-POST-EVAL-PRINT.

Whenever ld prints anything (whether the input form, a query, or some
results) it "eviscerates" it if ld-evisc-tuple is non-nil.
Essentially, evisceration is a generalization of Common Lisp's use of
*print-level* and *print-length* to hide large substructures.  See
EVISC-TUPLE and also see SET-IPRINT.

We now return to the case of a form whose evaluation signals an error.
In this case, ld first restores the ACL2 logical world to what it was
just before the erroneous form was evaluated.  Thus, a form that
partially changes the world (i.e., begins to store properties) and then
signals an error, has no effect on the world.  You may see this happen
on commands that execute several events (e.g., an encapsulate or a
progn of several defuns): even though the output makes it appear that
the initial events were executed, if an error is signalled by a later
event the entire block of events is discarded.

After rolling back, ld takes an action determined by ld-error-action.
If the action is :continue, ld merely iterates the read-eval-print
step.  Note that nothing suggestive of the value of the "erroneous"
form is printed.  If the action is :return, ld terminates normally;
similarly if the action is :return!, but a special value is returned
that can cause superior ld commands to terminate; see
LD-ERROR-ACTION for details.  If the action is :error, ld terminates
signalling an error to its caller.  If its caller is in fact another
instance of ld and that instance is watching out for error signals, the
entire world created by the inner ld will be discarded by the outer ld
if the inner ld terminates with an error.

Ld returns an error triple, (mv erp val state).  Erp is t or nil
indicating whether an error is being signalled.  If no error is
signalled, val is the "reason" ld terminated and is one of :exit
(meaning :q was read), :eof (meaning the input source was exhausted),
:error (meaning an error occurred but has been supressed), :filter
(meaning the ld-pre-eval-filter terminated ld), or a cons pair whose
first component is the symbol :STOP-LD, which typically indicates that
an error occurred while the value of variable 'ld-error-action was
:RETURN!.  See LD-ERROR-ACTION for details of this last case.

CALLING-LD-IN-BAD-CONTEXTS    errors caused by calling ld in inappropriate contexts

The macro ld was designed to be called directly in the top-level ACL2
loop, although there may be a few occasions for calling it from
functions.  ACL2 cannot cope with invocations of ld during the process
of loading a compiled file for a book, so this is an error.

To see how that can happen, consider the following book, where file
const.lsp contains the single form (defconst *foo* '(a b)).

       (in-package "ACL2")
       (defttag t)
       (progn! (ld "const.lsp"))

An attempt to certify this book will cause an error, but that particular
error can be avoided, as discussed below.  If the book is certified,
however, with production of a corresponding compiled file (which is the
default behavior for certify-book), then any subsequent call of
include-book that loads this compiled file will cause an error.  Again,
this error is necessary because of how ACL2 is designed; specifically,
this ld call would interfere with tracking of constant definitions when
loading the compiled file for the book.

Because including such a book (with a compiled file) causes an error,
then as a courtesy to the user, ACL2 arranges that the certification
will fail (thus avoiding a surprise later when trying to include the
book).  The error in that case will look as follows.

       ACL2 Error in LD:  It is illegal to call LD in this context.  See DOC
       calling-ld-in-bad-contexts.

If you really think it is OK to avoid this error, you can get around it
by setting state global variable ld-okp to t:  (assign ld-okp t).  You
can then certify the book in the example above, but you will still not
be able to include it with a compiled file.

PRINT-GV    print a form whose evaluation caused a guard violation

By default, ACL2 checks input constraints on functions, known as
guards.  When guards are violated, an informative message is printed;
but sometimes it is useful to investigate why the guard check fails.
The utility print-gv is provided for that purpose.  (Alternatively, you
may prefer to avoid guards entirely with (set-guard-checking :none);
see SET-GUARD-CHECKING.)

     Example Forms:
     (print-gv)
     (print-gv :evisc-tuple (evisc-tuple 4 4 nil nil))
     (print-gv :evisc-tuple (evisc-tuple 4 ; print-level
                                         5 ; print-length
                                         (world-evisceration-alist state nil)
                                         nil ; hiding-cars
                                         ))

     General Form:
     (print-gv :evisc-tuple x)

where the :evisc-tuple argument is optional and defaults to one that
hides only the ACL2 logical world, by printing <world> instead of a
very large structure.  See EVISC-TUPLE for a discussion of
evisc-tuples.

To see how one might use print-gv, consider the following definition.

     (defun foo (x)
       (declare (xargs :guard (and (my-first-predicate x)
                                   (my-second-predicate x))))
       (cdr x))

Now suppose we evaluate a call of foo and obtain a guard violation.

     ACL2 !>(foo 3)

     ACL2 Error in TOP-LEVEL:  The guard for the function call (FOO X),
     which is (AND (MY-FIRST-PREDICATE X) (MY-SECOND-PREDICATE X)), is violated
     by the arguments in the call (FOO 3).  To debug: See :DOC print-gv,
     see :DOC trace, and see :DOC wet.  See :DOC set-guard-checking for
     information about suppressing this check with (set-guard-checking :none),
     as recommended for new users.

     ACL2 !>

We can obtain (in essence) the guard form that was false, as follows.

     ACL2 !>(print-gv)

     (LET ((X '3))
          (DECLARE (IGNORABLE X))
          (AND (MY-FIRST-PREDICATE X)
               (MY-SECOND-PREDICATE X)))

     ACL2 !>

But which conjunct is to blame?  With a bit of editing we can try each
conjunct in turn.

     ACL2 !>(LET ((X '3))
                 (DECLARE (IGNORABLE X))
                 (MY-FIRST-PREDICATE X))
     T
     ACL2 !>(LET ((X '3))
                 (DECLARE (IGNORABLE X))
                 (MY-SECOND-PREDICATE X))
     NIL
     ACL2 !>

Aha!  Now we can investigate why the second predicate fails for 3.

The following hack will give you access in raw Lisp to the form printed
by (print-gv).  After a guard violation, just submit this form to raw
Lisp:

     (print-gv1 (wormhole-data (cdr (assoc 'ev-fncall-guard-er-wormhole
                                           *wormhole-status-alist*)))
                state)

If you use local stobjs (see WITH-LOCAL-STOBJ), you my need to
edit the output of print-gv in order to evaluate it.  Consider the
following example.

     (defstobj st fld)

     (defun g (x st)
       (declare (xargs :guard (consp x) :stobjs st)
                (ignore x))
       (fld st))

     (defun test ()
       (with-local-stobj
        st
        (mv-let (result st)
                (mv (g 3 st) st)
                result)))

     (test)

Then :print-gv yields the result shown below.

     (FLET ((G{GUARD} (X ST)
                      (DECLARE (IGNORABLE X ST))
                      (AND (STP ST) (CONSP X))))
           (G{GUARD} '3 |<some-local-stobj>|))

In this example you could replace "|<some-local-stobj>|" by "st" to
obtain a result of nil.  But similar cases may require the use of a
local stobj that is no longer available, in which case you may need to
be creative in order to take advantage of :print-gv.  Here is such an
example.

     (defstobj st2 fld2)

     (defun g2 (st2)
       (declare (xargs :guard (null (fld2 st2)) :stobjs st2))
       (mv 0 st2))

     (defun test2 ()
       (with-local-stobj
        st2
        (mv-let (result st2)
                (let ((st2 (update-fld2 17 st2)))
                  (g2 st2))
                result)))

     (test2)

In this case, :print-gv yields the following.

     (FLET ((G2{GUARD} (ST2)
                       (DECLARE (IGNORABLE ST2))
                       (AND (ST2P ST2) (NULL (FLD2 ST2)))))
           (G2{GUARD} |<some-local-stobj>|))

But if you replace "|<some-local-stobj>|" by "st", the guard holds; it
is only the local stobj, which is no longer available, that produced a
guard violation (because its field had been updated to a cons).

     ACL2 !>(FLET ((G2{GUARD} (ST2)
                              (DECLARE (IGNORABLE ST2))
                              (AND (ST2P ST2) (NULL (FLD2 ST2)))))
                  (G2{GUARD} st2))
     T
     ACL2 !>

Finally, we note that while print-gv is a utility for debugging guard
violations, in contrast, see GUARD-DEBUG for a utility to
assist in debugging failed proofs arising from guard verification.

PROPS    print the ACL2 properties on a symbol

     Example:
     :props assoc-eq

Props takes one argument, a symbol, and prints all of the properties
that are on that symbol in the ACL2 world.

PSO    show the most recently saved output

Evaluate :pso in order to print output that was generated in an
environment where output was being saved;  see SET-SAVED-OUTPUT
for details.  However, proof-tree output will be suppressed; use :pso!
if you want that output to be printed as well.

Also see PSOG, for printing saved output in gag-mode.

PSO!    show the most recently saved output, including proof-tree output

Evaluate :pso! in order to print output that was generated in an
environment where output was being saved; see SET-SAVED-OUTPUT
for details.  Note that proof-tree will be included; use :pso if you
want that output to be suppressed.

Also see PSOG, for printing saved output in gag-mode.

PSOF    show the most recently saved output

For a similar utility, see PSO.  Like :pso, the :psof command
prints output that was generated in an environment where output was
being saved, typically gag-mode; also see SET-SAVED-OUTPUT.
But unlike :pso, :psof takes a filename argument and saves output to
that file, instead of to the terminal.  For large proofs, :psof may
complete more quickly than :pso.  Note that as with :pso, proof-tree
output will be suppressed.

The first line of output from :psof directs the Emacs editor to use
auto-revert mode.  You can change the frequency of auto-reverting the
buffer connected to a file by evaluating a suitable command in Emacs.
For example, the command (setq auto-revert-interval .1) arranges for
auto-revert mode to update as needed every 1/10 of a second.

PSOG    show the most recently saved output in gag-mode

Evaluate :psog in order to print output in gag-mode that was generated
in an environment where output was being saved;  see
SET-SAVED-OUTPUT for details.

Also see PSO and see PSO! for printing the full output.

PSTACK    seeing what is the prover up to

     General Forms:
     (pstack)      ; inspect break
     (pstack t)    ; inspect break, printing all calls in abbreviated form
     (pstack :all) ; as above, but only abbreviating the ACL2 world

When the form (pstack) is executed during a break from a proof, or at
the end of a proof that the user has aborted, a "process stack" (or
"prover stack") will be printed that gives some idea of what the
theorem prover has been doing.  Moreover, by evaluating (verbose-pstack
t) before starting a proof (see VERBOSE-PSTACK) one can get
trace-like information about prover functions, including time
summaries, printed to the screen during a proof.  This feature is
currently quite raw and may be refined considerably as time goes on,
based on user suggestions.  For example, the usual control of printing
given by set-inhibit-output-lst is irrelevant for printing the pstack.

The use of (pstack t) or (pstack :all) should only be used by those who
are comfortable looking at functions in the ACL2 source code.
Otherwise, simply use (pstack).

Entries in the pstack include the following (listed here alphabetically,
except for the first).

preprocess-clause, simplify-clause, etc. (in general,xxx-clause):
top-level processes in the prover "waterfall"

clausify: splitting a goal into subgoals

ev-fncall: evaluating a function on explicit arguments

ev-fncall-meta:  evaluating a metafunction

forward-chain: building a context for the current goal using
forward-chaining rules

induct: finding an induction scheme

pop-clause:  getting the next goal to prove by induction

process-assumptions:  creating forcing rounds

remove-built-in-clauses: removing built-in clauses (see
BUILT-IN-CLAUSE)

process-equational-polys:  deducing interesting equations

remove-trivial-equivalences:  removing trivial equalities (and
equivalences) from the current goal

rewrite-atm:  rewriting a top-level term in the current goal

setup-simplify-clause-pot-lst:  building the linear arithmetic database
for the current goal

strip-branches,  subsumption-replacement-loop:  subroutines of clausify

waterfall: top-level proof control

VERBOSE-PSTACK    seeing what is the prover up to (for advanced users)

     General Forms:
     (verbose-pstack t)   ; get trace-like information on prover during proofs
     (verbose-pstack '(fn1 fn2 ...))
                          ; as above, but omit calls of the indicated functions
     (verbose-pstack nil) ; turn off trace-like information on prover

For example, (verbose-pstack '(ev-fncall)) will provide a trace of
various prover functions during proofs, except for the function
ev-fncall.

By evaluating (verbose-pstack t) one can get trace-like information
during subsequent proofs about prover functions, including time
summaries, printed to the screen during a proof.  To turn off this
feature, evaluate (verbose-pstack nil).  Also See PSTACK.

Q    quit ACL2 (type :q) -- reenter with (lp)

     Example:
     ACL2 !>:Q

The keyword command :q typed at the top-level of the ACL2 loop will
terminate the loop and return control to the Common Lisp top-level (or,
more precisely, to whatever program invoked lp).  To reenter the ACL2
loop, execute (acl2::lp) in Common Lisp.  You will be in the same state
as you were when you exited with :q, unless during your stay in Common
Lisp you messed the data structures representating the ACL2 state
(including files, property lists, and single-threaded objects).

Unlike all other keyword commands, typing :q is not equivalent to
invoking the function q.  There is no function q.

QUIT    quit entirely out of Lisp

Same as good-bye.

REBUILD    a convenient way to reconstruct your old state

     Examples:
     ACL2 !>(rebuild "project.lisp")
     ACL2 !>(rebuild "project.lisp" t)
     ACL2 !>(rebuild "project.lisp" t :dir :system)
     ACL2 !>(rebuild "project.lisp" :all)
     ACL2 !>(rebuild "project.lisp" :query)
     ACL2 !>(rebuild "project.lisp" 'lemma-22)

Rebuild allows you to assume all the commands in a given file or list,
supplied in the first argument.  Because rebuild processes an arbitrary
sequence of commands with ld-skip-proofsp t, it is unsound!  However,
if each of these commands is in fact admissible, then processing them
with rebuild will construct the same logical state that you would be in
if you typed each command and waited through the proofs again.  Thus,
rebuild is a way to reconstruct a state previously obtained by proving
your way through the commands.

The second, optional argument to rebuild is a "filter" (see
LD-PRE-EVAL-FILTER) that lets you specify which commands to process.
You may specify t, :all, :query, or a new logical name.  t and :all
both mean that you expect the entire file or list to be processed.
:query means that you will be asked about each command in turn.  A new
name means that all commands will be processed as long as the name is
new, i.e., rebuild will stop processing commands immediately after
executing a command that introduces name.  Rebuild will also stop if
any command causes an error.  You may therefore wish to plant an
erroneous form in the file, e.g., (mv t nil state), (see
LD-ERROR-TRIPLES), to cause rebuild to stop there.  The form
(i-am-here) is such a pre-defined form.  If you do not specify a
filter, rebuild will query you for one.

Inspection of the definition of rebuild, e.g., via :pc rebuild-fn, will
reveal that it is just a glorified call to the function ld.  See
LD if you find yourself wishing that rebuild had additional
functionality.

If you supply the above "filter" argument, then you may also supply the
keyword argument :dir, which is then passed to ld; see LD.

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.  For example, you might
want to execute (redo-flat :succ-ld-skip-proofsp nil) if you use the
must-fail utility from distributed book make-event/eval.lisp, since for
example (must-fail (thm (equal x y))) normally succeeds but would cause
an error if proofs are skipped.

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

RESET-LD-SPECIALS    restores initial settings of the ld specials

     Examples:
     (reset-ld-specials t)
     (reset-ld-specials nil)

Roughly speaking, the ld specials are certain state global variables,
such as current-package, ld-prompt, and ld-pre-eval-filter, which are
managed by ld as though they were local variables.  These variables
determine the channels on which ld reads and prints and control many
options of ld.  See LD for the details on what the ld specials
are.

This function, reset-ld-specials, takes one Boolean argument, flg.  The
function resets all of the ld specials to their initial, top-level
values, except for the three channel variables, standard-oi,
standard-co, and proofs-co, which are reset to their initial values
only if flg is non-nil.  Of course, if you are in a recursive call of
ld, then when you exit that call, the ld specials will be restored to
the values they had at the time ld was called recursively.  To see what
the initial values are, inspect the value of the constant
*initial-ld-special-bindings*.

SAVE-EXEC    save an executable image and (for most Common Lisps) a wrapper script

See SAVING-AND-RESTORING for an explanation of why one might
want to use this function.

     Examples:
     ; Save an executable named my-saved_acl2:
     (save-exec "my-saved_acl2"
                "This saved image includes Version 7 of Project Foo.")

     ; Same as above, but with a generic comment instead:
     (save-exec "my-saved_acl2" nil)

     General Form:
     (save-exec exec-filename extra-startup-string)

where exec-filename is the filename of the proposed executable and
extra-startup-string is a non-empty string to be printed after the
normal ACL2 startup message when you start up the saved image.  However,
extra-startup-string is allowed to be nil, in which case a generic
string will be printed instead.

*Notes*:

1. For technical reasons, you must first exit the ACL2 read-eval-print
loop, for example by executing :q, before evaluating a save-exec call.

2. The image will be saved so that in the new image, the raw Lisp
package and the package in the ACL2 read-eval-print loop (see
LP) will be the same as their respective values at the time save-exec
is called.

3. For most Common Lisps, the specified file (e.g., "my-saved_acl2" in
the examples above) will be written as a small script, which in turn
invokes a saved image to which an extension has been appended (e.g.,
my-saved_acl2.gcl for the examples above, when the underlying Common
Lisp is GCL on a non-Windows system).

SET-ACCUMULATED-PERSISTENCE    See ACCUMULATED-PERSISTENCE.

SHARP-BANG-READER    package prefix that is not restricted to symbols

     Examples:

     ACL2 !>(defpkg "FOO" nil)

     Summary
     Form:  ( DEFPKG "FOO" ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      "FOO"
     ACL2 !>'#!foo(a b)
     (FOO::A FOO::B)
     ACL2 !>'#!foo(a #!acl2 b)
     (FOO::A B)
     ACL2 !>'#!foo(#!acl2 a b)
     (A FOO::B)
     ACL2 !>'#!foo(#!"ACL2" a b)
     (A FOO::B)
     ACL2 !>

The ACL2 reader supports the syntax #!pkg-name expr where pkg-name is a
string or symbol that names a package known to ACL2.  As illustrated
above, this syntax nests as one might expect.  In the special case that
expr is a symbol, #!pkg-name expr is equivalent to pkg-name::expr.

SHARP-COMMA-READER    DEPRECATED read-time evaluation of constants

The use of `#,' has been deprecated.  Please use `#.' instead; see
SHARP-DOT-READER.

SHARP-DOT-READER    read-time evaluation of constants

     Example:

     ACL2 !>(defconst *a* '(a b c))

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      *A*
     ACL2 !>(quote (1 2 #.*a* 3 4))
     (1 2 (A B C) 3 4)
     ACL2 !>

The ACL2 reader supports the syntax #.*a* where *a* was defined by
defconst.  In this case, the reader treats #.*a* as though it were
reading the value of *a*.  This feature can be useful in conjunction
with the use of evisc-table to abbreviate large constants, so that the
abbreviation can be read back in; see EVISC-TABLE.

Note that the ACL2 reader only supports `#.' as described above, unlike
Common Lisp.  Older versions (preceding  3.5) used `#.' to abort, but
that functionality is now carried out by (a!); see A!.  For a
related feature that only pops up one level, see P!.

SHARP-U-READER    allow underscore characters in numbers

     Example:

     ACL2 !>#ub1000_1000_1000_
     2184
     ACL2 !>#b100010001000
     2184
     ACL2 !>#uo1_1
     9
     ACL2 !>#o11
     9
     ACL2 !>#u34_5
     345
     ACL2 !>#u345
     345
     ACL2 !>345
     345
     ACL2 !>#ux12_a
     298
     ACL2 !>#ux12a
     298
     ACL2 !>#u x12a
     298
     ACL2 !>#x12a
     298
     ACL2 !>#u123_456/7_919
     123456/7919
     ACL2 !>

The ACL2 reader supports the use of #ub, #uo, and #ux where one would
otherwise write #b, #o, and #x, respectively (for binary, octal, and
hexadecimal numerals), but where underscore characters (`_') are
allowed but ignored.  Also supported is the prefix #u in front of a an
expression that is a decimal numeral except that underscore characteres
are allowed but ignored.

The precise specification of #u is as follows.  The Lisp reader reads
one expression after the #u.  If the result is a number, then that
number is returned by the reader.  Otherwise the result must be a
symbol whose name begins with one of the characters `B', `O', or `X',
or else a decimal digit (one of the characters `0, 1, ..., 9').  All
underscores are removed from the name of that symbol to obtain a string
and in the first three cases only, a `#' character is prepended to that
string.  The resulting string is then handed to the Lisp reader in
order to obtain the final result, which must be a number or else an
error occurs.

SHOW-ACCUMULATED-PERSISTENCE    See ACCUMULATED-PERSISTENCE.

SKIP-PROOFS    skip proofs for a given form -- a quick way to introduce unsoundness

     Example Form:
     (skip-proofs
       (defun foo (x)
         (if (atom x) nil (cons (car x) (foo (reverse (cdr x)))))))

     General Form:
     (skip-proofs form)

where form is processed as usual except that the proof obligations
usually generated are merely assumed.

Normally form is an event; see EVENTS.  If you want to put
skip-proofs around more than one event, consider the following (see
PROGN): (skip-proofs (progn event1 event2 ... eventk)).

WARNING: Skip-proofs allows inconsistent events to be admitted to the
logic.  Use it at your own risk!

Sometimes in the development of a formal model or proof it is
convenient to skip the proofs required by a given event.  By embedding
the event in a skip-proofs form, you can avoid the proof burdens
generated by the event, at the risk of introducing unsoundness.  Below
we list four illustrative situations in which you might find
skip-proofs useful.

1. The termination argument for a proposed function definition is
complicated.  You presume you could admit it, but are not sure that
your definition has the desired properties.  By embedding the defun
event in a skip-proofs you can "admit" the function and experiment with
theorems about it before undoing (see UBT) and then paying the
price of its admission.  Note however that you might still have to
supply a measure.  The set of formals used in some valid measure, known
as the "measured subset" of the set of formals, is used by ACL2's
induction heuristics and therefore needs to be suitably specified.  You
may wish to specify the special measure of (:? v1 ... vk), where (v1
... vk) enumerates the measured subset.

2. You intend eventually to verify the guards for a definition but do
not want to take the time now to pursue that.  By embedding the
verify-guards event in a skip-proofs you can get the system to behave
as though the guards were verified.

3. You are repeatedly recertifying a book while making many experimental
changes.  A certain defthm in the book takes a very long time to prove
and you believe the proof is not affected by the changes you are
making.  By embedding the defthm event in a skip-proofs you allow the
theorem to be assumed without proof during the experimental
recertifications.

4. You are constructing a proof top-down and wish to defer the proof of
a defthm until you are convinced of its utility.  You can embed the
defthm in a skip-proofs.  Of course, you may find later (when you
attempt prove the theorem) that the proposed defthm is not a theorem.

Unsoundness or Lisp errors may result if the presumptions underlying a
use of skip-proofs are incorrect.  Therefore, skip-proofs must be
considered a dangerous (though useful) tool in system development.

Roughly speaking, a defthm embedded in a skip-proofs is essentially a
defaxiom, except that it is not noted as an axiom for the purposes of
functional instantiation (see LEMMA-INSTANCE).  But a skipped
defun is much more subtle since not only is the definitional equation
being assumed but so are formulas relating to termination and type.
The situation is also difficult to characterize if the skip-proofs
events are within the scope of an encapsulate in which constrained
functions are being introduced.  In such contexts no clear logical
story is maintained; in particular, constraints aren't properly tracked
for definitions.  A proof script involving skip-proofs should be
regarded as work-in-progress, not as a completed proof with some
unproved assumptions.  A skip-proofs event represents a promise by the
author to admit the given event without further axioms.  In other
words, skip-proofs should only be used when the belief is that the
proof obligations are indeed theorems in the existing ACL2 logical
world.

ACL2 allows the certification of books containing skip-proofs events by
providing the keyword argument :skip-proofs-okp t to the certify-book
command.  This is contrary to the spirit of certified books, since one
is supposedly assured by a valid certificate that a book has been
"blessed."  But certification, too, takes the view of skip-proofs as
"work-in-progress" and so allows the author of the book to promise to
finish.  When such books are certified, a warning to the author is
printed, reminding him or her of the incurred obligation.  When books
containing skip-proofs are included into a session, a warning to the
user is printed, reminding the user that the book is in fact incomplete
and possibly inconsistent.  This warning is in fact an error if
:skip-proofs-okp is nil in the include-book form; see
INCLUDE-BOOK.

We conclude with a technical note.  Skip-proofs works by binding the ld
special ld-skip-proofsp to t unless it is already bound to a non-nil
value; see LD-SKIP-PROOFSP.

THM    prove a theorem

     Example:
     (thm (equal (app (app a b) c)
                 (app a (app b c))))

Also see DEFTHM.  Unlike defthm, thm does not create an event;
it merely causes the theorem prover to attempt a proof.

     General Form:
     (thm term
          :hints        hints
          :otf-flg      otf-flg
          :doc          doc-string)

where term is a term alleged to be a theorem, and hints, otf-flg and
doc-string are as described in the corresponding :doc entries.  The
three keyword arguments above are all optional.

TOP-LEVEL    evaluate a top-level form as a function body

Some forms, such as calls of with-local-stobj, are illegal when
supplied directly to the ACL2 top-level loop.  The macro top-level
provides a workaround in such cases, by defining a temporary
:program-mode function named top-level-fn whose only argument is state
and whose body is the form to be evaluated.  When the call of top-level
returns there is no change to the existing ACL2 logical world.  The
following edited log illustrates all of the above points.

     ACL2 !>:pbt 0
               0  (EXIT-BOOT-STRAP-MODE)
     ACL2 !>(defstobj st fld)

     Summary
     Form:  ( DEFSTOBJ ST ...)
     Rules: NIL
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      ST
     ACL2 !>(top-level
             (with-local-stobj
              st
              (mv-let (result st)
                      (let ((st (update-fld 17 st)))
                        (mv (fld st) st))
                      result)))
     17
     ACL2 !>(top-level
             (with-local-stobj
              st
              (mv-let (result st)
                      (let ((st (update-fld 17 st)))
                        (mv (fld st) st))
                      (mv nil result state))))
      17
     ACL2 !>(top-level
             (with-local-stobj
              st
              (mv-let (result st)
                      (let ((st (update-fld 17 st)))
                        (mv (fld st) st))
                      (mv result state))))
     (17 <state>)
     ACL2 !>:pbt 0
               0  (EXIT-BOOT-STRAP-MODE)
        d      1:x(DEFSTOBJ ST FLD)
     ACL2 !>

Each argument of top-level after the first should be a declare form or
documentation string, as the list of these extra arguments will be
placed before the first argument when forming the definition of
top-level-fn.

Top-level generates a call of ld, so that the value returned is printed
in the normal way.  The call of top-level itself actually evaluates to
(mv nil :invisible state), which normally results in no additional
output.

TRANS    print the macroexpansion of a form

     Examples:
     :trans (list a b c)
     :trans (caddr x)
     :trans (cond (p q) (r))

This function takes one argument, an alleged term, and translates it,
expanding the macros in it completely.  Either an error is caused or
the formal meaning of the term is printed.  We also print the "output
signature" which indicates how many results are returned and which are
single-threaded objects.  For example, a term that returns one ordinary
object (e.g., an object other than STATE or a user-defined
single-threaded object (see DEFSTOBJ)) has the output signature

     => *

A term that returns the single-threaded object STATE has the output
signature

     => STATE

and a term that returns four results might have the output signature

     => (MV $MEM * * STATE)

This signature indicates that the first result is the (user defined)
single-threaded object $MEM, that the next two results are ordinary,
and that the last result is STATE.

See TRANS! for a corresponding command that does not enforce
restrictions of single-threaded objects.

It is sometimes more convenient to use trans1 which is like trans but
which only does top-level macroexpansion.

For more, see TERM.

TRANS!    print the macroexpansion of a form without single-threadedness concerns

     Examples:
     :trans! (list a b c)
     :trans! (append x state)

:Trans! is identical to :trans, except that unlike :trans, :trans!
ignores single-threadedness restrictions.  Thus, the second form above
is legal for :trans!.  Also see TRANS and see TRANS1.

TRANS1    print the one-step macroexpansion of a form

     Examples:
     :trans1 (list a b c)
     :trans1 (caddr x)
     :trans1 (cond (p q) (r))

This function takes one argument, an alleged term, and expands the
top-level macro in it for one step only.  Either an error is caused,
which happens when the form is not a call of a macro, or the result is
printed.  Also see TRANS, which translates the given form
completely.

VERIFY-GUARDS-FORMULA    view the guard proof obligation, without proving it

See VERIFY-GUARDS and see GUARD for a discussion of
guards.  This utility is provided for viewing a guard proof obligation,
without doing a proof.

     Example Forms:
     (verify-guards-formula foo)
     (verify-guards-formula foo :guard-debug t)
     (verify-guards-formula foo :otf-flg dont-care :xyz whatever)
     (verify-guards-formula (+ (foo x) (bar y)) :guard-debug t)

Verify-guards-formula allows all keywords, but only pays attention to
:guard-debug, which has the same effect as in verify-guards (see
GUARD-DEBUG).  Apply verify-guards-formula to a name just as you
would use verify-guards, but when you only want to view the formula
rather than creating an event.  If the first argument is not a symbol,
then it is treated as the body of a defthm event for which you want the
guard proof obligation.

See GUARD-OBLIGATION if you want to obtain guard proof
obligations for use in a program.

WALKABOUT    explore an ACL2 cons tree

By typing (walkabout x state) for an ACL2 term x whose value is a cons
tree, you can walk around that tree.  For example, ACL2 developers
often use this utility to explore the ACL2 logical world.

When you issue a walkabout command, a summary of commands will be
printed before you enter an interactive loop.

     Commands:
     0, 1, 2, ..., nx, bk, pp, (pp n), (pp lev len), =, (= symb), and q.

In the interactive walkabout loop, a positive integer n takes you to the
nth position, while 0 takes you up a level.  The commands nx and bk
take you to the next and previous position, respectively, at the same
level.  The command pp prints the current object in full, while (pp
level length) hides sub-objects below the indicated level and past the
indicated length, if non-nil; see EVISC-TUPLE.  The command (pp
n) abbreviates (pp n n), so in particular (pp nil) is equivalent to pp.

The following example illustrates the commands described above.

     ACL2 !>(walkabout (append '(a (b1 b2 b3)) '(c d e f)) state)

     Commands:
     0, 1, 2, ..., nx, bk, pp, (pp n), (pp lev len), =, (= symb), and q.

     (A (B1 B2 B3) C ...)
     :2
     (B1 B2 B3)
     :3
     B3
     :0
     (B1 B2 B3)
     :nx
     C
     :nx
     D
     :0
     (A (B1 B2 B3) C ...)
     :pp
     (A (B1 B2 B3) C D E F)
     :(pp 4)
     (A (B1 B2 B3) C D ...)
     :(pp 1 4)
     (A # C D ...)
     :(pp nil 2)
     (A (B1 B2 ...) ...)
     :q
     ACL2 !>

Finally we describe the commands q, =, and (= symb), where symb is a
symbol.  The command q simply causes an exit from the walkabout loop.
The command = also exits, but causes the current object to be printed
in full.  The command (= symb) saves an association of symb with the
current object, which can be retrieved outside the walkabout loop using
the macro walkabout=, as illustrated below.

     :2
     (B1 B2 B3)
     :(= my-list)
     (walkabout= MY-LIST) is
     (B1 B2 B3)
     :q
     ACL2 !>(walkabout= MY-LIST)
     (B1 B2 B3)
     ACL2 !>

Finally, we remark that for trees that are not true-lists, walkabout
treats the dot as an object that can be "walked about".  The following
example illustrates this point.

     ACL2 !>(walkabout '(c d e . f) state)

     Commands:
     0, 1, 2, ..., nx, bk, pp, (pp n), (pp lev len), =, (= symb), and q.

     (C D E . F)
     :3
     E
     :nx
     .
     :nx
     F
     :0
     (C D E . F)
     :4
     .
     :0
     (C D E . F)
     :5
     F
     :

WITH-PROVER-STEP-LIMIT    limit the number of steps for proofs

Logically, (with-prover-step-limit expr form) is equivalent to form,
except that if the number of "prover steps" executed during evaluation
of form exceeds a bound specified by the value of expr, then that proof
will abort.  See SET-PROVER-STEP-LIMIT for a related utility
that sets the limit on prover steps globally instead of setting it for
just one form, and for a discussion of the notion of "prover steps",
which could change in future ACL2 releases.  For a related utility
based on time instead of prover steps, see
WITH-PROVER-TIME-LIMIT.

The arguments of (with-prover-step-limit expr form) are evaluated.  The
optional extra argument, discussed below, is not evaluated.

Depending on the machine you are using, you may have only (very
roughly) a half-hour of time before the number of prover steps exceeds
the maximum limit on prover steps that may be imposed, which is one
less than the value of *default-step-limit*.  But there is no limit
unless you explicitly call with-prover-step-limit or
set-prover-step-limit.

For examples of how step-limits work besdies those presented below, see
the distributed book books/misc/misc2/step-limits.lisp.

Note that with-prover-step-limit may not be called inside definitions,
and that it is simply the identity macro in raw Lisp.  However,
with-prover-step-limit! may be called in place of
with-prover-step-limit, with the same effect as described here.

     Examples:

     ; Limit (mini-proveall) to 100,000 prover steps (which is enough to complete)
     (with-prover-step-limit 100000 (mini-proveall))

     ; Same as above for the inner call of with-prover-step-limit; so the
     ; mini-proveall call completes, but then we get an error because the second
     ; argument of the outer with-prover-step-limit call took more than 200
     ; steps.
     (with-prover-step-limit
      200
      (with-prover-step-limit 100000 (mini-proveall)))

     ; Same as preceding form just above, except that this time there is no error,
     ; because the inner call of with-prover-step-limit has an extra argument
     ; of t inserted into the second argument position, which specifies that this
     ; entire inner call is treated as though it uses no prover steps.
     (with-prover-step-limit
      200
      (with-prover-step-limit 100000 t (mini-proveall)))

     ; The inner call limit (mini-proveall) to 200 prover steps, which fails
     ; almost immediately.
     (with-prover-step-limit 100000 (with-prover-step-limit 200 (mini-proveall)))

     ; Do not limit the number of prover steps, regardless of such a limit imposed
     ; globally or by the surrounding context.
     (with-prover-step-limit nil (mini-proveall))

     ; Same as just above (indeed, nil above is converted to
     ; *default-step-limit*):
     (with-prover-step-limit *default-step-limit* (mini-proveall))

     ; Limit the indicated theorem to 100 steps, and when the proof does not
     ; complete, then put down a label instead.
     (mv-let (erp val state)
             (with-prover-step-limit
              100
              (thm (equal (append (append x x) x)
                          (append x x x))))
             (if erp
                 (deflabel foo :doc "Attempt failed.")
               (value (list :succeeded-with val))))

     ; Use extra argument of t to avoid ``charging'' steps for the indicated
     ; form.
     (with-prover-step-limit
      500
      (encapsulate
       ()
       (with-prover-step-limit
        500
        t ; Don't charge prover steps for this first defthm.
        (defthm test1
          (equal (append x (append y z))
                 (append (append x y) z))
          :rule-classes nil))
       (defthm test2
         (equal (append x (append y z))
                (append (append x y) z))
         :rule-classes nil)))

     General Forms:
     (with-prover-step-limit expr form)
     (with-prover-step-limit expr flg form)

where form is an arbitrary form to evaluate, and expr evaluates either,
nil, or to a natural number not exceeding the value of
*default-step-limit*, or to the special value, :START.  The extra
argument, flg, should be Boolean if supplied.

If the value of expr is a non-negative integer less than the value of
*default-step-limit*, then that value is the maximum number of prover
steps permitted during evaluation of form before an error occurs.  If
however the value of expr is nil or is the value of
*default-step-limit*, then no limit is placed on the number of prover
steps during processing of form.  Otherwise, that value is the keyword
:START, which is treated as follows.

     - If a preceding call of set-prover-step-limit is in force, then
     this call provides the new limit or establishes that there is no
     limit.  See SET-PROVER-STEP-LIMIT for a discussion of how
     this works.

     - Otherwise, if there is a superior call of
     with-prover-step-limit, then if the immediately superior such call
     did not establish a limit, then there is no limit.

     - Otherwise, if there is a superior call of
     with-prover-step-limit, then the limit is the current limit, i.e.,
     the difference between the limit established by that superior call
     and the number of prover steps already recorded since the point of
     entering that call.

     - Otherwise there is no limit.

Finally we describe the optional extra Boolean argument, flg.  If flg
is nil or omitted, then a running count of prover steps is maintained
after form is evaluated; otherwise, that count is not affected by
evaluation of form.  To see how this works when flg is nil or omitted,
consider an event of shape (progn form1 form2), where we are tracking
prover steps (say, because of a superior call of
with-prover-step-limit).  If n is the number of prover steps available
when the progn form is entered, and if s prover steps are executed
while evaluating form1, then n-s steps are available for evaluation of
form2 provided s does not exceed n; otherwise, an error occurs.  In
particular, this is the case if form is an event
(with-prover-step-limit k form1').  However, if form is an event
(with-prover-step-limit k t form1'), then because of the extra argument
of t, no steps are "charged" to form; that is, all n steps, rather than
n-s steps, are available for evaluation of form2.

WITH-PROVER-TIME-LIMIT    limit the time for proofs

     Examples:

     ; Limit (mini-proveall) to about 1/4 second:
     (with-prover-time-limit 1/4 (mini-proveall))

     ; Limit (mini-proveall) to about 1/4 second, even if surrounding call of
     ; with-prover-time-limit provides for a more restrictive bound:
     (with-prover-time-limit '(1/4) (mini-proveall))

     ; Limit the indicated theorem to about 1/50 second, and if the proof does not
     ; complete or it fails, then put down a label instead.
     (mv-let (erp val state)
             (with-prover-time-limit
              1/50
              (thm (equal (append (append x x) x)
                          (append x x x))))
             (if erp
                 (deflabel foo :doc "Attempt failed.")
               (value (list :succeeded-with val))))

     General Form:
     (with-prover-time-limit time form)

where time evaluates to a positive rational number or to a list
containing such, and form is arbitrary.  Logically,
(with-prover-time-limit time form) is equivalent to form.  However, if
the runtime for evaluation of form exceeds the value specified by time,
and if ACL2 notices this fact during a proof, then that proof will
abort, for example like this:

     ACL2 Error in ( DEFTHM PERM-REFLEXIVE ...):  Out of time in the rewriter.

If there is already a surrounding call of with-prover-time-limit that
has set up an expiration time, the inner with-prover-time-limit call is
not allowed to push that time further into the future unless the inner
time is specified as a list containing a rational, rather than as a
rational.

For a related utility based on prover steps instead of time, see
WITH-PROVER-STEP-LIMIT; also see SET-PROVER-STEP-LIMIT.  Those
utilities have the advantage of having platform-independent behavior,
unlike time limits, which of course are generally less restrictive for
faster processors.  But note that the prover steps counted need not
correspond closely to prover time.

Although with-prover-time-limit behaves like an ACL2 function in the
sense that it evaluates both its arguments, it is however actually a
macro that behaves as follows.  (1) The value of its first (time limit)
argument affects the evaluation of its second argument (by causing an
error during that evaluation if the time for completion is
insufficient).  (2) The second argument can return multiple values (see
MV), which are then returned by the call of
with-prover-time-limit.  (3) Thus, there is not a fixed number of
values returned by with-prover-time-limit.

If you find that the time limit appears to be implemented too loosely,
it may be because the prover only checks the time elapsed at certain
points during the proof process, for example at entry to the rewriter.
For example, if you write your own clause-processor that does an
expensive computation, the time is unlikely to be checked during its
execution.  If however you find the time limit seems to be ignored even
during ordinary prover operation, you are encouraged to email an
example to the ACL2 implementors with instructions on how to observe
the undesirable behavior.  This information can perhaps be used to
improve ACL2 by the insertion of more checks for expiration of the time
limit.

The rest of this documentation topic explains the rather subtle logical
story, and is not necessary for understanding how to use
with-prover-time-limit.  The ACL2 state object logically contains a
field called the acl2-oracle, which is an arbitrary true list of
objects.  This field can be read by a function called read-acl2-oracle,
which however is untouchable (see PUSH-UNTOUCHABLE), meaning
that it is cannot be called by ACL2 users.  The acl2-oracle field is
thus "secret".  Our claim is that any ACL2 session makes sense for
*some* value of acl2-oracle in the initial state for that session.
Logically, with-prover-time-limit is a no-op, just returning its second
value.  But under the hood, it provides a "hint" for the acl2-oracle,
so that (logically speaking) when its first element (car) is consulted
by ACL2's prover to see if the time limit has expired, it gets the
"right" answer (specifically, either nil if all is well or else a
message to print if the time limit has expired).  Logically, the
acl2-oracle is then cdr'ed -- that is, its first element is popped off
-- so that future results from read-acl2-oracle are independent of the
one just obtained.

WOF    direct standard output and proofs output to a file

     Example Form:
     (wof "tmp" (pso)) ; same as (psof "tmp")

     General Form:
     (wof filename form)

where filename is a writable filename and form is any form that
evaluates to an error triple (see PROGRAMMING-WITH-STATE), that
is, a multiple value of the form (mv erp val state).  All output to
channels standard-co and proofs-co will be directed to the indicated
file.  It is acceptable to replace filename with (quote filename).

Note that so-called comment-window output (see CW and see
OBSERVATION-CW) is not redirected by wof to a file, nor is printing
from a wormhole.

PARALLELISM    experimental extension for parallel execution and proofs

This documentation topic relates to an experimental extension of ACL2,
ACL2(p), created initially by David L. Rager.  See
COMPILING-ACL2P for how to build an executable image that supports
parallel execution.  Also see books/parallel for examples.  For a
completely different sort of parallelism, at the system level, see
PROVISIONAL-CERTIFICATION.

IMPORTANT NOTE.  We hope and expect that every evaluation result is
correctly computed by ACL2(p), and that every formula proved using
ACL2(p) is a theorem of the ACL2 logic (and in fact is provable using
ACL2).  However, we do not guarantee these properties.  Since ACL2(p)
is intended to be an aid in efficient evaluation and proof development,
we focus less on ironclad soundness and more on providing an efficient
and working implementation.  Nevertheless, if you encounter a case
where ACL2(p) computes an incorrect result, or produces a proof where
ACL2 fails to do so (and this failure is not discussed in
unsupported-waterfall-parallelism-features), please notify the
implementors.

The ACL2 source code provides experimental parallel execution and proof
capabilities.  For example, one of ACL2's strengths lies in its ability
to simulate industrial models efficiently, and it can also decrease the
time required for proofs about such models both by making use of
parallel evaluation and by dispatching proof subgoals in parallel.

While we aim to support Clozure Common Lisp (CCL), Steel Bank Common
Lisp (SBCL), and Lispworks, SBCL and Lispworks both currently sometimes
experience problems when evaluating the ACL2 proof process (the
"waterfall") in parallel.  Therefore, CCL is the recommend Lisp for
anyone that wants to use parallelism and isn't working on fixing those
problems.

COMPILING-ACL2P    compiling ACL2(p)

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.  See
PARALLEL and see PARALLELISM-TUTORIAL for an
introduction to parallel programming in ACL2.

You can build an experimental version of ACL2 that supports parallel
execution in the following host Common Lisp implementations:

     * CCL (OpenMCL)

     * Lispworks 6.0

     * SBCL with threads (feature :sb-thread)

The command below will compile ACL2 to support parallel execution,
including parallel execution during proofs.  Any non-empty string may
be used in place of t, and the value of LISP (shown here as ccl) is any
Lisp executable on which one can build ACL2(p) (see
PARALLELISM).

     make ACL2_PAR=t LISP=ccl

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

     make large DOC ACL2_PAR=t LISP=ccl

PARALLEL-PROGRAMMING    parallel programming in ACL2(p)

Here we document support for parallel programming in ACL2(p), an
experimental extension of ACL2; also see PARALLELISM.

Related topics other than immediate subtopics:

One of ACL2's strengths lies in its ability to execute industrial models
efficiently.  The ACL2 source code provides an experimental parallel
execution capability that can increase the speed of explicit evaluation,
including simulator runs using such models, and it can also decrease
the time required for proofs that make heavy use of the evaluation of
ground terms.

The parallelism primitives are plet, pargs, pand, por, and spec-mv-let.
Pand and por terminate early when an argument is found to evaluate to
nil or non-nil, respectively, thus potentially improving on the
efficiency of lazy evaluation.  Spec-mv-let is a modification of mv-let
that supports speculative and parallel execution.

Of the above five parallelism primitives, all but spec-mv-let allow for
limiting parallel execution (spawning of so-called "threads") depending
on resource availability.  Specifically, the primitives allow
specification of a size condition to control the granularity under
which threads are allowed to spawn.  You can use such granularity
declarations in recursively-defined functions to implement
data-dependent parallelism in their execution.

We recommend that in order to learn to use the parallelism primitives,
you begin by reading examples: see PARALLELISM-TUTORIAL.  That
section will direct you to further documentation topics.

In addition to providing parallel programming primitives, ACL2(p) also
provides the ability to execute the main ACL2 proof process in parallel.
See SET-WATERFALL-PARALLELISM for further details.

DEFLOCK    define a wrapper macro that provides mutual exclusion in ACL2(p)

This documentation topic relates to the experimental extension of ACL2
supporting parallel evaluation and proof; see PARALLELISM.

     Example Form:
     (deflock *my-lock*)

     General Form:
     (deflock *symbol*)

where *symbol* is a symbol whose first and last characters are both the
character #\*.

A call of this macro generates a definition of another macro, named
with-<modified-lock-symbol>, where <modified-lock-symbol> is the given
symbol with the leading and trailing * characters removed.  This newly
defined macro will guarantee mutually exclusive execution when called
in the body of the raw Lisp definition of a function, as is typically
the case for guard-verified functions, for :program mode functions, and
for calls of macro top-level.  (See GUARD-EVALUATION-TABLE for
details of how raw Lisp code might not be invoked when guard-checking
(see SET-GUARD-CHECKING) has value :none or :all.)

To see how mutual exclusion is guaranteed, consider the raw Lisp code
generated for the macro, with-<modified-lock-symbol>, that is introduced
by a call of deflock.  This code uses a lock (with the given *symbol*
as its name), which guarantees that for any two forms that are each in
the scope of a call of with-<modified-lock-symbol>, the forms do not
execute concurrently.

Note that a call of deflock expands into the application of progn to
two events, as illustrated below.

     ACL2 !>:trans1 (deflock *my-cw-lock*)
      (PROGN (TABLE LOCK-TABLE '*MY-CW-LOCK* T)
             (DEFMACRO WITH-MY-CW-LOCK (&REST ARGS)
                       (LIST* 'WITH-LOCK '*MY-CW-LOCK* ARGS)))
     ACL2 !>

Thus, deflock forms are legal embedded event forms (see
EMBEDDED-EVENT-FORM) for books as well as encapsulate and progn
events.

The following log shows a lock in action.  Recall that locks work as
expected in guard-verified and :program mode functions; they do not,
however, work in :logic mode functions that have not been
guard-verified, as illustrated below.

     ACL2 !>(deflock *my-cw-lock*)
     [[.. output omitted ..]]
      WITH-MY-CW-LOCK
     ACL2 !>(defun foo (n)
              (declare (xargs :guard (natp n) :verify-guards nil))
              (plet ((x1 (with-my-cw-lock (cw "~x0" (make-list n))))
                     (x2 (with-my-cw-lock (cw "~x0" (make-list n)))))
                    (and (null x1) (null x2))))
     [[.. output omitted ..]]
      FOO
     ACL2 !>(foo 20)
     (NIL NIL NIL NIL( NIL NIL NIL NIL NIL NILNIL  NIL NILNIL  NIL NILNIL
          NIL NILNIL NIL  NIL NILNIL  NIL NIL
     NIL      NILNIL  NIL NILNIL )
     NIL NIL NIL NIL NIL NIL NIL NIL)
     T
     ACL2 !>(verify-guards foo)
     [[.. output omitted ..]]
      FOO
     ACL2 !>(foo 20)
     (NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
          NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL)
     (NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
          NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL)
     T
     ACL2 !>

EARLY-TERMINATION    early termination for pand and por.

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

The evaluation of (and expr1 expr2) returns nil if expr1 evaluates to
nil, avoiding the evaluation of expr2.  More generally, the evaluation
of (and expr1 expr2 ... exprk) terminates with a return value of nil as
soon as any expri evaluates to nil -- no exprj is evaluated in this
case for j > i.  This so-called "lazy evaluation" of and terms can thus
save some computation; roughly speaking, the smaller the i, the more
computation is saved.

If the above call of and is replaced by its parallel version, pand,
then there can be even more opportunity for skipping work.  The
arguments to pand can be evaluated in parallel, in which case the first
such evaluation that returns with a value of nil, if any, causes the
remaining such evaluations to abort.

Consider the following functions that compute whether a tree is valid
(see GRANULARITY for a discussion of the granularity form).

     (defun valid-tip (x)
       (declare (xargs :guard t))
       (or (eq x 'A)
           (eq x 'T)
           (eq x 'C)
           (eq x 'G)))

     (defun pvalid-tree (x depth)
       (declare (xargs :guard (natp depth)))
       (if (atom x)
           (valid-tip x)
         (pand (declare (granularity (< depth 10)))
               (pvalid-tree (car x) (1+ depth))
               (pvalid-tree (cdr x) (1+ depth)))))

We would like to stop execution as soon as any tip is found to be
invalid.  So, when computing the conjunction of terms by using pand,
once one of those terms evaluates to nil, the computations for the
other terms are aborted and the pand call returns nil.  By using pand,
we can in principle attain a speedup factor greater than the number of
available cores.

The concept of early termination also applies to por, except that early
termination occurs when an argument evaluates to non-nil.

ERROR-TRIPLES-AND-PARALLELISM    how to avoid error triples in ACL2(p)

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

ACL2 supports the use of error triples in many features; e.g.,
computed-hints.  (For background on error triples, see
PROGRAMMING-WITH-STATE.)  However, ACL2(p) does not support the use of
error triples in some of these features (e.g., computed-hints) while
waterfall-parallelism is enabled.

You may see an error message like the following when running ACL2(p)
with waterfall-parallelism enabled:

     ACL2 Error in ( THM ...):  Since we are translating a form in ACL2(p)
     intended to be executed with waterfall parallelism enabled, the form
     (MY-STATE-MODIFYING-COMPUTED-HINT ID STATE) was expected to represent
     an ordinary value, not an error triple (mv erp val state), as would
     be acceptable in a serial execution of ACL2.  Therefore, the form returning
     a tuple of the form (* * STATE) is an error.  See :DOC unsupported-
     waterfall-parallelism-features and :DOC error-triples-and-parallelism
     for further explanation.

In this particular example, the cause of the error was trying to use a
computed hint that returned state, which is not allowed when executing
the waterfall in parallel (see
UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES for other related
information).

Often, the only reason users need to return state is so they can perform
some output during the proof process.  In this case, we suggest using
one of the state-free output functions, like cw or observation-cw.  If
the user is concerned about the interleaving of their output with other
output, these calls can be surrounded with the macro with-output-lock.

Another frequent reason users return state is so they can cause a soft
error and halt the proof process.  In this case, we suggest instead
calling er with the hard or hard? severity.  By using these mechanisms,
the user avoids modifying state, a requirement for much of the code
written in ACL2(p).

You may encounter other similar error messages when using
computed-hints, custom-keyword-hints, or override-hints.  Chances are
that you are somehow returning an error triple when an ordinary value
is needed.  If this turns out not to be the case, please let the ACL2
implementors know.

GRANULARITY    limit the amount of parallelism

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

Some function calls are on arguments whose evaluation time is long
enough to warrant parallel execution, while others are not.  A
granularity form can be used to make appropriate restrictions on the
use of parallelism.

For example, consider the Fibonacci function.  Experiments have
suggested that execution time can be reduced if whenever the argument
is less than 27, a serial version of the Fibonacci function is called.
One way to utilize this information is to write two definitions of the
Fibonacci function, one serial and one parallel.

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (binary-+ (fib (- x 1))
                          (fib (- x 2))))))

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             ((< x 27) (binary-+ (fib (- x 1))
                                 (fib (- x 2))))
             (t (pargs (binary-+ (pfib (- x 1))
                                 (pfib (- x 2)))))))

We realize quickly that writing both of these function definitions is
cumbersome and redundant.  This problem can be avoided by using a
granularity declaration with a parallelism primitive.  This form ensures
that a call is parallelized only if resources are available and the
granularity form evaluates to a non-nil value at the time of the call.
Below is a definition of the Fibonacci function using a granularity
form.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (pargs (declare (granularity (>= x 27)))
                       (binary-+ (pfib (- x 1))
                                 (pfib (- x 2)))))))

A granularity form can reference an extra formal parameter that
describes the call depth of the function the user is parallelizing.
Consider for example the following parallel mergesort function, based
on Davis's Ordered Sets library.  It splits the data into symmetric
chunks for computation, so we increment the depth argument during the
recursive call on both the car and cdr.

     (include-book "finite-set-theory/osets/sets" :dir :system)
     (defun sets::pmergesort-exec (x depth)
       (declare (xargs :mode :program))
       (cond ((endp x) nil)
             ((endp (cdr x)) (sets::insert (car x) nil))
             (t (mv-let (part1 part2)
                        (sets::split-list x nil nil)
                        (pargs
                         (declare (granularity (< depth 2)))
                         (sets::union (sets::pmergesort-exec part1
                                                             (1+ depth))
                                      (sets::pmergesort-exec part2
                                                             (1+ depth))))))))

A less intrusive method (i.e., not requiring an extra formal parameter
like the depth argument just above), which however can be less
efficient, involves analyzing the data itself for structural
properties.  For example:

     (defun some-depth-exceeds (x n)
       (declare (xargs :guard (natp n)))
       (if (atom x)
           nil
         (if (zp n)
             t
           (or (some-depth-exceeds (car x) (1- n))
               (some-depth-exceeds (cdr x) (1- n))))))

     (defun valid-tip (x)
       (declare (xargs :guard t))
       (or (eq x 'A)
           (eq x 'T)
           (eq x 'C)
           (eq x 'G)))

     (defun pvalid-tree (x)
       (declare (xargs :guard t))
       (if (atom x)
           (valid-tip x)
         (pand (declare (granularity (some-depth-exceeds x 3)))
               (pvalid-tree (car x))
               (pvalid-tree (cdr x)))))

If you experiment with calls of pvalid-tree, you are likely to find that
the "speedup" it provides over a corresponding serial version is, in
fact, a slowdown!  The problem is likely that some-depth-exceeds is an
expensive function to run repeatedly.  Instead of the approach above,
it is often handy to add an extra formal parameter in order to allow
for more efficient granularity forms, as we have done above in the
definition of SETS::pmergesort-exec.

PAND    parallel, Boolean version of and

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     Example Forms:
     (pand (subsetp-equal x y)
           (subsetp-equal y x))

     (pand (declare
            (granularity
             (and (> (length x) 500)
                  (> (length y) 500))))
            (subsetp-equal x y)
            (subsetp-equal y x))

     General Form:
     (pand (declare (granularity expr)) ; optional granularity declaration
           arg1 ... argN)

where N >= 0 and each argi and expr are arbitrary terms.

Pand evaluates its arguments in parallel.  It returns a Boolean result:
nil if any argument evaluates to nil, else t.  Note that pand always
returns a Boolean result, even though and can return a non-nil value
other than t, namely the value of its last argument.  (A moment's
reflection will make it clear that in order for por to parallelize
efficiently, it needs to return a Boolean value; so pand returns a
Boolean value for consistency with por.)

Another difference between pand and and is that for a call of pand,
even if an argument evaluates to nil, a subsequent argument may be
evaluated.  Consider the following example (where cw prints a string;
see CW).

     (defun bar ()
       (pand (equal (make-list 100000) nil) ; evaluates to nil
             (cw "hello world~%")))

When (bar) is evaluated, the above arguments of pand can execute in
parallel, causing "hello world" to be printed to the terminal.  If we
had used and rather than pand, then since (equal (make-list 100000)
nil) evaluates to nil, the above call of cw would be avoided and no
such printing would take place.  Even with pand, such printing _might_
not take place, depending on resources, timing of thread creation, and
whether or not parallel execution is enabled (see
SET-PARALLEL-EXECUTION).

Note that unlike the case for and, the definition of pand does not
provide (consp x) as a guard to (car x) in the call of pand below:

     (defun h (x)
       (declare (xargs :guard t))
       (pand (consp x) (equal (car x) 'foo)))

As a result, guard verification will fail for the above definition.  If
pand were replaced by and, then guard verification would succeed.

See PARALLELISM-TUTORIAL for another example.  Also see
PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.  Finally
see EARLY-TERMINATION to read how pand can offer more
efficiency than and by avoiding evaluation of some of its arguments.

PARALLEL-EXECUTION    for ACL2(p): configure parallel execution

See SET-PARALLEL-EXECUTION for how to configure parallel
execution for calls of plet, pargs, pand, por (but not spec-mv-let).

PARALLELISM-AT-THE-TOP-LEVEL    parallel execution in the ACL2 top-level loop

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

Calls of parallelism primitives made explicitly in the ACL2 top-level
loop, as opposed to inside function bodies, will never cause parallel
execution.  Such calls will either execute with serial execution or
will cause an error; see SET-PARALLEL-EXECUTION.  For a way
around this restriction, see TOP-LEVEL.

Consider for example the following call of pargs in the ACL2 top-level
loop.  Instead of executing pargs, ACL2 macroexpands away this call,
leaving us with serial execution of the arguments to the cons call, or
else causes an error (see SET-PARALLEL-EXECUTION).  If there is
no error, then

     (pargs (cons (expensive-fn-1 4) (expensive-fn-2 5)))

expands into:

     (cons (expensive-fn-1 4) (expensive-fn-2 5))

One trivial way to enable parallel execution of a form is to surround it
with a call to macro top-level.  Consider the following example.

     (top-level (pargs (cons (expensive-fn-1 4) (expensive-fn-2 5))))

Then in an executable image that supports parallel execution -- see
COMPILING-ACL2P for instructions on how to build such an
executable -- (expensive-fn-1 4) and (expensive-fn-2 5) can evaluate in
parallel.

A second way to enable parallel execution of a form is to place it
inside a function body.  For example, consider the following definition.

     (defun foo (x y)
       (pargs (cons (expensive-fn-1 x) (expensive-fn-2 y))))

Then in an executable image that supports parallel execution,
submission of the form (foo 4 5) can cause parallel execution of
(expensive-fn-1 4) and (expensive-fn-2 5).

Note that guards need not be verified in order to obtain parallel
execution.  The only restrictions on parallel execution are to use an
executable supporting it, to avoid calling parallelism primitives
directly in the top-level loop, to have sufficient resources
(especially, threads) available, and to avoid explicitly disabling
parallel execution (see SET-PARALLEL-EXECUTION).

PARALLELISM-PERFORMANCE    performance issues for parallel execution

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

See GRANULARITY for an important construct that limits the
spawning of parallel computations, which can be important when a
computation is too short-lived to warrant a separate thread.

There are times in which parallelism provides no speedup because of
garbage collection in the underlying Lisp implementation.  The
following example illustrates this phenomenon.  If you change the
granularity declaration so that the depth bound is 3, 4, or larger
instead of 2, you may still find no speedup.  In all cases you may find
that parallelism results in a significantly greater time spent in
garbage collection.

     (include-book "finite-set-theory/osets/sets" :dir :system)
     (defun sets::pmergesort-exec (x depth)
         (declare (xargs :mode :program))
         (cond ((endp x) nil)
               ((endp (cdr x)) (sets::insert (car x) nil))
               (t (mv-let (part1 part2)
                          (sets::split-list x nil nil)
                          (pargs
                           (declare (granularity (< depth 2)))
                           (sets::union (sets::pmergesort-exec part1
                                                               (1+ depth))
                                        (sets::pmergesort-exec part2
                                                               (1+ depth))))))))
     (defconst *x* (reverse (fromto 1 400000)))
     (time$ (length (sets::pmergesort-exec *x* 0)))
     (set-parallel-execution nil)
     (time$ (length (sets::pmergesort-exec *x* 0)))

PARALLELISM-TUTORIAL    a tutorial on how to use the parallelism library.

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

In this topic we introduce the ACL2 parallelism primitives using the
example of a doubly-recursive Fibonacci function, whose basic
definition is as follows.  See PARALLELISM for a very
high-level summary of the parallelism capability described here, and
see COMPILING-ACL2P for how to build an executable image that
supports parallel execution.  Here, we assume that such an executable
is being used.

Serial Fibonacci

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

Introducing Pargs

A simple way to introduce parallelism into this function definition is
to wrap the addition expression with a call of pargs, and the arguments
to the addition will be computed in parallel whenever resources are
available.  As a result, we end up with a very similar and thus
intuitive function definition.  Note that we replaced + by binary-+,
since pargs expects a function call, not a macro call.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (pargs (binary-+ (pfib (- x 1))
                                 (pfib (- x 2)))))))

Introducing the Granularity Problem

After you submit the above two versions of the Fibonacci function, test
them with the following forms.

     (time$ (fib 10))
     (time$ (pfib 10))

Now increase the argument by increments of 5 to 10 until you find your
curiosity satisfied or your patience wearing thin.  You can interrupt
evaluation if necessary and return to the ACL2 loop.  You will
immediately notice that you have not increased execution speed, at
least not by much, by introducing parallelism.

First, consider the computation of (pfib 4).  Assuming resources are
available, (pfib 4) will create a thread for computing (pfib 3) and
another thread for (pfib 2).  It is easy to imagine that setting up each
thread takes much longer than the entire computation of (fib 4).

Second, we must realize that if we have two threads available for
computing (fib 10), then the evaluation of (fib 8) will probably
complete before the evaluation of (fib 9).  Once (fib 8) finishes,
parallelism resources will become available for the next recursive call
made on behalf of (fib 9).  If for example that call is (fib 3), we
will waste a lot of cycles just handing work to the thread that does
this relatively small computation.  We need a way to ensure that
parallelism resources are only used on problems of a "large" size.
Ensuring that only "large" problems are spawned is called the
"granularity problem."

In summary: We want to tell ACL2 that it can evaluate the arguments of
pargs in parallel only when the parameter of pfib is greater than some
threshold.  Our tests using CCL have suggested that 27 is a reasonable
threshold.

Explicit Programming for the Granularity Problem

One way to avoid the granularity problem is to duplicate code as
follows.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (if (> x 27) ; the granularity test
                    (pargs (binary-+ (pfib (- x 1))
                                     (pfib (- x 2))))
                  (binary-+ (pfib (- x 1))
                            (pfib (- x 2)))))))

Duplicating code is fundamentally a bad design principle, because it can
double the work for future maintenance.  A "granularity form" is an
expression

     (declare (granularity <form>))

that can allow threads to be spawned (without duplicating code)
whenever the evaluation of <form> results in a non-nil value.  It may
be placed inside any call of a parallelism primitive, in a position
documentated separately for each primitive.  Here is a definition of
pfib using this feature for a call of the parallelism primitive pargs.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (pargs
                 (declare (granularity (> x 27)))
                 (binary-+ (pfib (- x 1))
                           (pfib (- x 2)))))))

Test each version as follows (or substitute your own natural number for
33).

       (time$ (fib 33))
       (time$ (pfib 33))

Another Granularity Issue Related to Thread Limitations

Our implementation of parallelism primitives has the property that once
a thread is assigned a computation, that assignment stays in effect
until the computation is complete.  In particular, if a thread
encounters a parallelism primitive that spawns child threads, the
parent thread stays assigned, waiting until the child computations
complete before it can continue its own computation.  In the meantime,
the parent thread reduces the number of additional threads that Lisp
can provide by 1, rather than being reassigned to do other work.

How can this lack of reassignment affect the user?  Consider, for
example, the application of a recursive function to a long list.
Imagine that this function is written so that the body contains a
recursive call, for example as (pargs (process (car x)) (recur (cdr
x))).  Each such pargs call that spawns child work must wait for its
children, one of which is the work of evaluating (recur (cdr x)), to
complete.  There is an ACL2 limit on how much pending work can be in
the system, limiting the number of pargs calls that can result in
parallel execution.  For example, if the ACL2 limit is k and each call
of pargs actually spawns threads for evaluating  its arguments, then
after k cdrs there will be no further parallel execution.

Possible solutions may include reworking of algorithms (for example to
be tree-based rather than list-based) or using appropriate granularity
forms.  We hope that future implementations will allow thread
"re-deployment" in order to mitigate this problem.  This problem
applies to plet, pargs, pand, por, and spec-mv-let.

Introducing Plet

We can use a let binding to compute the recursive calls of fib and then
add the bound variables together, as follows.

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (let ((a (fib (- x 1)))
                      (b (fib (- x 2))))
                  (+ a b)))))

By using the parallelism primitive plet, we can introduce parallelism
much as we did using pargs, with an optional granularity form, as
follows.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (plet
                 (declare (granularity (> x 27)))
                 ((a (pfib (- x 1)))
                  (b (pfib (- x 2))))
                 (+ a b)))))

Notice that this time, we were able to use + rather than being forced to
use binary-+.  Unlike pargs, which expects a function call (not a macro
call), plet allows macros at the top level of its body.

Introducing Pand (By Way of a Tree Validation Example)

Consider "genetic trees" that contains leaves of DNA elements, in the
sense that each tip is one of the symbols A, G, C, or T.  First we
define the function valid-tip which recognizes whether a tip contains
one of these symbols.

     (defun valid-tip (tip)
       (declare (xargs :guard t))
       (or (eq tip 'A)
           (eq tip 'G)
           (eq tip 'C)
           (eq tip 'T)))

Now we define a function that traverses the tree, checking that every
tip is valid.

     (defun valid-tree-serial (tree)
       (declare (xargs :guard t))
       (if (atom tree)
           (valid-tip tree)
         (and (valid-tree-serial (car tree))
              (valid-tree-serial (cdr tree)))))

We also define a parallel version.

     (defun valid-tree-parallel (tree)
       (declare (xargs :guard t))
       (if (atom tree)
           (valid-tip tree)
         (pand (valid-tree-parallel (car tree))
               (valid-tree-parallel (cdr tree)))))

Before we can time the functions, we need to create test trees.  We have
found that test trees need to be approximately 1 gigabyte before we
clearly see speedup, and we make them asymmetric to demonstrate the
ability of our implementation to adapt to asymmetric data.  We can
create the trees with the execution of the following forms.

     (defun make-valid-binary-tree (x)
       (declare (xargs :mode :program))
       (if (< x 0)
           (cons (cons 'C 'G) (cons 'A 'T))
         (cons (make-valid-binary-tree (- x 2)) ; 2 to make asymmetric
               (make-valid-binary-tree (- x 1)))))

     (defconst *valid-tree* (make-valid-binary-tree 30)) ; takes awhile
     (defconst *invalid-tree* (cons *valid-tree* nil)) ; nil is invalid tip

We can time our functions with the forms:

     (time$ (valid-tree-serial *valid-tree*))
     (time$ (valid-tree-parallel *valid-tree*))

Unfortunately, the serial version runs faster than the parallelism
version; however, there is more to this story.

Demonstrating Early Termination with an Invalid Tree

Now observe this magic:

     (time$ (valid-tree-serial   *invalid-tree*))
     (time$ (valid-tree-parallel *invalid-tree*))

The serial version took awhile, while the parallel version finished
almost immediately.  The test for validation was split into testing the
car and the cdr of the *invalid-tree* root, and since the cdr was equal
to nil, its test returned immediately.  This immediate return quickly
interrupted the computation associated with the car, and returned the
result.

Granularity with Pand

We can also define a parallel version with a granularity form:

     (defun valid-tree-parallel (tree depth)
       (declare (xargs :guard (natp depth)))
       (if (atom tree)
           (valid-tip tree)
         (pand
          (declare (granularity (< depth 5)))
          (valid-tree-parallel (car tree) (1+ depth))
          (valid-tree-parallel (cdr tree) (1+ depth)))))

We can test this form by executing our previous forms.  You will
probably find some speedup on a machine with several cores available,
but more speedup can likely be obtained with an expensive test on the
leaves in place of valid-tip.

     (time$ (valid-tree-serial   *valid-tree*))
     (time$ (valid-tree-parallel *valid-tree* 0))

Introducing Por

Por can be used in the same way as pand, but with early termination
occurring when an argument evaluates to a non-nil value, in which case
the value returned is t.  Finally, por also supports the use of a
granularity form.

PARGS    parallel evaluation of arguments in a function call

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     Example Forms:
     (pargs (binary-+ (fibonacci (- x 1)) (fibonacci (- x 2))))

     (pargs (declare (granularity (> x 35)))
            (binary-+ (fibonacci (- x 1)) (fibonacci (- x 2))))

     General Form:
     (pargs (declare (granularity expr)) ; optional granularity declaration
            (f arg1 ... argN))

where N >= 0 and each argi and expr are arbitrary terms.  Logically,
pargs is just the identity macro, in the sense that the above forms can
logically be replaced by (f arg1 ... argN).  However, this pargs form
may parallelize the evaluation of arguments arg1 through argN before
applying function f to those results.  If the above granularity
declaration is present, then its expression (expr above) is first
evaluated, and if the result is nil, then such parallelism is avoided.
Even if parallelism is not thus avoided, parallelism may be limited by
available resources.

Since macros can change expressions in unexpected ways, it is illegal
to call pargs on a form that is a macro call.  To parallelize
computation of arguments to a macro, see PLET.

See PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.

PLET    parallel version of let

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     Example Forms:
     (plet ((a (fibonacci (- x 1)))
            (b (fibonacci (- x 2))))
           (+ a b))

     (plet (declare (granularity (> x 35)))
           ((a (fibonacci (- x 1)))
            (b (fibonacci (- x 2))))
           (+ a b))

     General Form:
     (plet (declare (granularity expr)) ; optional granularity declaration
           ((var1 val1)
            ...
            (varN valN))
           (declare ...) ... (declare ...) ; optional declarations
           body)

The syntax of plet is identical to the syntax of let, except that plet
permits an optional granularity declaration in the first argument
position; see GRANULARITY.  In the logic a call of plet
macroexpands to the corresponding call of let, where the granularity
declaration (if any) is dropped.

Plet cause the evaluation of each vali above to be done in parallel
before processing the body.  If the above granularity declaration is
present, then its expression (expr above) is first evaluated, and if the
result is nil, then such parallelism is avoided.  Even if parallelism is
not thus avoided, parallelism may be limited by available resources.

See PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.

POR    parallel, Boolean version of or

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     Example Forms:
     (por (subsetp-equal x y)
          (subsetp-equal y x))

     (por (declare
           (granularity
            (and (> (length x) 500)
                 (> (length y) 500))))
           (subsetp-equal x y)
           (subsetp-equal y x))

     General Form:
     (por (declare (granularity expr)) ; optional granularity declaration
          arg1 ... argN)

where N >= 0 and each argi and expr are arbitrary terms.

Por evaluates its arguments in parallel.  It returns a Boolean result:
t if any argument evaluates to non-nil, else nil.  Note that while or
returns the first non-nil value from evaluating its arguments
left-to-right (if any such value is not nil) por always returns a
Boolean result, in support of efficiency (see EARLY-TERMINATION)
in light of the nondeterministic order in which argument values are
returned.

Another difference between por and or is that for a call of por, even
if the an argument's value is not nil, a subsequent argument may be
evaluated.  See PAND for a discussion of the analogous property
of pand.  In particular, guards generated from calls of por may not
assume for an argument that the preceding arguments evaluated to nil.

See PARALLELISM-TUTORIAL for another example.  Also see
PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.  Finally
see EARLY-TERMINATION to read how por can offer more efficiency
than or by avoiding evaluation of some of its arguments.

SPEC-MV-LET    modification of mv-let supporting speculative and parallel execution

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     Example Form:
     (defun pfib-with-step-count (x)
       (declare (xargs :mode :program))
       (if (or (zp x) (< x 33))
           (fib-with-step-count x)
         (spec-mv-let
          (a cnt1)
          (pfib-with-step-count (- x 1))
          (mv-let (b cnt2)
                  (pfib-with-step-count (- x 2))
                  (if t
                      (mv (+ a b)
                          (+ 1 cnt1 cnt2))
                    (mv "speculative result is always needed"
                        -1))))))

     General Form:
     (spec-mv-let
      (v1 ... vn)  ; bind distinct variables
      <spec>       ; evaluate speculatively; return n values
      (mv-let      ; or, use mv?-let if k=1 below
       (w1 ... wk) ; bind distinct variables
       <eager>     ; evaluate eagerly
       (if <test>  ; use results from <spec> if true
           <typical-case> ; may mention v1 ... vn
         <abort-case>)))  ; does not mention v1 ... vn

Our design of spec-mv-let is guided by its use in ACL2 source code to
parallelize part of ACL2's proof process, in the experimental parallel
extension of ACL2.  The user can think of spec-mv-let as a speculative
version of mv-let.  (In ordinary ACL2, the semantics agree with this
description but without speculative or parallel execution.)

Evaluation of the above general form proceeds as suggested by the
comments.  First, <spec> is executed speculatively.  Control then
passes immediately to the mv-let call, without waiting for the result
of evaluating <spec>.  The variables (w1 ... wk) are bound to the
result of evaluating <eager>, and then <test> is evaluated.  If the
value of <test> is true, then the values of (v1 ... vn) are needed, and
<typical-case> blocks until they are available.  If the value of <test>
is false, then the values of (v1 ... vn) are not needed, and the
evaluation of <spec> may be aborted.

The calls to mv-let and to if displayed above in the General Form are
an essential part of the design of spec-mv-let, and are thus required.

The following definition of fib-with-step-count completes the example
above:

     (defun fib-with-step-count (x)
     (declare (xargs :mode :program))
     (cond ((<= x 0)
            (mv 0 1))
           ((= x 1) (mv 1 1))
           (t (mv-let (a cnt1)
                      (fib-with-step-count (- x 1))
                      (mv-let (b cnt2)
                              (fib-with-step-count (- x 2))
                              (mv (+ a b)
                                  (+ 1 cnt1 cnt2)))))))

WITH-OUTPUT-LOCK    provides a mutual-exclusion mechanism for performing output in parallel

This documentation topic relates to an experimental extension of ACL2,
ACL2(p), created initially by David L. Rager.  See
COMPILING-ACL2P for how to build an executable image that supports
parallel execution.  Also see distributed directory books/parallel/ for
examples.

One may wish to perform output while executing code in parallel.  If
threads are allowed to print concurrently, the output will be
interleaved and often unreadable.  To avoid this, the user can surround
forms that perform output with the with-output-lock macro.

Take the following definition of pfib as an example.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((mbe :logic (or (zp x) (<= x 0))
                   :exec (<= x 0))
              0)
             ((= x 1) 1)
             (t (plet (declare (granularity t))
                      ((a (prog2$ (cw "Computing pfib ~x0~%" (- x 1))
                                  (pfib (- x 1))))
                       (b (prog2$ (cw "Computing pfib ~x0~%" (- x 2))
                                  (pfib (- x 2)))))
                      (+ a b)))))

With parallel-execution enabled, a call of (pfib 5)results in
non-deterministically interleaved output, for example as follows.

     ACL2 !>(pfib 5)
     CComputing pfib 4
     omputing pfib 3
     ComCpuotmipnugt ipnfgi bp fib3
     2
     Computing pCfiobm put2i
     ng pfib 1
     Computing pfib Co1mp
     uting pfib 0
     CCoommppuuttiinngg  ppffiibb  12

     ComCpuotmipnugt ipnfgi bp fib1
     0
     CoCmopmuptuitnign gp fpifbi b 1
     0
     5
     ACL2 !>

If the user instead surrounds the calls to cw with the macro
with-output-lock, as in the following session, the output will no longer
be interleaved.

     ACL2 !>
     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((mbe :logic (or (zp x) (<= x 0))
                   :exec (<= x 0))
              0)
             ((= x 1) 1)
             (t (plet (declare (granularity t))
                      ((a (prog2$ (with-output-lock
                                   (cw "Computing pfib ~x0~%" (- x 1)))
                                  (pfib (- x 1))))
                       (b (prog2$ (with-output-lock
                                   (cw "Computing pfib ~x0~%" (- x 2)))
                                  (pfib (- x 2)))))
                      (+ a b)))))

     <snip>

     ACL2 !>(pfib 5)
     Computing pfib 4
     Computing pfib 3
     Computing pfib 3
     Computing pfib 2
     Computing pfib 2
     Computing pfib 1
     Computing pfib 2
     Computing pfib 1
     Computing pfib 1
     Computing pfib 0
     Computing pfib 1
     Computing pfib 0
     Computing pfib 1
     Computing pfib 0
     5
     ACL2 !>

PARALLEL-PROOF    parallel proof in ACL2(p)

Here we document support for parallel proof in ACL2(p), an experimental
extension of ACL2; also see PARALLELISM, and for parallel
programming in particular, see PARALLEL-PROGRAMMING.

Related topics other than immediate subtopics:

ACL2P-KEY-CHECKPOINTS    key checkpoints in ACL2(p)

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

For printing output, the parallel version of the waterfall follows the
precedent of gag-mode.  The idea behind gag mode is to print only the
subgoals most relevant to debugging a failed proof attempt.  These
subgoals are called 'key checkpoints' (see SET-GAG-MODE for the
definition of "key" and "checkpoint"), and we restrict the default
output mode for the parallel version of the waterfall to printing
checkpoints similar to these key checkpoints.

Related topics other than immediate subtopics:

As of this writing, we are aware of exactly one discrepancy between gag
mode's key checkpoints and the parallel version of the waterfall's
checkpoints.  This discrepancy occurs when using "by" hints (see
HINTS).  As an example, take the following form, which attempts to
prove a non-theorem:

     (thm (equal (append x y z) (append z (append y x)))
          :hints (("Subgoal *1/2'''" :by nil)))

With waterfall parallelism enabled, Subgoal *1/2" will be printed as a
key checkpoint.  This is different from using gag-mode while running
the serial version of the waterfall, which skips printing the subgoal
as a checkpoint.

For those familiar with the ACL2 waterfall, we note that that the
parallel version of the waterfall prints key checkpoints that are
unproved in the following sense: a subgoal is a key checkpoint if it
leads, in the current call of the waterfall, to a goal that is pushed
for induction.

DEFAULT-TOTAL-PARALLELISM-WORK-LIMIT    for ACL2(p): returns the default value for global total-parallelism-work-limit

See SET-TOTAL-PARALLELISM-WORK-LIMIT.

PARALLEL-PUSHING-OF-SUBGOALS-FOR-INDUCTION    consequences of how parallelized proofs of subgoals are pushed for induction

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

The following discussion, concerning the naming of subgoals pushed for
proof by induction and the timeliness of aborting when two or more
goals are pushed for proof by induction, only applies when waterfall
parallelism is enabled (see SET-WATERFALL-PARALLELISM).

When two sibling subgoals (e.g. 4.5 and 4.6) both push goals to be
proved by induction (e.g., 4.6 pushes *1 and 4.5 pushes *2), a name is
assigned to the second pushed subgoal (e.g., *2) as if the first push
hasn't happened (e.g., *2 is mistakenly called *1).  In such a case, we
say what the name _could_ be.  The following non-theorem illustrates
how this works.

     (set-waterfall-parallelism :full)
     (thm (equal (append (car (cons x x)) y z) (append x x y)))

There is another consequence of the way the parallelized waterfall
pushes subgoals for proof by induction.  Without waterfall parallelism
enabled, ACL2 sometimes decides to abort instead of pushing a goal for
later proof by induction, preferring instead to induct on the original
conjecture.  But with waterfall parallelism enabled, the prover no
longer necessarily immediately aborts to prove the original conjecture.
Suppose for example that sibling subgoals, Subgoal 4.6 and Subgoal 4.5,
each push a subgoal for induction.  If the waterfall is performing the
proof of each of these subgoals in parallel, the proof will no longer
abort immediately after the second push occurs, that is at Subgoal 4.5.
As a result, the prover will continue through Subgoal 4.4, Subgoal 4.3,
and beyond.  It is not until the results of combining the proof results
of Subgoal 4.6 with the results from the remaining sibling subgoals
(4.5, 4.4, and so on), that the proof attempt will abort and revert to
prove the original conjecture by induction.  This example illustrates
behavior that is rather like the case that :otf-flg is t, in the sense
that the abort does not happen immediately, but also rather like the
case that :otf-flg is nil, in the sense that the abort does occur
before getting to Subgoal 3.

UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES    proof features not supported with waterfall-parallelism enabled

For a general introduction to ACL2(p), an experimental extension of
ACL2 that supports parallel execution and proof, see
PARALLELISM.  Please note that although this extension is usable and,
we hope, robust in its behavior, there are still known issues to
address beyond those listed explicitly below.  While we expect ACL2(p)
to perform correctly, it may never have the same level of attention to
correctness as is given to ACL2; see PARALLELISM, specifically
the "IMPORTANT NOTE" there.

Below we list proof features of ACL2 that are not yet supported when
parallel execution is enabled for the primary ACL2 proof process,
generally known as "the waterfall", typically by calling
set-waterfall-parallelism.

Please note that this topic is limited to the case that such waterfall
parallelism is enabled.  We believe that all ACL2 proof procedures are
supported when waterfall parallelism is disabled, even in executables
that support parallelism (see COMPILING-ACL2P).

Without a trust tag (see DEFTTAG): We support clause-processors,
computed-hints, and custom-keyword-hints that do not modify state, but
we do not permit override-hints, regardless of whether they modify
state.  With a trust tag, the user can use clause-processors that
modify state and can also use override-hints (see
SET-WATERFALL-PARALLELISM-HACKS-ENABLED for a convenient mechanism for
adding a trust tag).  See ERROR-TRIPLES-AND-PARALLELISM for a
discussion of how to avoid modifying state in such situations.
Regardless of whether a trust tag is active: We do not support checkers
of custom-keyword-hints to be anything but the default checker.

GNU Make versions 3.81 and 3.82 formerly caused a lot of problems
(version 3.80 somewhat less so), at least on Linux, when certifying
books with ACL2 built on a host Lisp of CCL using make (see
BOOK-MAKEFILES).  CCL was updated around March 23, 2011 to fix this
problem, so if you get segfaults (for example) with CCL, try updating
your CCL installation.

Book certification should generally work but may present some issues,
including the following.

     o The standard make-based process for book certification will not
     use waterfall-parallelism, which is disabled by default (even when
     compiling-acl2p by using the ACL2_PAR flag).  See
     BOOK-MAKEFILES, which explains that acl2-customization files are
     ignored during that process unless specified explicitly on the
     command line or in the environment.

     o A book certified with ACL2(p) might subsequently cause an error
     when included with ACL2.  As of this writing, however, we have
     only seen this for a book in which deftheory-static is used.

     o In general, ACL2(p) is primarily intended to support more rapid
     interactive development.  While we are unaware of an unsoundness
     likely to affect an ACL2(p) user, we suggest using ACL2 for final
     book certification, rather than ACL2(p), to lower the risk of
     unsound book certification.

Proof output can contain repeated printing of the same subgoal name.

Gag-mode isn't officially supported, although it has proved helpful to
use ACL2(p) in conjunction with (set-gag-mode t) (because this setting
suppresses the output that occurs outside the waterfall).  This being
said, ACL2(p) also prints key checkpoints (for example see
INTRODUCTION-TO-KEY-CHECKPOINTS), but with a notion of "key
checkpoint" that does not take into account whether the goal is later
proved by induction.  See ACL2P-KEY-CHECKPOINTS for further
explanation of these key checkpoints.  Note that pso is also not
supported.

The :brr utility is not supported.

The accumulated-persistence utility is not supported.

Time limits (see WITH-PROVER-TIME-LIMIT) aren't supported.

The timing information printed at the end of a proof attempt may be
somewhat inaccurate.  Consider using time$ to obtain timing information.

The use of wormholes is not recommended, as there may be race
conditions.

Output specific to :OR hints is disabled.

Proof trees are likely not to work as originally designed.

The use of set-inhibit-output-lst may not fully inhibit proof output.

Interrupting a proof attempt is not yet properly supported.  At a
minimum, interrupts are trickier with waterfall parallelism enabled.
For one, the user typically needs to issue the interrupt twice before
the proof attempt is actually interrupted.  Additionally, on rare
occasions the theorem is registered as proved, even though the prover
did not finish the proof.  If this occurs, issue a :u (see UBT)
and you will likely be at a stable state.

Also with regards to interrupting a proof attempt, sometimes the user
may need to issue a :q and lp to reset properly the parallelism
implementation to a stable state.  The primary symptom that the user is
experiencing this issue is that threads will continue to compute in the
background, even though there should be no proof attempt in progress.
The user can observe this symptom by examining the CPU utilization of
their ACL2 process, for example on Linux/Unix with the shell process
top.  Lisp usage greater than a few percent is indicative of this
problem.

Because of how ACL2 arrays are designed, the user may find that, in
practice, ACL2 arrays work (but perhaps with some slow-array-warning
messages).  However, we are aware of race conditions that can cause
problems.

Instead of dynamically monitoring rewrites, dmr instead dynamically
outputs information helpful for debugging the performance of proof
parallelism.  The instructions concerning how to see this debugging
information are the same as the instructions for enabling dmr mode.

If you are working with LispWorks 6.0 or 6.0.1, then you may see
messages about misaligned conses.  The state of the system may be
corrupted after such a message has been printed.  This LispWorks bug is
fixed in LispWorks 6.1.

The waterfall parallelism mode :resource-and-timing-based is not fully
supported when the host Lisp is other than CCL.  It may work, but we
have not attempted to address a potential race condition.

(Comment for ACL2(h) users; see HONS-AND-MEMOIZATION.)
Memoization may not work as intended when executing in parallel
(including the waterfall).  In an effort to be helpful to the user, the
functions automatically memoized by ACL2(h) are unmemoized when setting
waterfall parallelism to anything but nil.  Those exact functions are
again memoized once waterfall parallelism is disabled.  Additionally,
any functions memoized within the ACL2 loop (by a call of memoize) are
also unmemoized when enabling waterfall parallelism and once again
memoized when disabling waterfall parallelism.  This is implemented by
returning the memoization state to what it was before enabling
waterfall parallelism.  As such, the user should be aware that any
changes made to the memoization state while waterfall parallelism is
enabled will be lost once waterfall parallelism is disabled.

WATERFALL-PARALLELISM    for ACL2(p): configuring the parallel execution of the waterfall

See SET-WATERFALL-PARALLELISM.

WATERFALL-PRINTING    for ACL2(p): configuring the printing within the parallelized waterfall

See SET-WATERFALL-PRINTING.

UNSUPPORTED-PARALLELISM-FEATURES    ACL2 features not supported in ACL2(p)

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.  See
PARALLEL and see PARALLELISM-TUTORIAL for an
introduction to parallel execution in ACL2.

For proof features of ACL2 that are not yet supported when parallel
execution is enabled for the primary ACL2 proof process, generally
known as "the waterfall", see
UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES.

Please note that this topic discusses ACL2 features that are disabled
when using ACL2(p) (see COMPILING-ACL2P).  These features are
disabled regardless of whether waterfall parallelism is enabled.

Calls of observation-cw simply convert to calls of cw, so suppressing
observations (see SET-INHIBIT-OUTPUT-LST) will not suppress
these messages.

Memoization is not supported when executing in parallel.  See
UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES for memoization details
related to waterfall parallelism.

Since, as of April 2012, garbage collection is inherently sequential,
ACL2(p) minimizes the use of garbage collection by setting a high
garbage collection threshold.  As a result, ACL2(p) is not expected to
perform well on machines with less memory than this threshold (1
gigabyte, as of April 2012).

In CCL, the underlying parallel execution engine is tuned for the
number of CPU cores (or hardware threads) actually available in the
machine.  SBCL and LispWorks are tuned for a machine with 16 CPU cores.

CCL is considered to be the "flagship Lisp" for parallel execution in
ACL2.  The SBCL and LispWorks implementations are thought to be
generally stable.  However, due to their relatively less common use,
the SBCL and LispWorks implementations are likely less robust than the
CCL implementation.

PROGRAMMING    programming in ACL2

This documentation topic is a parent topic under which we include
documentation topics for built-in functions, macros, and special forms
(see ACL2-BUILT-INS) as well as topics for notions important to
programming with ACL2.  If you don't find what you're looking for, see
the Index or see individual topics that may be more directly
appropriate; for example, see EVENTS for top-level event
constructorsr like defun.

Related topics other than immediate subtopics:

ACL2-BUILT-INS    built-in ACL2 functions

This documentation topic is a parent topic under which we include
documentation for built-in functions, macros, and special forms that are
typically used in programming.  For others, including those typically
used as top-level commands or those that create events (defun, defthm,
and so on), documentation may be found as a subtopic of some other
parent topic.  We do not document some of the more obscure functions
provided by ACL2 that do not correspond to functions of Common Lisp.

See any documentation for Common Lisp for more details on many of these
functions.

*    multiplication macro

* is really a macro that expands to calls of the function binary-*.  So
for example

     (* x y 4 z)

represents the same term as

     (binary-* x (binary-* y (binary-* 4 z))).

See BINARY-*.

* is a Common Lisp function.  See any Common Lisp documentation for
more information.

+    addition macro

+ is really a macro that expands to calls of the function binary-+.  So
for example

     (+ x y 4 z)

represents the same term as

     (binary-+ x (binary-+ y (binary-+ 4 z))).

See BINARY-+.

-    macro for subtraction and negation

See BINARY-+ for addition and see UNARY-- for negation.

Note that - represents subtraction as follows:

     (- x y)

represents the same term as

     (+ x (- y))

which is really

     (binary-+ x (unary-- y)).

Also note that - represents arithmetic negation as follows:

     (- x)

expands to

     (unary-- x).

/    macro for division and reciprocal

See BINARY-* for multiplication and see UNARY-/ for
reciprocal.

Note that / represents division as follows:

     (/ x y)

represents the same term as

     (* x (/ y))

which is really

     (binary-* x (unary-/ y)).

Also note that / represents reciprocal as follows:

     (/ x)

expands to

     (unary-/ x).

/ is a Common Lisp macro.  See any Common Lisp documentation for more
information.

/=    test inequality of two numbers

(/= x y) is logically equivalent to (not (equal x y)).

Unlike equal, /= has a guard requiring both of its arguments to be
numbers.  Generally, /= is executed more efficiently than a combination
of not and equal.

For a discussion of the various ways to test against 0, See
ZERO-TEST-IDIOMS.

/= is a Common Lisp function.  See any Common Lisp documentation for
more information.

1+    increment by 1

(1+ x) is the same as (+ 1 x).  See +.

1+ is a Common Lisp function.  See any Common Lisp documentation for
more information.

1-    decrement by 1

(1- x) is the same as (- x 1).  See -.

1- is a Common Lisp function.  See any Common Lisp documentation for
more information.

<    less-than

Completion Axiom (completion-of-<):

     (equal (< x y)
            (if (and (rationalp x)
                     (rationalp y))
                (< x y)
              (let ((x1 (if (acl2-numberp x) x 0))
                    (y1 (if (acl2-numberp y) y 0)))
                (or (< (realpart x1) (realpart y1))
                    (and (equal (realpart x1) (realpart y1))
                         (< (imagpart x1) (imagpart y1)))))))

Guard for (< x y):

     (and (rationalp x) (rationalp y))

Notice that like all arithmetic functions, < treats non-numeric inputs
as 0.

This function has the usual meaning on the rational numbers, but is
extended to the complex rational numbers using the lexicographic order:
first the real parts are compared, and if they are equal, then the
imaginary parts are compared.

<=    less-than-or-equal test

<= is a macro, and (<= x y) expands to the same thing as (not (< y x)).
See <.

<= is a Common Lisp function.  See any Common Lisp documentation for
more information.

=    test equality of two numbers

(= x y) is logically equivalent to (equal x y).

Unlike equal, = has a guard requiring both of its arguments to be
numbers.  Generally, = is executed more efficiently than equal.

For a discussion of the various ways to test against 0, See
ZERO-TEST-IDIOMS.

= is a Common Lisp function.  See any Common Lisp documentation for
more information.

>    greater-than test

> is a macro, and (> x y) expands to the same thing as (< y x).  See
<.

> is a Common Lisp function.  See any Common Lisp documentation for
more information.

>=    greater-than-or-equal test

>= is a macro, and (>= x y) expands to the same thing as (not (< x y)).
See <.

>= is a Common Lisp function.  See any Common Lisp documentation for
more information.

@    get the value of a global variable in state

     Examples:
     (+ (@ y) 1)
     (assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))

     General Form:
     (@ symbol)

where symbol is any symbol to which you have assigned a global value.
This macro expands into (f-get-global 'symbol state), which retrieves
the stored value of the symbol.

The macro f-get-global is closely related to @: (@ var) macroexpands to
(f-get-global 'var state).

The macro assign makes it convenient to set the value of a symbol.  The
:ubt operation has no effect on the global-table of state.  Thus, you
may use these globals to hang onto useful data structures even though
you may undo back past where you computed and saved them.

ABS    the absolute value of a real number

(Abs x) is -x if x is negative and is x otherwise.

The guard for abs requires its argument to be a rational (real, in
ACL2(r)) number.

Abs is a Common Lisp function.  See any Common Lisp documentation for
more information.

From "Common Lisp the Language" page 205, we must not allow complex x
as an argument to abs in ACL2, because if we did we would have to
return a number that might be a floating point number and hence not an
ACL2 object.

To see the ACL2 definition of this function, see PF.

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.

ACL2-NUMBERP    recognizer for numbers

(acl2-numberp x) is true if and only if x is a number, i.e., a rational
or complex rational number.

ACONS    constructor for association lists

(Acons key datum alist) equals the result of consing the pair (cons key
datum) to the front of the association list alist.

(Acons key datum alist) has a guard of (alistp alist).  Acons is a
Common Lisp function.  See any Common Lisp documentation for more
information.

To see the ACL2 definition of this function, see PF.

ADD-TO-SET    add a symbol to a list

     General Forms:
     (add-to-set x lst)
     (add-to-set x lst :test 'eql)   ; same as above (eql as equality test)
     (add-to-set x lst :test 'eq)    ; same, but eq is equality test
     (add-to-set x lst :test 'equal) ; same, but equal is equality test

For a symbol x and an object lst, (add-to-set-eq x lst) is the result
of consing x on to the front of lst, unless x is already a member of
lst, in which case the result is lst. The optional keyword, :TEST, has
no effect logically, but provides the test (default eql) used for
comparing x with successive elements of lst.

The guard for a call of add-to-set depends on the test.  In all cases,
the second argument must satisfy true-listp.  If the test is eql, then
either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
add-to-set and its variants:

     (add-to-set-eq x lst) is equivalent to (add-to-set x lst :test
     'eq);

     (add-to-set-equal x lst) is equivalent to (add-to-set x lst :test
     'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function add-to-set-equal.

ADD-TO-SET-EQ    See ADD-TO-SET.

ADD-TO-SET-EQL    See ADD-TO-SET.

ADD-TO-SET-EQUAL    See ADD-TO-SET.

ALISTP    recognizer for association lists

(alistp x) is true if and only if x is a list of cons pairs.

(alistp x) has a guard of t.

To see the ACL2 definition of this function, see PF.

ALLOCATE-FIXNUM-RANGE    set aside fixnums in GCL

(Allocate-fixnum-range fixnum-lo fixnum-hi) causes Gnu Common Lisp
(GCL) to create a persistent table for the integers between fixnum-lo
and fixnum-hi (both bounds inclusive). This table is referenced first
when any integer is boxed and the existing box in the table is used if
the integer is in bounds.  This can speed up GCL considerably by
avoiding wasteful fixnum boxing.  Here, fixnum-lo and fixnum-hi should
be fixnums, more specifically of type (signed-byte 30), with fixnum-lo
<= fixnum-hi.

When this function is executed in a Lisp implementation other than GCL,
it has no side effect.  This function always returns nil.

ALPHA-CHAR-P    recognizer for alphabetic characters

(Alpha-char-p x) is true if and only if x is a alphabetic character,
i.e., one of the characters #a, #b, ..., #z, #A, #B, ..., #Z.

The guard for alpha-char-p requires its argument to be a character.

Alpha-char-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

To see the ACL2 definition of this function, see PF.

ALPHORDER    total order on atoms

Alphorder is a non-strict total order, a "less than or equal," on
atoms.  By "non-strict total order" we mean a function that always
returns t or nil and satisfies the following properties.

     o Antisymmetry:  XrY & YrX -> X=Y

     o Transitivity:  XrY & YrZ -> XrZ

     o Trichotomy:  XrY v YrX

Also see LEXORDER, which extends alphorder to all objects.

(Alphorder x y) has a guard of (and (atom x) (atom y)).

Within a single type: rationals are compared arithmetically, complex
rationals are compared lexicographically, characters are compared via
their char-codes, and strings and symbols are compared with alphabetic
ordering.  Across types, rationals come before complexes, complexes
come before characters, characters before strings, and strings before
symbols.  We also allow for "bad atoms," i.e., atoms that are not legal
Lisp objects but make sense in the ACL2 logic; these come at the end,
after symbols.

To see the ACL2 definition of this function, see PF.

AND    conjunction

And is the macro for conjunctions.  And takes any number of arguments.
And returns nil if one of the arguments is nil, but otherwise returns
the last argument.  If there are no arguments, and returns t.

And is a Common Lisp macro.  See any Common Lisp documentation for more
information.

APPEND    concatenate zero or more lists

Append, which takes zero or more arguments, expects all the arguments
except perhaps the last to be true (null-terminated) lists.  It returns
the result of concatenating all the elements of all the given lists
into a single list.  Actually, in ACL2 append is a macro that expands
into calls of the binary function binary-append if there are at least
two arguments; if there is just one argument then the expansion is that
argument; and finally, (append) expands to nil.

Append is a Common Lisp function.  See any Common Lisp documentation for
more information.

ASH    arithmetic shift operation

(ash i c) is the result of taking the two's complement representation
of the integer i and shifting it by c bits:  shifting left and padding
with c 0 bits if c is positive, shifting right and dropping (abs c)
bits if c is negative, and simply returning i if c is 0.

The guard for ash requires that its arguments are integers.

Ash is a Common Lisp function.  See any Common Lisp documentation for
more information.

To see the ACL2 definition of this function, see PF.

ASSERT$    cause a hard error if the given test is false

     General Form:
     (assert$ test form)

where test returns a single value and form is arbitrary.  Semantically,
this call of assert$ is equivalent to form.  However, it causes a hard
error if the value of test is nil.  That hard error invokes the
function illegal, which has a guard that is equal to nil; so if you use
assert$ in code for which you verify guards, then a proof obligation
will be that the occurrence of test is never nil.

ASSIGN    assign to a global variable in state

     Examples:
     (assign x (expt 2 10))
     (assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))

     General Form:
     (assign symbol term)

where symbol is any symbol (with certain enforced exclusions to avoid
overwriting ACL2 system "globals") and term is any ACL2 term that could
be evaluated at the top-level.  Assign evaluates the term, stores the
result as the value of the given symbol in the global-table of state,
and returns the result.  (Note:  the actual implementation of the
storage of this value is much more efficient than this discussion of
the logic might suggest.)  Assign is a macro that effectively expands
to the more complicated but understandable:

     (pprogn (f-put-global 'symbol term state)
             (mv nil (f-get-global 'symbol state) state)).

The macro f-put-global is closely related to assign: (assign var val)
macroexpands to (f-put-global 'var val state).

The macro @ gives convenient access to the value of such globals.  The
:ubt operation has no effect on the global-table of state.  Thus, you
may use these globals to hang onto useful data structures even though
you may undo back past where you computed and saved them.

ASSOC    look up key in association list

     General Forms:
     (assoc x alist)
     (assoc x alist :test 'eql)   ; same as above (eql as equality test)
     (assoc x alist :test 'eq)    ; same, but eq is equality test
     (assoc x alist :test 'equal) ; same, but equal is equality test

(Assoc x alist) is the first member of alist whose car is x, or nil if
no such member exists.  The optional keyword, :TEST, has no effect
logically, but provides the test (default eql) used for comparing x
with the cars of successive elements of alist.

The guard for a call of assoc depends on the test.  In all cases, the
second argument must satisfy alistp.  If the test is eql, then either
the first argument must be suitable for eql (see EQLABLEP) or
the second argument must satisfy eqlable-alistp.  If the test is eq,
then either the first argument must be a symbol or the second argument
must satisfy symbol-alistp.

See EQUALITY-VARIANTS for a discussion of the relation between
assoc and its variants:

     (assoc-eq x alist) is equivalent to (assoc x alist :test 'eq);

     (assoc-equal x alist) is equivalent to (assoc x alist :test
     'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function assoc-equal.

Assoc is defined by Common Lisp.  See any Common Lisp documentation for
more information.

ASSOC-EQ    See ASSOC.

ASSOC-EQUAL    See ASSOC.

ASSOC-KEYWORD    look up key in a keyword-value-listp

If l is a list of even length of the form (k1 a1 k2 a2 ... kn an),
where each ki is a keyword, then (assoc-keyword key l) is the first
tail of l starting with key if key is some ki, and is nil otherwise.

The guard for (assoc-keyword key l) is (keyword-value-listp l).

To see the ACL2 definition of this function, see PF.

ASSOC-STRING-EQUAL    look up key, a string, in association list

(Assoc-string-equal x alist) is similar to assoc-equal.  However, for
string x and alist alist, the comparison of x with successive keys in
alist is done using string-equal rather than equal.

The guard for assoc-string-equal requires that x is a string and alist
is an alist.

To see the ACL2 definition of this function, see PF.

ATOM    recognizer for atoms

(atom x) is true if and only if x is an atom, i.e., not a cons pair.

Atom has a guard of t, and is a Common Lisp function.  See any Common
Lisp documentation for more information.

To see the ACL2 definition of this function, see PF.

ATOM-LISTP    recognizer for a true list of atoms

The predicate atom-listp tests whether its argument is a true-listp of
atoms, i.e., of non-conses.

Also see GOOD-ATOM-LISTP.

To see the ACL2 definition of this function, see PF.

BINARY-*    multiplication function

Completion Axiom (completion-of-*):

     (equal (binary-* x y)
            (if (acl2-numberp x)
                (if (acl2-numberp y)
                    (binary-* x y)
                  0)
              0))

Guard for (binary-* x y):

     (and (acl2-numberp x) (acl2-numberp y))

Notice that like all arithmetic functions, binary-* treats non-numeric
inputs as 0.

Calls of the macro * expand to calls of binary-*; see *.

BINARY-+    addition function

Completion Axiom (completion-of-+):

     (equal (binary-+ x y)
            (if (acl2-numberp x)
                (if (acl2-numberp y)
                    (binary-+ x y)
                  x)
              (if (acl2-numberp y)
                  y
                0)))

Guard for (binary-+ x y):

     (and (acl2-numberp x) (acl2-numberp y))

Notice that like all arithmetic functions, binary-+ treats non-numeric
inputs as 0.

Calls of the macro + expand to calls of binary-+; see +.

BINARY-APPEND    concatenate two lists

This binary function implements append, which is a macro in ACL2.  See
APPEND

The guard for binary-append requires the first argument to be a
true-listp.

To see the ACL2 definition of this function, see PF.

BOOLE$    perform a bit-wise logical operation on 2 two's complement integers

When integers x and y are viewed in their two's complement
representation, (boole$ op x y) returns the result of applying the
bit-wise logical operation specified by op.  The following table is
adapted from documentation for analogous Common Lisp function boole in
the Common Lisp HyperSpec
(`http://www.lisp.org/HyperSpec/Body/fun_boole.html#boole').  Note that
the values of op for boole$ are ACL2 constants, rather than
corresponding values of op for the Common Lisp function boole.

     op               result
     -----------      ---------
     *boole-1*        x
     *boole-2*        y
     *boole-andc1*    and complement of x with y
     *boole-andc2*    and x with complement of y
     *boole-and*      and
     *boole-c1*       complement of x
     *boole-c2*       complement of y
     *boole-clr*      the constant 0 (all zero bits)
     *boole-eqv*      equivalence (exclusive nor)
     *boole-ior*      inclusive or
     *boole-nand*     not-and
     *boole-nor*      not-or
     *boole-orc1*     or complement of x with y
     *boole-orc2*     or x with complement of y
     *boole-set*      the constant -1 (all one bits)
     *boole-xor*      exclusive or

The guard of boole$ specifies that op is the value of one of the
constants above and that x and y are integers.

See any Common Lisp documentation for analogous information about
Common Lisp function boole.

To see the ACL2 definition of this function, see PF.

BOOLEANP    recognizer for booleans

(Booleanp x) is t if x is t or nil, and is nil otherwise.

See GENERALIZED-BOOLEANS for a discussion of a potential
soundness problem for ACL2 related to the question:  Which Common Lisp
functions are known to return Boolean values?

To see the ACL2 definition of this function, see PF.

BREAK$    cause an immediate Lisp break

ACL2 users are generally advised to avoid breaking into raw Lisp.
Advanced users may, on occasion, see the need to do so.  Evaluating
(break$) will have that effect.  (Exception: break$ is disabled after
evaluation of (set-debugger-enable :never); see
SET-DEBUGGER-ENABLE.)

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.

BUTLAST    all but a final segment of a list

(Butlast l n) is the list obtained by removing the last n elements from
the true list l.  The following is a theorem (though it takes some
effort, including lemmas, to get ACL2 to prove it).

     (implies (and (integerp n)
                   (<= 0 n)
                   (true-listp l))
              (equal (length (butlast l n))
                     (if (< n (length l))
                         (- (length l) n)
                       0)))

For related functions, see TAKE and see NTHCDR.

The guard for (butlast l n) requires that n is a nonnegative integer
and lst is a true list.

Butlast is a Common Lisp function.  See any Common Lisp documentation
for more information.  Note:  In Common Lisp the second argument of
butlast is optional, but in ACL2 it is required.

To see the ACL2 definition of this function, see PF.

CAAAAR    car of the caaar

See any Common Lisp documentation for details.

CAAADR    car of the caadr

See any Common Lisp documentation for details.

CAAAR    car of the caar

See any Common Lisp documentation for details.

CAADAR    car of the cadar

See any Common Lisp documentation for details.

CAADDR    car of the caddr

See any Common Lisp documentation for details.

CAADR    car of the cadr

See any Common Lisp documentation for details.

CAAR    car of the car

See any Common Lisp documentation for details.

CADAAR    car of the cdaar

See any Common Lisp documentation for details.

CADADR    car of the cdadr

See any Common Lisp documentation for details.

CADAR    car of the cdar

See any Common Lisp documentation for details.

CADDAR    car of the cddar

See any Common Lisp documentation for details.

CADDDR    car of the cdddr

See any Common Lisp documentation for details.

CADDR    car of the cddr

See any Common Lisp documentation for details.

CADR    car of the cdr

See any Common Lisp documentation for details.

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.

CAR    returns the first element of a non-empty list, else nil

Completion Axiom (completion-of-car):

     (equal (car x)
            (cond
             ((consp x)
              (car x))
             (t nil)))

Guard:

     (or (consp x) (equal x nil))

Notice that in the ACL2 logic, car returns nil for every atom.

CASE    conditional based on if-then-else using eql

     Example Form:
     (case typ
       ((:character foo)
        (open file-name :direction :output))
       (bar (open-for-bar file-name))
       (otherwise
        (my-error "Illegal.")))

is the same as

     (cond ((member typ '(:character foo))
            (open file-name :direction :output))
           ((eql typ 'bar)
            (open-for-bar file-name))
           (t (my-error "Illegal.")))

which in turn is the same as

     (if (member typ '(:character foo))
         (open file-name :direction :output)
         (if (eql typ 'bar)
             (open-for-bar file-name)
             (my-error "Illegal.")))

Notice the quotations that appear in the example above: '(:character
foo) and 'bar.

     General Forms:
     (case expr
       (x1 val-1)
       ...
       (xk val-k)
       (otherwise val-k+1))

     (case expr
       (x1 val-1)
       ...
       (xk val-k)
       (t val-k+1))

     (case expr
       (x1 val-1)
       ...
       (xk val-k))

where each xi is either eqlablep or a true list of eqlablep objects.
The final otherwise or t case is optional.

Case is defined in Common Lisp.  See any Common Lisp documentation for
more information.

CASE-MATCH    pattern matching or destructuring

     General Form:
     (case-match x
       (pat1 dcl1 body1)
       ...
       (patk dclk bodyk))

where x is a variable symbol, the pati are structural patterns as
described below, the dcli are optional declare forms and the bodyi are
terms.  Return the value(s) of the bodyi corresponding to the first
pati matching x, or nil if none matches.

Pattern Language:
With the few special exceptions described below, matching requires that
the cons structure of x be isomorphic to that of the pattern, down to
the atoms in the pattern.  Non-symbol atoms in the pattern match only
themselves.  Symbols in the pattern denote variables which match
anything and which are bound by a successful match to the corresponding
substructure of x.  Variables that occur more than once must match the
same (EQUAL) structure in every occurrence.

     Exceptions:
     &               Matches anything and is not bound.  Repeated
                       occurrences of & in a pattern may match different
                       structures.
     nil, t, *sym*   These symbols cannot be bound and match only their
                       global values.
     !sym            where sym is a symbol that is already bound in the
                       context of the case-match, matches only the
                       current binding of sym.
     'obj            Matches only itself.

Some examples are shown below.

Below we show some sample patterns and examples of things they match
and do not match.

     pattern       matches         non-matches
     (x y y)       (ABC 3 3)       (ABC 3 4)    ; 3 is not 4
     (fn x . rst)  (P (A I) B C)   (ABC)        ; NIL is not (x . rst)
                   (J (A I))                    ; rst matches nil
     ('fn (g x) 3) (FN (H 4) 3)    (GN (G X) 3) ; 'fn matches only itself
     (& t & !x)    ((A) T (B) (C))              ; provided x is '(C)

Consider the two binary trees that contain three leaves.  They might be
described as (x . (y . z)) and ((x . y) . z), where x, y, and z are
atomic.  Suppose we wished to recognize those trees.  The following
case-match would do:

     (case-match tree
       ((x . (y . z))
        (and (atom x) (atom y) (atom z)))
       (((x . y) . z)
        (and (atom x) (atom y) (atom z))))

Suppose we wished to recognize such trees where all three tips are
identical.  Suppose further we wish to return the tip if the tree is
one of those recognized ones and to return the number 7 otherwise.

     (case-match tree
       ((x . (x . x))
        (if (atom x) x 7))
       (((x . x) . x)
        (if (atom x) x 7))
       (& 7))

Note that case-match returns nil if no pati matches.  Thus if we must
return 7 in that case, we have to add as the final pattern the &, which
always matches anything.

CDAAAR    cdr of the caaar

See any Common Lisp documentation for details.

CDAADR    cdr of the caadr

See any Common Lisp documentation for details.

CDAAR    cdr of the caar

See any Common Lisp documentation for details.

CDADAR    cdr of the cadar

See any Common Lisp documentation for details.

CDADDR    cdr of the caddr

See any Common Lisp documentation for details.

CDADR    cdr of the cadr

See any Common Lisp documentation for details.

CDAR    cdr of the car

See any Common Lisp documentation for details.

CDDAAR    cdr of the cdaar

See any Common Lisp documentation for details.

CDDADR    cdr of the cdadr

See any Common Lisp documentation for details.

CDDAR    cdr of the cdar

See any Common Lisp documentation for details.

CDDDAR    cdr of the cddar

See any Common Lisp documentation for details.

CDDDDR    cdr of the cdddr

See any Common Lisp documentation for details.

CDDDR    cdr of the cddr

See any Common Lisp documentation for details.

CDDR    cdr of the cdr

See any Common Lisp documentation for details.

CDR    returns the second element of a cons pair, else nil

Completion Axiom (completion-of-cdr):

     (equal (cdr x)
            (cond
             ((consp x)
              (cdr x))
             (t nil)))

Guard:

     (or (consp x) (equal x nil))

Notice that in the ACL2 logic, cdr returns nil for every atom.

CEILING    division returning an integer by truncating toward positive infinity

     Example Forms:
     ACL2 !>(ceiling 14 3)
     5
     ACL2 !>(ceiling -14 3)
     -4
     ACL2 !>(ceiling 14 -3)
     -4
     ACL2 !>(ceiling -14 -3)
     5
     ACL2 !>(ceiling -15 -3)
     5

(Ceiling i j) is the result of taking the quotient of i and j and
returning the smallest integer that is at least as great as that
quotient.  For example, the quotient of -14 by 3 is -4 2/3, and the
smallest integer at least that great is -4.

The guard for (ceiling i j) requires that i and j are rational (real,
in ACL2(r)) numbers and j is non-zero.

Ceiling is a Common Lisp function.  See any Common Lisp documentation
for more information.  However, note that unlike Common Lisp, the ACL2
ceiling function returns only a single value,

To see the ACL2 definition of this function, see PF.

CHAR    the nth element (zero-based) of a string

(Char s n) is the nth element of s, zero-based.  If n is greater than
or equal to the length of s, then char returns nil.

(Char s n) has a guard that n is a non-negative integer and s is a
stringp.

Char is a Common Lisp function.  See any Common Lisp documentation for
more information.

To see the ACL2 definition of this function, see PF.

CHAR-CODE    the numeric code for a given character

Completion Axiom (completion-of-char-code):

     (equal (char-code x)
            (if (characterp x)
                (char-code x)
              0))

Guard for (char-code x):

     (characterp x)

This function maps all non-characters to 0.

CHAR-DOWNCASE    turn upper-case characters into lower-case characters

(Char-downcase x) is equal to #a when x is #A, #b when x is #B, ...,
and #z when x is #Z, and is x for any other character.

The guard for char-downcase requires its argument to be a standard
character (see STANDARD-CHAR-P).

Char-downcase is a Common Lisp function.  See any Common Lisp
documentation for more information.

To see the ACL2 definition of this function, see PF.

CHAR-EQUAL    character equality without regard to case

For characters x and y, (char-equal x y) is true if and only if x and y
are the same except perhaps for their case.

The guard on char-equal requires that its arguments are both standard
characters (see STANDARD-CHAR-P).

Char-equal is a Common Lisp function.  See any Common Lisp
documentation for more information.

To see the ACL2 definition of this function, see PF.

CHAR-UPCASE    turn lower-case characters into upper-case characters

(Char-upcase x) is equal to #A when x is #a, #B when x is #b, ..., and
#Z when x is #z, and is x for any other character.

The guard for char-upcase requires its argument to be a standard
character (see STANDARD-CHAR-P).

Char-upcase is a Common Lisp function.  See any Common Lisp
documentation for more information.

To see the ACL2 definition of this function, see PF.

CHAR<    less-than test for characters

(char< x y) is true if and only if the character code of x is less than
that of y.  See CHAR-CODE.

The guard for char< specifies that its arguments are characters.

Char< is a Common Lisp function.  See any Common Lisp documentation for
more information.

To see the ACL2 definition of this function, see PF.

CHAR<=    less-than-or-equal test for characters

(char<= x y) is true if and only if the character code of x is less
than or equal to that of y.  See CHAR-CODE.

The guard for char<= specifies that its arguments are characters.

Char<= is a Common Lisp function.  See any Common Lisp documentation
for more information.

To see the ACL2 definition of this function, see PF.

CHAR>    greater-than test for characters

(char> x y) is true if and only if the character code of x is greater
than that of y.  See CHAR-CODE.

The guard for char> specifies that its arguments are characters.

Char> is a Common Lisp function.  See any Common Lisp documentation for
more information.

To see the ACL2 definition of this function, see PF.

CHAR>=    greater-than-or-equal test for characters

(char>= x y) is true if and only if the character code of x is greater
than or equal to that of y.  See CHAR-CODE.

The guard for char>= specifies that its arguments are characters.

Char>= is a Common Lisp function.  See any Common Lisp documentation
for more information.

To see the ACL2 definition of this function, see PF.

CHARACTER-ALISTP    recognizer for association lists with characters as keys

(Character-alistp x) is true if and only if x is a list of pairs of the
form (cons key val) where key is a characterp.

CHARACTER-LISTP    recognizer for a true list of characters

The predicate character-listp tests whether its argument is a true list
of characters.

To see the ACL2 definition of this function, see PF.

CHARACTERP    recognizer for characters

(characterp x) is true if and only if x is a character.