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.

QUANTIFIER-TUTORIAL    A Beginner's Guide to Reasoning about Quantification in ACL2

The initial version of this tutorial was written by Sandip Ray.
Additions and revisions are welcome.  Sandip has said:

     "This is a collection of notes that I wrote to remind myself of
     how to reason about quantifiers when I just started.  Most users
     after they have gotten the hang of quantifiers probably will not
     need this and will be able to use their intuitions to guide them
     in the process.  But since many ACL2 users are not used to
     quantification, I am hoping that this set of notes might help them
     to think clearly while reasoning about quantifiers in ACL2."

Many ACL2 papers start with the sentence "ACL2 is a quantifier-free
first-order logic of recursive functions."  It is true that the _syntax_
of ACL2 is quantifier-free; every formula is assumed to be universally
quantified over all free variables in the formula.  But the _logic_ in
fact does afford arbitrary first-order quantification.  This is
obtained in ACL2 using a construct called defun-sk.  See
DEFUN-SK.

Many ACL2 users do not think in terms of quantifiers.  The focus is
almost always on defining recursive functions and reasoning about them
using induction.  That is entirely justified, in fact, since proving
theorems about recursive functions by induction plays to the strengths
of the theorem prover.  Nevertheless there are situations where it is
reasonable and often useful to think in terms of quantifiers.  However,
reasoning about quantifiers requires that you get into the mindset of
thinking about theorems in terms of quantification.  This note is about
how to do this effectively given ACL2's implementation of
quantification.  This does not discuss defun-sk in detail, but merely
shows some examples.  A detailed explanation of the implementation is
in the ACL2 documentation (see DEFUN-SK); also see
CONSERVATIVITY-OF-DEFCHOOSE.

[Note: Quantifiers can be used for some pretty cool things in ACL2.
Perhaps the most interesting example is the way of using quantifiers to
introduce arbitrary tail-recursive equations; see the paper "Partial
Functions in ACL2" by Panagiotis Manolios and J Strother Moore.  This
note does not address applications of quantifiers, but merely how you
would reason about them once you think you want to use them.]

Assume that you have some function P.  I have just left P as a unary
function stub below, since I do not care about what P is.

     (defstub P (*) => *)

Now suppose you want to specify the concept that "there exists some x
such that (P x) holds".  ACL2 allows you to write that directly using
quantifiers.

     (defun-sk exists-P () (exists x (P x)))

If you submit the above form in ACL2 you will see that the theorem
prover specifies two functions exists-p and exists-p-witness, and
exports the following constraints:

     1.  (defun exists-P () (P (exists-P-witness)))
     2.  (defthm exists-P-suff (implies (p x) (exists-p)))

Here exists-P-witness is a new function symbol in the current ACL2
theory.  What do the constraints above say?  Notice the constraint
exists-p-suff.  It says that if you can provide any x such that (P x)
holds, then you know that exists-p holds.  Think of the other
constraint (definition of exists-p) as going the other way.  That is, it
says that if exists-p holds, then there is some x, call it
(exists-p-witness), for which P holds.  Notice that nothing else is
known about exists-p-witness than the two constraints above.

[Note: exists-p-witness above is actually defined in ACL2 using a
special form called defchoose.  See DEFCHOOSE.  This note does
not talk about defchoose.  So far as this note is concerned, think of
exists-p-witness as a new function symbol that has been generated
somehow in ACL2, about which nothing other than the two facts above is
known.]

Similarly, you can talk about the concept that "for all x (P x) holds."
This can be specified in ACL2 by the form:

     (defun-sk forall-P () (forall x (P x)))

This produces the following two constraints:

     1.  (defun forall-P () (P (forall-p-witness)))
     2.  (defthm forall-p-necc (implies (not (P x)) (not (forall-p))))

To understand these, think of for-all-p-witness as producing some x
which does not satisfy P, if such a thing exists.  The constraint
forall-p-necc merely says that if forall-p holds then P is satisfied
for every x.  (To see this more clearly, just think of the
contrapositive of the formula shown.) The other constraint (definition
of forall-p) implies that if forall-p does not hold then there is some
x, call it (forall-p-witness), which does not satisfy P.  To see this,
just consider the following formula which is immediately derivable from
the definition.

     (implies (not (forall-p)) (not (P (forall-witness))))

The description above suggests that to reason about quantifiers, the
following Rules of Thumb, familiar to most any student of logic, are
useful.

     RT1: To prove (exists-p), construct some object A such that P
     holds for A and then use exists-P-suff.

     RT2: If you assume exists-P in your hypothesis, use the definition
     of exists-p to know that P holds for exists-p-witness.  To use this
     to prove a theorem, you must be able to derive the theorem based
     on the hypothesis that P holds for something, whatever the
     something is.

     RT3: To prove forall-P, prove the theorem (P x) (that is, that P
     holds for an arbitrary x), and then simply instantiate the
     definition of forall-p, that is, show that P holds for the witness.

     RT4: If you assume forall-p in the hypothesis of the theorem, see
     how you can prove your conclusion if indeed you were given (P x)
     as a theorem.  Possibly for the conclusion to hold, you needed
     that P holds for some specific set of x values.  Then use the
     theorem forall-p-necc by instantiating it for the specific x
     values you care about.

Perhaps the above is too terse.  In the remainder of the note, we will
consider several examples of how this is done to prove theorems in ACL2
that involve quantified notions.

Let us consider two trivial theorems.  Assume that for some unary
function r, you have proved (r x) as a theorem.  Let us see how you can
prove that (1) there exists some x such that (r x) holds, and (2) for
all x (r x) holds.

We first model these things using defun-sk.  Below, r is simply some
function for which (r x) is a theorem.

     (encapsulate
      (((r *) => *))
      (local (defun r (x) (declare (ignore x)) t))
      (defthm r-holds (r x)))

     (defun-sk exists-r () (exists x (r x)))
     (defun-sk forall-r () (forall x (r x)))

ACL2 does not have too much reasoning support for quantifiers.  So in
most cases, one would need :use hints to reason about quantifiers.  In
order to apply :use hints, it is preferable to keep the function
definitions and theorems disabled.

     (in-theory (disable exists-r exists-r-suff forall-r forall-r-necc))

Let us now prove that there is some x such that (r x) holds.  Since we
want to prove exists-r, we must use exists-r-suff by RT1.  We do not
need to construct any instance here since r holds for all x by the
theorem above.

     (defthm exists-r-holds
       (exists-r)
       :hints (("Goal" :use ((:instance exists-r-suff)))))

Let us now prove the theorem that for all x, (r x) holds.  By RT3, we
must be able to prove it by definition of forall-r.

     (defthm forall-r-holds
       (forall-r)
       :hints (("Goal" :use ((:instance (:definition forall-r))))))

[Note: Probably no ACL2 user in his or her right mind would prove the
theorems exists-r-holds and forall-r-holds above.  The theorems shown
are only for demonstration purposes.]

For the remainder of this note we will assume that we have two stubbed
out unary functions M and N, and we will look at proving some quantified
properties of these functions.

     (defstub M (*) => *)
     (defstub N (*) => *)

Let us now define the predicates all-M, all-N, ex-M, and ex-N
specifying the various quantifications.

     (defun-sk all-M () (forall x (M x)))
     (defun-sk all-N () (forall x (N x)))
     (defun-sk some-M () (exists x (M x)))
     (defun-sk some-N () (exists x (N x)))

     (in-theory (disable all-M all-N all-M-necc all-N-necc))
     (in-theory (disable some-M some-N some-M-suff some-N-suff))

Let us prove the classic distributive properties of quantification: the
distributivity of universal quantification over conjunction, and the
distributivity of existential quantification over disjunction.  We can
state these properties informally in "pseudo ACL2" notation as follows:

     1.  (exists x: (M x)) or (exists x: (N x)) <=> (exists x: (M x) or (N x))
     2.  (forall x: (M x)) and (forall: x (N x)) <=> (forall x: (M x) and (N x))

To make these notions formal we of course need to define the formulas
at the right-hand sides of 1 and 2.  So we define some-MN and all-MN to
capture these concepts.

     (defun-sk some-MN () (exists x (or (M x) (N x))))
     (defun-sk all-MN () (forall x (and (M x) (N x))))

     (in-theory (disable all-MN all-MN-necc some-MN some-MN-suff))

First consider proving property 1.  The formal statement of this
theorem would be: (iff (some-MN) (or (some-M) (some-N))).

How do we prove this theorem?  Looking at RT1-RT4 above, note that they
suggest how one should reason about quantification when one has an
"implication".  But here we have an "equivalence".  This suggests
another rule of thumb.

     RT5: Whenever possible, prove an equivalence involving quantifiers
     by proving two implications.

Let us apply RT5 to prove the theorems above.  So we will first prove:
(implies (some-MN) (or (some-M) (some-N)))

How can we prove this?  This involves assuming a quantified predicate
(some-MN), so we must use RT2 and apply the definition of some-MN.
Since the conclusion involves a disjunction of two quantified
predicates, by RT1 we must be able to construct two objects A and B
such that either M holds for A or N holds for B, so that we can then
invoke some-M-suff and some-N-suff to prove the conclusion.  But now
notice that if some-MN is true, then there is already an object, in fact
some-MN-witness, such that either M holds for it, or N holds for it.
And we know this is the case from the definition of some-MN! So we will
simply prove the theorem instantiating some-M-suff and some-N-suff with
this witness.  The conclusion is that the following event will go
through with ACL2.

     (defthm le1
       (implies (some-MN)
                (or (some-M) (some-N)))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-MN))
                       (:instance some-M-suff
                                  (x (some-MN-witness)))
                       (:instance some-N-suff
                                  (x (some-MN-witness)))))))

This also suggests the following rule of thumb:

     RT6: If a conjecture involves assuming an existentially quantified
     predicate in the hypothesis from which you are trying to prove an
     existentially quantified predicate, use the witness of the
     existential quantification in the hypothesis to construct the
     witness for the existential quantification in the conclusion.

Let us now try to prove the converse of le1, that is: (implies (or
(some-M) (some-N)) (some-MN))

Since the hypothesis is a disjunction, we will just prove each case
individually instead of proving the theorem by a :cases hint.  So we
prove the following two lemmas.

     (defthm le2
       (implies (some-M) (some-MN))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-M))
                       (:instance some-MN-suff
                                  (x (some-M-witness)))))))

     (defthm le3
       (implies (some-N) (some-MN))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-N))
                       (:instance some-MN-suff
                                  (x (some-N-witness)))))))

Note that the hints above are simply applications of RT6 as in le1.
With these lemmas, of course the main theorem is trivial.

     (defthmd |some disjunction|
       (iff (some-MN) (or (some-M) (some-N)))
       :hints (("Goal"
                 :use ((:instance le1)
                       (:instance le2)
                       (:instance le3)))))

Let us now prove the distributivity of universal quantification over
conjunction, that is, the formula: (iff (all-MN) (and (all-M) (all-N)))

Applying RT5, we will again decompose this into two implications.  So
consider first the one-way implication: (implies (and (all-M) (all-N))
(all-MN)).

Here we get to assume all-M and all-N.  Thus by RT4 we can use
all-M-necc and all-N-necc to think as if we are given the formulas (M
x) and (N x) as theorems.  The conclusion here is also a universal
quantification, namely we have to prove all-MN.  Then RT3 tells us to
proceed as follows.  Take any object y.  Try to find an instantiation z
of the hypothesis that implies (and (M y) (N y)).  Then instantiate y
with all-MN-witness.  Note that the hypothesis lets us assume (M x) and
(N x) to be theorems.  Thus to justify we need to instantiate x with y,
and in this case, therefore, with all-MN-witness.  To make the long
story short, the following event goes through with ACL2:

     (defthm lf1
        (implies (and (all-M) (all-N))
                 (all-MN))
         :rule-classes nil
         :hints (("Goal"
                   :use ((:instance (:definition all-MN))
                         (:instance all-M-necc (x (all-MN-witness)))
                         (:instance all-N-necc (x (all-MN-witness)))))))

This suggests the following rule of thumb which is a dual of RT6:

     RT7: If a conjecture assumes some universally quantified predicate
     in the hypothesis and its conclusion asserts a universallly
     quantified predicate, then instantiate the "necessary condition"
     (forall-mn-necc) of the hypothesis with the witness of the
     conclusion to prove the conjecture.

Applying RT7 now we can easily prove the other theorems that we need to
show that universal quantification distributes over conjunction.  Let
us just go through this motion in ACL2.

     (defthm lf2
       (implies (all-MN)
                (all-M))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition all-M))
                       (:instance all-MN-necc
                                  (x (all-M-witness)))))))

     (defthm lf3
       (implies (all-MN)
                (all-N))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition all-N))
                       (:instance all-MN-necc
                                  (x (all-N-witness)))))))

     (defthmd |all conjunction|
       (iff (all-MN)
            (and (all-M) (all-N)))
      :hints (("Goal" :use ((:instance lf1)
                            (:instance lf2)
                            (:instance lf3)))))

The rules of thumb for universal and existential quantification should
make you realize the duality of their use.  Every reasoning method
about universal quantification can be cast as a way of reasoning about
existential quantification, and vice versa.  Whether you reason using
universal and existential quantifiers depends on what is natural in a
particular context.  But just for the sake of completeness let us prove
the duality of universal and existential quantifiers.  So what we want
to prove is the following:

     3.  (forall x (not (M x))) = (not (exists x (M x)))

We first formalize the notion of (forall x (not (M x))) as a
quantification.

     (defun-sk none-M () (forall x (not (M x))))
     (in-theory (disable none-M none-M-necc))

So we now want to prove: (equal (none-M) (not (some-M))).

As before, we should prove this as a pair of implications.  So let us
prove first: (implies (none-M) (not (some-M))).

This may seem to assert an existential quantification in the
conclusion, but rather, it asserts the _negation_ of an existential
quantification.  We are now trying to prove that something does not
exist.  How do we do that?  We can show that nothing satisfies M by
just showing that (some-M-witness) does not satisfy M.  This suggests
the following rule of thumb:

     RT8: When you encounter the negation of an existential
     quantification think in terms of a universal quantification, and
     vice-versa.

Ok, so now applying RT8 and RT3 you should be trying to apply the
definition of some-M.  The hypothesis is just a pure (non-negated)
universal quantification so you should apply RT4.  A blind application
lets us prove the theorem as below.

     (defthm nl1
       (implies (none-M) (not (some-M)))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-M))
                       (:instance none-M-necc (x (some-M-witness)))))))

How about the converse implication?  I have deliberately written it as
(implies (not (none-M)) (some-M)) instead of switching the left-hand and
right-hand sides of nl1, which would have been equivalent.  Again, RH8
tells us how to reason about it, in this case using RH2, and we succeed.

     (defthm nl2
       (implies (not (none-M)) (some-M))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition none-M))
                       (:instance some-M-suff (x (none-M-witness)))))))

So finally we just go through the motions of proving the equality.

     (defthmd |forall not = not exists|
       (equal (none-M) (not (some-M)))
       :hints (("Goal"
                 :use ((:instance nl1)
                       (:instance nl2)))))

Let us now see if we can prove a slightly more advanced theorem which
can be stated informally as: If there is a natural number x which
satisfies M, then there is a least natural number y that satisfies M.

[Note: Any time I have had to reason about existential quantification I
have had to do this particular style of reasoning and state that if
there is an object satisfying a predicate, then there is also a
"minimal" object satisfying the predicate.]

Let us formalize this concept.  We first define the concept of
existence of a natural number satisfying x.

     (defun-sk some-nat-M () (exists x (and (natp x) (M x))))
     (in-theory (disable some-nat-M some-nat-M-suff))

We now talk about what it means to say that x is the least number
satisfying M.

     (defun-sk none-below (y)
       (forall r (implies (and (natp r) (< r y)) (not (M r))))))
     (in-theory (disable none-below none-below-necc))

     (defun-sk min-M () (exists y (and (M y) (natp y) (none-below y))))
     (in-theory (disable min-M min-M-suff))

The predicate none-below says that no natural number less than y
satisfies M.  The predicate min-M says that there is some natural
number y satisfying M such that none-below holds for y.

So the formula we want to prove is: (implies (some-nat-M) (min-M)).

Since the formula requires that we prove an existential quantification,
RT1 tells us to construct some object satisfying the predicate over
which we are quantifying.  We should then be able to instantiate
min-M-suff with this object.  That predicate says that the object must
be the least natural number that satisfies M.  Since such an object is
uniquely computable if we know that there exists some natural number
satisfying M, let us just write a recursive function to compute it.
This function is least-M below.

     (defun least-M-aux (i bound)
       (declare (xargs :measure (nfix (- (1+ bound) i))))
       (cond ((or (not (natp i))
                  (not (natp bound))
                  (> i bound))
              0)
            ((M i) i)
            (t (least-M-aux (+ i 1) bound))))

     (defun least-M (bound) (least-M-aux 0 bound))

Let us now reason about this function as one does typically.  So we
prove that this object is indeed the least natural number that
satisfies M, assuming that bound is a natural number that satisfies M.

     (defthm least-aux-produces-an-M
       (implies (and (natp i)
                     (natp bound)
                     (<= i bound)
                     (M bound))
                (M (least-M-aux i bound))))

     (defthm least-<=bound
       (implies (<= 0 bound)
                (<= (least-M-aux i bound) bound)))

     (defthm least-aux-produces-least
       (implies (and (natp i)
                     (natp j)
                     (natp bound)
                     (<= i j)
                     (<= j bound)
                     (M j))
                 (<= (least-M-aux i bound) j)))

     (defthm least-aux-produces-natp
       (natp (least-M-aux i bound)))

     (defthmd least-is-minimal-satisfying-m
       (implies (and (natp bound)
                     (natp i)
                      (< i (least-M bound)))
                (not (M i)))
       :hints (("Goal"
                 :in-theory (disable least-aux-produces-least least-<=bound)
                 :use ((:instance least-<=bound
                                  (i 0))
                       (:instance least-aux-produces-least
                                  (i 0)
                                  (j i))))))

     (defthm least-has-m
       (implies (and (natp bound)
                     (m bound))
                (M (least-M bound))))

     (defthm least-is-natp
       (natp (least-M bound)))

So we have done that, and hopefully this is all that we need about
least-M.  So we disable everything.

     (in-theory (disable least-M natp))

Now of course we note that the statement of the conjecture we are
interested in has two quantifiers, an inner forall (from none-below)
and an outer exists (from min-M).  Since ACL2 is not very good with
quantification, we hold its hands to reason with the quantifier part.
So we will first prove something about the forall and then use it to
prove what we need about the exists.

     RT9: When you face nested quantifiers, reason about each nesting
     separately.

So what do we want to prove about the inner quantifier?  Looking
carefully at the definition of none-below we see that it is saying that
for all natural numbers r < y, (M r) does not hold.  Well, how would we
want to use this fact when we want to prove our final theorem?  We
expect that we will instantiate min-M-suff with the object (least-M
bound) where we know (via the outermost existential quantifier) that M
holds for bound, and we will then want to show that none-below holds for
(least-M bound).  So let us prove that for any natural number (call it
bound), none-below holds for (least-M bound).  For the final theorem we
only need it for natural numbers satisfying M, but note that from the
lemma least-is-minimal-satisfying-m we really do not need that bound
satisfies M.

So we are now proving: (implies (natp bound) (none-below (least-M
bound))).

Well since this is a standard case of proving a universally quantified
predicate, we just apply RT3.  We have proved that for all naturals i <
(least-M bound), i does not satisfy M (lemma
least-is-minimal-satisfying-M), so we merely need the instantiation of
that lemma with none-below-witness of the thing we are trying to prove,
that is, (least-M bound).  The theorem below thus goes through.

     (defthm least-is-minimal
       (implies (natp bound)
                (none-below (least-M bound)))
       :hints (("Goal"
                 :use ((:instance (:definition none-below)
                                  (y (least-M bound)))
                       (:instance least-is-minimal-satisfying-m
                                  (i (none-below-witness (least-M bound))))))))

Finally we are in the outermost existential quantifier, and are in the
process of applying min-M-suff.  What object should we instantiate it
with?  We must instantiate it with (least-M bound) where bound is an
object which must satisfy M and is a natural.  We have such an object,
namely (some-nat-M-witness) which we know have all these qualities given
the hypothesis.  So the proof now is just RT1 and RT2.

     (defthm |minimal exists|
       (implies (some-nat-M) (min-M))
       :hints (("Goal"
                 :use ((:instance min-M-suff
                                  (y (least-M (some-nat-M-witness))))
                       (:instance (:definition some-nat-M))))))

If you are comfortable with the reasoning above, then you are
comfortable with quantifiers and probably will not need these notes any
more.  In my opinion, the best way of dealing with ACL2 is to ask
yourself why you think something is a theorem, and the rules of thumb
above are simply guides to the questions that you need to ask when you
are dealing with quantification.

Here are a couple of simple exercises for you to test if you understand
the reasoning process.

*Exercise 1*.  Formalize and prove the following theorem.  Suppose there
exists x such that (R x) and suppose that all x satisfy (P x).  Then
prove that there exists x such that (P x) & (R x).  (See
`http://www.cs.utexas.edu/users/moore/acl2/contrib/quantifier-exercise-1-solution.html'
for a solution.)

*Exercise 2*.  Recall the example just before the preceding exercise,
where we showed that if there exists a natural number x satisfying M
then there is another natural number y such that y satisfies M and for
every natural number z < y, z does not.  What would happen if we remove
the restriction of x, y, and z being naturals?  Of course, we will not
talk about < any more, but suppose you use the total order on all ACL2
objects (from "books/misc/total-order").  More concretely, consider the
definition of some-M above.  Let us now define two other functions:

     (include-book "misc/total-order" :dir :system)

     (defun-sk none-below-2 (y)
       (forall r (implies (<< r y) (not (M r)))))

     (defun-sk min-M2 () (exists y (and (M y) (none-below-2 y))))

The question is whether (implies (some-M) (min-M2)) is a theorem.  Can
you prove it?  Can you disprove it?

QUANTIFIERS    issues about quantification in ACL2

ACL2 supports first-order quantifiers exists and forall by way of the
defun-sk event.  However, proof support for quantification is quite
limited.  Therefore, you may prefer using recursion in place of defun-sk
when possible (following common ACL2 practice).

For example, the notion "every member of x has property p" can be
defined either with recursion or explicit quantification, but proofs
may be simpler when recursion is used.  We illustrate this point with
two proofs of the same informal claim, one of which uses recursion
which the other uses explicit quantification.  Notice that with
recursion, the proof goes through fully automatically; but this is far
from true with explicit quantification (especially notable is the ugly
hint).

The informal claim for our examples is:  If every member a of each of
two lists satisfies the predicate (p a), then this holds of their
append; and, conversely.

See QUANTIFIERS-USING-RECURSION for a solution to this example
using recursion.

See QUANTIFIERS-USING-DEFUN-SK for a solution to this example
using defun-sk.  Also See QUANTIFIERS-USING-DEFUN-SK-EXTENDED
for an elaboration on that solution.

But perhaps first, see DEFUN-SK for an ACL2 utility to
introduce first-order quantification in a direct way.  Examples of the
use of defun-sk are also available: see DEFUN-SK-EXAMPLE and
see TUTORIAL4-DEFUN-SK-EXAMPLE for basic examples, and see
QUANTIFIER-TUTORIAL for a more complete, careful beginner's
introduction that takes you through typical kinds of quantifier-based
reasoning in ACL2.

QUANTIFIERS-USING-DEFUN-SK    quantification example

See QUANTIFIERS for the context of this example.  It should be
compared to a corresponding example in which a simpler proof is
attained by using recursion in place of explicit quantification; see
QUANTIFIERS-USING-RECURSION.

     (in-package "ACL2")

     ; We prove that if every member A of each of two lists satisfies the
     ; predicate (P A), then this holds of their append; and, conversely.

     ; Here is a solution using explicit quantification.

     (defstub p (x) t)

     (defun-sk forall-p (x)
       (forall a (implies (member a x)
                          (p a))))

     (defthm member-append
       (iff (member a (append x1 x2))
            (or (member a x1) (member a x2))))

     (defthm forall-p-append
       (equal (forall-p (append x1 x2))
              (and (forall-p x1) (forall-p x2)))
       :hints (("Goal" ; ``should'' disable forall-p-necc, but no need
                :use
                ((:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x1)))
                 (:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x2)))
                 (:instance forall-p-necc
                            (x x1)
                            (a (forall-p-witness (append x1 x2))))
                 (:instance forall-p-necc
                            (x x2)
                            (a (forall-p-witness (append x1 x2))))))))

Also see QUANTIFIERS-USING-DEFUN-SK-EXTENDED for an elaboration
on this example.

QUANTIFIERS-USING-DEFUN-SK-EXTENDED    quantification example with details

See QUANTIFIERS-USING-DEFUN-SK for the context of this example.

     (in-package "ACL2")

     ; We prove that if every member A of each of two lists satisfies the
     ; predicate (P A), then this holds of their append; and, conversely.

     ; Here is a solution using explicit quantification.

     (defstub p (x) t)

     (defun-sk forall-p (x)
       (forall a (implies (member a x)
                          (p a))))

     ; The defun-sk above introduces the following axioms.  The idea is that
     ; (FORALL-P-WITNESS X) picks a counterexample to (forall-p x) if there is one.

     ;   (DEFUN FORALL-P (X)
     ;     (LET ((A (FORALL-P-WITNESS X)))
     ;          (IMPLIES (MEMBER A X) (P A))))
     ;
     ;   (DEFTHM FORALL-P-NECC
     ;     (IMPLIES (NOT (IMPLIES (MEMBER A X) (P A)))
     ;              (NOT (FORALL-P X)))
     ;     :HINTS (("Goal" :USE FORALL-P-WITNESS)))

     ; The following lemma seems critical.

     (defthm member-append
       (iff (member a (append x1 x2))
            (or (member a x1) (member a x2))))

     ; The proof of forall-p-append seems to go out to lunch, so we break into
     ; directions as shown below.

     (defthm forall-p-append-forward
       (implies (forall-p (append x1 x2))
                (and (forall-p x1) (forall-p x2)))
       :hints (("Goal" ; ``should'' disable forall-p-necc, but no need
                :use
                ((:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x1)))
                 (:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x2)))))))

     (defthm forall-p-append-reverse
       (implies (and (forall-p x1) (forall-p x2))
                (forall-p (append x1 x2)))
       :hints (("Goal"
                :use
                ((:instance forall-p-necc
                            (x x1)
                            (a (forall-p-witness (append x1 x2))))
                 (:instance forall-p-necc
                            (x x2)
                            (a (forall-p-witness (append x1 x2))))))))

     (defthm forall-p-append
       (equal (forall-p (append x1 x2))
              (and (forall-p x1) (forall-p x2)))
       :hints (("Goal" :use (forall-p-append-forward
                             forall-p-append-reverse))))

QUANTIFIERS-USING-RECURSION    recursion for implementing quantification

The following example illustrates the use of recursion as a means of
avoiding proof difficulties that can arise from the use of explicit
quantification (via defun-sk).  See QUANTIFIERS for more about
the context of this example.

     (in-package "ACL2")

     ; We prove that if every member A of each of two lists satisfies the
     ; predicate (P A), then this holds of their append; and, conversely.

     ; Here is a solution using recursively-defined functions.

     (defstub p (x) t)

     (defun all-p (x)
       (if (atom x)
           t
         (and (p (car x))
              (all-p (cdr x)))))

     (defthm all-p-append
       (equal (all-p (append x1 x2))
              (and (all-p x1) (all-p x2))))

DEFUND    define a function symbol and then disable it

Use defund instead of defun when you want to disable a function
immediately after its definition.  This macro has been provided for
users who prefer working in a mode where functions are only enabled
when explicitly directed by :in-theory.  Specifically, the form

     (defund NAME FORMALS ...)

expands to:

     (progn
       (defun NAME FORMALS ...)
       (with-output
        :off summary
        (in-theory (disable NAME)))
       (value-triple '(:defund NAME))).

Only the :definition rule (and, for recursively defined functions, the
:induction rule) for the function are disabled.  In particular, defund
does not disable either the :type-prescription or the
:executable-counterpart rule.  Also, the summary for the in-theory
event is suppressed.

Note that defund commands are never redundant (see
REDUNDANT-EVENTS).  If the function has already been defined, then
the in-theory event will still be executed.

See DEFUN for documentation of defun.

DEFUND-INLINE    define a potentially disabled, inlined function symbol and associated macro

Defund-inline is a variant of defun-inline, the difference being that
defund-inline disables the newly-defined function symbol.  See
DEFUN-INLINE.

DEFUND-NOTINLINE    define a disabled, not-to-be-inlined function symbol and associated macro

Defund-notinline is a variant of defun-notinline, the difference being
that defund-notinline disables the newly-defined function symbol.  See
DEFUN-NOTINLINE.

ENCAPSULATE    constrain some functions and/or hide some events

The following example illustrates the idea of encapsulate.

     (encapsulate

     ; Introduce a function foo of one argument that returns one value:
      ( ((foo *) => *) )

     ; Introduce a ``witness'' (example) for foo, marked as local so that
     ; it is not exported:
      (local (defun foo (x) x))

     ; Introduce a non-local property to be exported:
      (defthm foo-preserves-consp
        (implies (consp x)
                 (consp (foo x))))
     )

The form above introduces a new function symbol, foo, with the indicated
property and no definition.  In fact, the output from ACL2 concludes as
follows.

     The following constraint is associated with the function FOO:

     (IMPLIES (CONSP X) (CONSP (FOO X)))

We turn now to more complete documentation.

     Other Examples:
     (encapsulate (((an-element *) => *))

     ; The list of signatures above could also be written
     ;            ((an-element (lst) t))

       (local (defun an-element (lst)
                (if (consp lst) (car lst) nil)))
       (local (defthm member-equal-car
                 (implies (and lst (true-listp lst))
                          (member-equal (car lst) lst))))
       (defthm thm1
          (implies (null lst) (null (an-element lst))))
       (defthm thm2
          (implies (and (true-listp lst)
                        (not (null lst)))
                   (member-equal (an-element lst) lst))))

     (encapsulate
      () ; empty signature: no constrained functions indicated

      (local (defthm hack
               (implies (and (syntaxp (quotep x))
                             (syntaxp (quotep y)))
                        (equal (+ x y z)
                               (+ (+ x y) z)))))

      (defthm nthcdr-add1-conditional
        (implies (not (zp (1+ n)))
                 (equal (nthcdr (1+ n) x)
                        (nthcdr n (cdr x))))))

     General Form:
     (encapsulate (signature ... signature)
       ev1
       ...
       evn)

where each signature is a well-formed signature, each signature
describes a different function symbol, and each evi is an embedded event
form (See EMBEDDED-EVENT-FORM).  Also see SIGNATURE, in
particular for a discussion of how a signature can assign a guard to a
function symbol.  There must be at least one evi.  The evi inside local
special forms are called "local" events below.  Events that are not
local are sometimes said to be "exported" by the encapsulation.  We
make the further restriction that no defaxiom event may be introduced
in the scope of an encapsulate (not even by encapsulate or include-book
events that are among the evi).  Furthermore, no non-local include-book
event is permitted in the scope of any encapsulate with a non-empty
list of signatures.

To be well-formed, an encapsulate event must have the properties that
each event in the body (including the local ones) can be successfully
executed in sequence and that in the resulting theory, each function
mentioned among the signatures was introduced via a local event and has
the signature listed.  (A utility is provided to assist in debugging
failures of such execution; see REDO-FLAT.)  In addition, the
body may contain no "local incompatibilities" which, roughly stated,
means that the events that are not local must not syntactically require
symbols defined by local events, except for the functions listed in the
signatures.  See LOCAL-INCOMPATIBILITY.  Finally, no non-local
recursive definition in the body may involve in its suggested induction
scheme any function symbol listed among the signatures.  See
SUBVERSIVE-RECURSIONS.

The result of an encapsulate event is an extension of the logic in
which, roughly speaking, the functions listed in the signatures are
constrained to have the signatures listed and to satisfy the non-local
theorems proved about them.  In fact, other functions introduced in the
encapsulate event may be considered to have "constraints" as well.
(See CONSTRAINT for details, which are only relevant to
functional instantiation.)  Since the constraints were all theorems in
the "ephemeral" or "local" theory, we are assured that the extension
produced by encapsulate is sound.  In essence, the local definitions of
the constrained functions are just "witness functions" that establish
the consistency of the constraints.  Because those definitions are
local, they are not present in the theory produced by encapsulation.
Encapsulate also exports all rules generated by its non-local events,
but rules generated by local events are not exported.

The default-defun-mode for the first event in an encapsulation is the
default defun-mode "outside" the encapsulation.  But since events
changing the defun-mode are permitted within the body of an
encapsulate, the default defun-mode may be changed.  However,
defun-mode changes occurring within the body of the encapsulate are not
exported.  In particular, the acl2-defaults-table after an encapsulate
is always the same as it was before the encapsulate, even though the
encapsulate body might contain defun-mode changing events, :program and
:logic.  See DEFUN-MODE.  More generally, after execution of an
encapsulate event, the value of acl2-defaults-table is restored to what
it was immediately before that event was executed.  See
ACL2-DEFAULTS-TABLE.

Theorems about the constrained function symbols may then be proved --
theorems whose proofs necessarily employ only the constraints.  Thus,
those theorems may be later functionally instantiated, as with the
:functional-instance lemma instance (see LEMMA-INSTANCE), to
derive analogous theorems about different functions, provided the
constraints (see CONSTRAINT) can be proved about the new
functions.

We make some remarks on guards and evaluation.  Calls of functions
introduced in the signatures list cannot be evaluated in the ACL2
read-eval-print loop.  See DEFATTACH for a way to overcome this
limitation.  Moreover, any :guard supplied in the signature is
automatically associated in the world with its corresponding function
symbol, with no requirement other than that the guard is a legal term
all of whose function symbols are in :logic mode with their guards
verified.  In particular, there need not be any relationship between a
guard in a signature and the guard in a local witness function.
Finally, note that for functions introduced non-locally inside an
encapsulate event, guard verification is illegal unless ACL2 determines
that the proof obligations hold outside the encapsulate event as well.

     (encapsulate
      ((f (x) t))
      (local (defun f (x) (declare (xargs :guard t)) (consp x)))
      ;; ERROR!
      (defun g (x)
        (declare (xargs :guard (f x)))
        (car x)))

Observe that if the signatures list is empty, encapsulate may still be
useful for deriving theorems to be exported whose proofs require lemmas
you prefer to hide (i.e., made local).

The order of the events in the vicinity of an encapsulate is confusing.
We discuss it in some detail here because when logical names are being
used with theory functions to compute sets of rules, it is sometimes
important to know the order in which events were executed.  (See
LOGICAL-NAME and see THEORY-FUNCTIONS.)  What, for example,
is the set of function names extant in the middle of an encapsulation?

If the most recent event is previous and then you execute an
encapsulate constraining an-element with two non-local events in its
body, thm1 and thm2, then the order of the events after the
encapsulation is (reading chronologically forward): previous, thm1,
thm2, an-element (the encapsulate itself).  Actually, between previous
and thm1 certain extensions were made to the world by the superior
encapsulate, to permit an-element to be used as a function symbol in
thm1.

Finally, we note that an encapsulate event is redundant if and only if
a syntactically identical encapsulate has already been executed under
the same default-defun-mode, default-ruler-extenders, and
default-verify-guards-eagerness.  See REDUNDANT-EVENTS.

EVISC-TABLE    support for abbreviated output

The evisc-table is an ACL2 table (see TABLE) whose purpose is
to modify the print representations of specified non-nil objects.  When
a key (some object) is associated with a string value, then that string
is printed instead of that key (as an abbreviation).  For example, the
following log shows how to abbreviate the key (a b c) with the token
<my-abc-list>.

     ACL2 !>(table evisc-table '(a b c) "<my-abc-list>")

     Summary
     Form:  ( TABLE EVISC-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      EVISC-TABLE
     ACL2 !>'(a b c)
     <my-abc-list>
     ACL2 !>'(4 5 a b c)
     (4 5 . <my-abc-list>)
     ACL2 !>

Every value in this table must be either a string or nil, where nil
eliminates any association of the key with an abbreviation.  Continuing
with the log above:

     ACL2 !>(table evisc-table '(a b c) nil)

     Summary
     Form:  ( TABLE EVISC-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      EVISC-TABLE
     ACL2 !>'(a b c)
     (A B C)
     ACL2 !>'(4 5 a b c)
     (4 5 A B C)
     ACL2 !>

It can be particularly helpful to use this table to abbreviate a
constant introduced by defconst by prefixing the constant name with
"#,", as we now describe.  Consider first the following example.

     (defconst *abc* '(1 2 3 4 5 6 7 8))
     (table evisc-table *abc*
       (concatenate 'string "#," (symbol-name '*abc*)))

Then the constant *abc* is printed as follows -- very helpful if its
associated structure is significantly larger than the 8-element list of
numbers shown above!

     ACL2 !>*abc*
     #,*ABC*
     ACL2 !>

What's more, the ACL2 reader will replace #,*C*, where *C* is defined by
defconst, by its value, regardless of evisc-table; see
SHARP-DOT-READER.  Continuing with the example above, we have:

     ACL2 !>(cdr (quote #,*ABC*))
     (2 3 4 5 6 7 8)
     ACL2 !>

Of course, more care needs to be taken if packages are involved (see
DEFPKG), as we now illustrate.

     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 !>(defconst foo::*a* '(1 2 3))

     Summary
     Form:  ( DEFCONST FOO::*A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO::*A*
     ACL2 !>(table evisc-table foo::*a* "#,foo::*a*")

     Summary
     Form:  ( TABLE EVISC-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      EVISC-TABLE
     ACL2 !>foo::*a*
     #,foo::*a*
     ACL2 !>'#,foo::*a*
     #,foo::*a*
     ACL2 !>(cdr '#,foo::*a*)
     (2 3)
     ACL2 !>

We conclude by an example showing some extra care that may be important
to consider taking.  We start with:

     (defconst |*BaR*| '(3 4))

Then the following works just fine; but try it without the extra code
for the may-need-slashes case and you'll see that the sharp-dot
printing is missing.  First:

     (table evisc-table
            |*BaR*|
            (let ((x (symbol-name '|*BaR*|)))
              (if (may-need-slashes x)
                  (concatenate 'string "#.|" x "|")
                (concatenate 'string "#." x))))

Then:

     ACL2 !>|*BaR*|
     #,|*BaR*|
     ACL2 !>

IN-ARITHMETIC-THEORY    designate theory for some rewriting done for non-linear arithmetic

We assume familiarity with theories; in particular, see
IN-THEORY for the normal way to set the current theory.  Here, we
discuss an analogous event that pertains only to non-linear arithmetic
(see NON-LINEAR-ARITHMETIC).

     Example:
     (in-arithmetic-theory '(lemma1 lemma2))

     General Form:
     (in-arithmetic-theory term :doc doc-string)

where term is a term that when evaluated will produce a theory (see
THEORIES), and doc-string is an optional documentation string
not beginning with ":Doc-Section ...".  Except for the variable world,
term must contain no free variables.  Term is evaluated with the
variable world bound to the current world to obtain a theory and the
corresponding runic theory (see THEORIES) is then used by
non-linear arithmetic (see NON-LINEAR-ARITHMETIC).

Warning:  If term involves macros such as ENABLE and DISABLE you will
probably not get what you expect!  Those macros are defined relative to
the CURRENT-THEORY.  But in this context you might wish they were
defined in terms of the "CURRENT-ARITHMETIC-THEORY" which is not
actually a defined function.  We do not anticipate that users will
repeatedly modify the arithmetic theory.  We expect term most often to
be a constant list of runes and so have not provided "arithmetic theory
manipulation functions" analogous to CURRENT-THEORY and ENABLE.

BECAUSE NO UNIQUE name is associated with an in-arithmetic-theory event,
there is no way we can store the documentation string doc-string in our
il[documentation] data base.  Hence, we actually prohibit doc-string
from having the form of an ACL2 documentation string; see
DOC-STRING.

See NON-LINEAR-ARITHMETIC.

IN-THEORY    designate "current" theory (enabling its rules)

     Example:
     (in-theory (set-difference-theories
                  (universal-theory :here)
                  '(flatten (:executable-counterpart flatten))))

     General Form:
     (in-theory term :doc doc-string)

where term is a term that when evaluated will produce a theory (see
THEORIES), and doc-string is an optional documentation string
not beginning with ":Doc-Section ...".  Except for the variable world,
term must contain no free variables.  Term is evaluated with the
variable world bound to the current world to obtain a theory and the
corresponding runic theory (see THEORIES) is then made the
current theory.  Thus, immediately after the in-theory, a rule is
enabled iff its rule name is a member of the runic interpretation (see
THEORIES) of some member of the value of term.  See
THEORY-FUNCTIONS for a list of the commonly used theory manipulation
functions.

Because no unique name is associated with an in-theory event, there is
no way we can store the documentation string doc-string in our
documentation data base.  Hence, we actually prohibit doc-string from
having the form of an ACL2 documentation string; see DOC-STRING.

Note that it is often useful to surround in-theory events with local,
that is, to use (local (in-theory ...)).  This use of local in
encapsulate events and books will prevent the effect of this theory
change from being exported outside the context of that encapsulate or
book.

Also see HINTS for a discussion of the :in-theory hint,
including some explanation of the important point that an :in-theory
hint will always be evaluated relative to the current ACL2 logical
world, not relative to the theory of a previous goal.

INCLUDE-BOOK    load the events in a file

     Examples:
     (include-book "my-arith")
     (include-book "/home/smith/my-arith")
     (include-book "/../../my-arith")

     General Form:
     (include-book file :load-compiled-file action
                        :uncertified-okp t/nil      ; [default t]
                        :defaxioms-okp t/nil        ; [default t]
                        :skip-proofs-okp t/nil      ; [default t]
                        :ttags ttags                ; [default nil]
                        :dir directory
                        :doc doc-string)

where file is a book name.  See BOOKS for general information,
see BOOK-NAME for information about book names, and see
PATHNAME for information about file names.  Action is one of t, nil,
:default, :warn, or :comp; these values are explained below, and the
default is :default.  The three -okp keyword arguments, which default
to t, determine whether errors or warnings are generated under certain
conditions explained below; when the argument is t, warnings are
generated.  The dir argument, if supplied, is a keyword that represents
an absolute pathname for a directory (see PATHNAME), to be used
instead of the current book directory (see CBD) for resolving
the given file argument to an absolute pathname.  In particular, by
default :dir :system resolves file using the distributed books/
directory of your ACL2 installation, unless your ACL2 executable was
built somewhere other than where it currently resides; please see the
"Distributed Books Directory" below.  To define other keywords that can
be used for dir, see ADD-INCLUDE-BOOK-DIR.  Doc-string is an
optional documentation string; see DOC-STRING.  If the book has
no certificate, if its certificate is invalid or if the certificate was
produced by a different version of ACL2, a warning is printed and the
book is included anyway; see CERTIFICATE.  This can lead to
serious errors, perhaps mitigated by the presence of a .port file from
an earlier certification; see UNCERTIFIED-BOOKS.  If the
portcullis of the certificate (see PORTCULLIS) cannot be raised
in the host logical world, an error is caused and no change occurs to
the logic.  Otherwise, the non-local events in file are assumed.  Then
the keep of the certificate is checked to ensure that the correct files
were read; see KEEP.  A warning is printed if uncertified books
were included.  Even if no warning is printed, include-book places a
burden on you; see CERTIFICATE.

If you use guards, please note include-book is executed as though
(set-guard-checking nil) has been evaluated; see
SET-GUARD-CHECKING.  If you want guards checked, please see
LD and/or see REBUILD.

The value, action, of :load-compiled-file controls whether a compiled
file is loaded by include-book.  If compilation has been suppressed by
(set-compiler-enabled nil), then action is coerced to nil; see
COMPILATION.  Otherwise, if action is missing or its value is the
keyword :default, then it is treated as :warn.  If action is nil, no
attempt is made to load the compiled file for the book provided.  In
order to load the compiled file, it must be more recent than the book's
certificate (except in raw mode, where it must be more recent than the
book itself; see SET-RAW-MODE).  For non-nil values of action
that do not result in a loaded compiled file, ACL2 proceeds as follows.
Note that a load of a compiled file or expansion file aborts partway
through whenever an include-book form is encountered for which no
suitable compiled or expansion file can be loaded.  For much more
detail, see BOOK-COMPILED-FILE.

     t: Cause an error if the compiled file is not loaded.  This same
     requirement is imposed on every include-book form evaluated during
     the course of evaluation of the present include-book form, except
     that for those subsidiary include-books that do not themselves
     specify :load-compiled-file t, it suffices to load the expansion
     file (see BOOK-COMPILED-FILE).

     :warn: An attempt is made to load the compiled file, and a warning
     is printed if that load fails to run to completion.

     :comp: A compiled file is loaded as with value t, except that if a
     suitable "expansion file" exists but the compiled file does not,
     then the compiled file is first created.  See
     BOOK-COMPILED-FILE.

The three -okp arguments, :uncertified-okp, defaxioms-okp, and
skip-proofs-okp, determine the system's behavior when the book or any
subbook is found to be uncertified, when the book or any subbook is
found to contain defaxiom events, and when the book or any subbook is
found to contain skip-proofs events, respectively.  All three default
to t, which means it is "ok" for the condition to arise.  In this case,
a warning is printed but the processing to load the book is allowed to
proceed.  When one of these arguments is nil and the corresponding
condition arises, an error is signaled and processing is aborted.
*Exception*: :uncertified-okp is ignored if the include-book is being
performed on behalf of a certify-book.

The keyword argument :ttags may normally be omitted.  A few constructs,
used for example if you are building your own system based on ACL2, may
require it.  See DEFTTAG for an explanation of this argument.

Include-book is similar in spirit to encapsulate in that it is a single
event that "contains" other events, in this case the events listed in
the file named.  Include-book processes the non-local event forms in
the file, assuming that each is admissible.  Local events in the file
are ignored.  You may use include-book to load several books, creating
the logical world that contains the definitions and theorems of all of
them.

If any non-local event of the book attempts to define a name that has
already been defined -- and the book's definition is not syntactically
identical to the existing definition -- the attempt to include the book
fails, an error message is printed, and no change to the logical world
occurs.  See REDUNDANT-EVENTS for the details.

When a book is included, the default defun-mode (see
DEFAULT-DEFUN-MODE) for the first event is always :logic.  That is,
the default defun-mode "outside" the book -- in the environment in
which include-book was called -- is irrelevant to the book.  Events
that change the defun-mode are permitted within a book (provided they
are not in local forms).  However, such changes within a book are not
exported, i.e., at the conclusion of an include-book, the "outside"
default defun-mode is always the same as it was before the include-book.

Unlike every other event in ACL2, include-book puts a burden on you.
Used improperly, include-book can be unsound in the sense that it can
create an inconsistent extension of a consistent logical world.  A
certification mechanism is available to help you carry this burden --
but it must be understood up front that even certification is no
guarantee against inconsistency here.  The fundamental problem is one
of file system security.  See CERTIFICATE for a discussion of
the security issues.

At the beginning of execution of an include-book form, even before
executing portcullis commands, the value of acl2-defaults-table is
restored to the value it had at startup, except that the value of key
:inhibit-warnings is preserved.  After execution of an include-book
form, the value of acl2-defaults-table is restored to what it was
immediately before that include-book form was executed.  See
ACL2-DEFAULTS-TABLE.

Distributed Books Directory.  We refer to the "books directory" of an
executable image as the full pathname string of the books directory
associated with :dir :system for that image.  This is where the
distributed books directory should reside.  By default, it is the books/
subdirectory of the directory where the sources reside and the
executable image is thus built (except for ACL2(r) -- see REAL
--, where it is books/nonstd/).  If those books reside elsewhere, the
environment variable ACL2_SYSTEM_BOOKS can be set to the books/
directory under which they reside (a Unix-style pathname, typically
ending in books/ or books, is permissible).  In most cases, your ACL2
executable is a small script in which you can set this environment
variable just above the line on which the actual ACL2 image is invoked,
for example:

     export ACL2_SYSTEM_BOOKS
     ACL2_SYSTEM_BOOKS=/home/acl2/4-0/acl2-sources/books

This concludes the guided tour through books.  See
SET-COMPILE-FNS for a subtle point about the interaction between
include-book and on-the-fly compilation.  See CERTIFY-BOOK for
a discussion of how to certify a book.

:cited-by Programming

LOCAL    hiding an event in an encapsulation or book

     Examples:
     (local (defthm hack1
              (implies (and (acl2-numberp x)
                            (acl2-numberp y)
                            (equal (* x y) 1))
                       (equal y (/ x)))))

     (local (defun double-naturals-induction (a b)
              (cond ((and (integerp a) (integerp b) (< 0 a) (< 0 b))
                     (double-naturals-induction (1- a) (1- b)))
                    (t (list a b)))))

     General Form:
     (local ev)

where ev is an event form.  If the current default defun-mode (see
DEFAULT-DEFUN-MODE) is :logic and ld-skip-proofsp is nil or t,
then (local ev) is equivalent to ev.  But if the current default
defun-mode is :program or if ld-skip-proofsp is 'include-book, then
(local ev) is a no-op.  Thus, if such forms are in the event list of an
encapsulate event or in a book, they are processed when the
encapsulation or book is checked for admissibility in :logic mode but
are skipped when extending the host world.  Such events are thus
considered "local" to the verification of the encapsulation or book.
The non-local events are the ones "exported" by the encapsulation or
book.  See ENCAPSULATE for a thorough discussion.  Also see
LOCAL-INCOMPATIBILITY for a discussion of a commonly
encountered problem with such event hiding:  you can't make an event
local if its presence is required to make sense of a non-local one.

Note that events that change the default defun-mode, and in fact any
events that set the acl2-defaults-table, are disallowed inside the
scope of local.  See EMBEDDED-EVENT-FORM.

MAKE-EVENT    evaluate (expand) a given form and then evaluate the result

Make-event is a utility for generating events.  It provides a
capability not offered by Lisp macros (see DEFMACRO), as it
allows access to the ACL2 state and logical world.  In essence, the
expression (make-event form) replaces itself with the result of
evaluating form, say, ev, as though one had submitted ev instead of the
make-event call.  But the evaluation of form may involve state and even
modify state, for example by attempting to admit some definitions and
theorems.  Make-event protects the ACL2 logical world so that it is
restored after form is evaluated, before ev is submitted.

     Examples:

     ; Trivial example: evaluate (quote (defun foo (x) x)) to obtain
     ; (defun foo (x) x), which is then evaluated.
     (make-event (quote (defun foo (x) x)))

     ; Evaluate (generate-form state) to obtain (mv nil val state), and
     ; then evaluate val.  (Generate-form is not specified here, but
     ; imagine for example that it explores the state and then generates
     ; some desired definition or theorem.)
     (make-event (generate-form state))

     ; As above, but make sure that if this form is in a book, then when
     ; we include the book, the evaluation of (generate-form state)
     ; should return the same value as it did when the book was
     ; certified.
     (make-event (generate-form state)
                 :check-expansion t)

     ; As above (where the :check-expansion value can be included or
     ; not), where if there is an error during expansion, then the error
     ; message will explain that expansion was on behalf of the indicated
     ; object, typically specified as the first argument.
     (make-event (generate-form state)
                 :on-behalf-of (generate-form state))

     General Form:
     (make-event form :check-expansion chk :on-behalf-of obj)

where chk is nil (the default), t, or the intended "expansion result"
from the evaluation of form (as explained below); and if supplied, obj
is an arbitrary ACL2 object, used only in reporting errors in
expansion, i.e., in the evaluation of form.

We strongly recommend that you browse some .lisp files in the
distribution directory books/make-event/.  You may even find it helpful,
in order to understand make-event, to do so before continuing to read
this documentation.  For example, eval.lisp contains definitions of
macros must-succeed and must-fail that are useful for testing and are
used in many other books in that directory, especially eval-tests.lisp.
Another example, defrule.lisp, shows how to use macros whose calls
expand to make-event forms, which in turn can generate events.  For more
examples, see file Readme.lsp in the above directory.  Other than the
examples, the explanations here should suffice for most users.  If you
want explanations of subtler details, see MAKE-EVENT-DETAILS.

Note that make-event may only be used at the "top level" or where an
event is expected.  See the section "Restriction to Event Contexts",
below.

Make-event is related to Lisp macroexpansion in the sense that its
argument is evaluated to obtain an expansion result, which is evaluated
again.  Let us elaborate on each of these notions in turn: "is
evaluated," "expansion result", and "evaluated again."

     "is evaluated" -- The argument can be any expression, which is
     evaluated as would be any expression submitted to ACL2's top level
     loop.  Thus, state and user-defined stobjs may appear in the form
     supplied to make-event.  Henceforth, we will refer to this
     evaluation as "expansion."  Expansion is actually done in a way
     that restores ACL2's built-in state global variables, including
     the logical world, to their pre-expansion values (with a few
     exceptions -- see MAKE-EVENT-DETAILS -- and where we note
     that changes to user-defined state global variables (see
     ASSIGN) are preserved).  So, for example, events might be
     evaluated during expansion, but they will disappear from the
     logical world after expansion returns its result.  Moreover,
     proofs are enabled by default at the start of expansion (see
     LD-SKIP-PROOFSP), because an anticipated use of make-event is to
     call the prover to decide which event to generate, and that would
     presumably be necessary even if proofs had been disabled.

     "expansion result" -- The above expansion may result in an ordinary
     (non-state, non-stobj) value, which we call the "expansion
     result."  Or, expansion may result in a multiple value of the form
     (mv erp val state stobj-1 ... stobj-k), where k may be 0; in fact
     the most common case is probably (mv erp val state).  In that
     case, if erp is not nil, then there is no expansion result, and
     the original make-event evaluates to a soft error.  If however erp
     is nil, then the resulting value is val.  Moreover, val must be an
     embedded event form (see EMBEDDED-EVENT-FORM); otherwise,
     the original make-event evaluates to a soft error.  Note that
     error messages from expansion are printed as described under
     "Error Reporting" below.

     "evaluated again" -- the expansion result is evaluated in place of
     the original make-event.

Note that the result of expansion can be an ordinary event, but it can
instead be another call of make-event, or even of a call of a macro that
expands to a call of make-event.  Or, expansion itself can cause
subsidiary calls of make-event, for example if expansion uses ld to
evaluate some make-event forms.  The state global variable
make-event-debug may be set to a non-nil value in order to see a trace
of the expansion process, where the level shown (as in "3>") indicates
the depth of expansions in progress.

Expansion of a make-event call will yield an event that replaces the
original make-event call.  In particular, if you put a make-event form
in a book, then in essence it is replaced by its expansion result,
created during the proof pass of the certify-book process.  We now
elaborate on this idea of keeping the original expansion.

By default, a make-event call in a certified book is replaced (by a
process hidden from the user, in an :expansion-alist field of the book's
certificate) by the expansion result from evaluation of its first
argument.  Thus, although the book is not textually altered during
certification, one may imagine a "book expansion" corresponding to the
original book in which all of the events for which expansion took place
(during the proof phase of certification) have been replaced by their
expansions.  A subsequent include-book will then include the book
expansion corresponding to the indicated book.  When a book is compiled
during certify-book, it is actually the corresponding book expansion,
stored as a temporary file, that is compiled instead.  That temporary
file is deleted after compilation unless one first evaluates the form
(assign keep-tmp-files t).  Note however that all of the original forms
must still be legal events (see EMBEDDED-EVENT-FORM).  So for
example, if the first event in a book is (local (defmacro my-id (x)
x)), followed by (my-id (make-event ...)), the final "include-book"
pass of certify-book will fail because my-id is not defined when the
my-id call is encountered.

The preceding paragraph begins with "by default" because if you specify
:check-expansion t, then subsequent evaluation of the same make-event
call -- during the second pass of an encapsulate or during event
processing on behalf of include-book -- will do the expansion again and
check that the expansion result equals the original expansion result.
In the unusual case that you know the expected expansion result, res,
you can specify :check-expansion res.  This will will cause a check that
every subsequent expansion result for the make-event form is res,
including the original one.  IMPORTANT NOTE: That expansion check is
only done when processing events, not during a preliminary load of a
book's compiled file.  The following paragraph elaborates.

(Here are details on the point made just above, for those who use the
:check-expansion argument to perform side-effects on the state.  When
you include a book, ACL2 generally loads a compiled file before
processing the events in the book; see BOOK-COMPILED-FILE.
While it is true that a non-nil :check-expansion argument causes
include-book to perform expansion of the make-event form during event
processing it does _not_ perform expansion when the compiled file (or
expansion file; again, see BOOK-COMPILED-FILE) is loaded.)

ACL2 performs the following space-saving optimization for book
certificates: a local event arising from make-event expansion is
replaced in that expansion by (local (value-triple :ELIDED)).

Finally, we note that ACL2 extends the notion of "make-event expansion"
to the case that a call of make-event is found in the course of
macroexpansion.  We illustrate with the following example.

     (encapsulate
      ()
      (defmacro my-mac ()
        '(make-event '(defun foo (x) x)))
      (my-mac))
     :pe :here

The above call of pe shows that the form (my-mac) has a make-event
expansion of (DEFUN FOO (X) X):

     (ENCAPSULATE NIL
                  (DEFMACRO MY-MAC
                            NIL
                            '(MAKE-EVENT '(DEFUN FOO (X) X)))
                  (RECORD-EXPANSION (MY-MAC)
                                    (DEFUN FOO (X) X)))

*Error Reporting.*

Suppose that expansion produces a soft error as described above.  That
is, suppose that the argument of a make-event call evaluates to a
multiple value (mv erp val state ...) where erp is not nil.  If erp is
a string, then that string is printed in the error message.  If erp is
a cons pair whose car is a string, then the error prints "~@0" with #\0
bound to that cons pair; see FMT.  Any other non-nil value of
erp causes a generic error message to be printed.

*Restriction to Event Contexts.*

A make-event call must occur either at the top level or as an argument
of an event constructor, as explained in more detail below.  This
restriction is imposed to enable ACL2 to track expansions produced by
make-event.  The following examples illustrate this restriction.

     ; Legal:
     (progn (with-output
             :on summary
             (make-event '(defun foo (x) x))))

     ; Illegal:
     (mv-let (erp val state)
             (make-event '(defun foo (x) x))
             (mv erp val state))

More precisely: after macroexpansion has taken place, a make-event call
must be in an "event context", defined recursively as follows.  (All but
the first two cases below correspond to similar cases for constructing
events; see EMBEDDED-EVENT-FORM.)

     o A form submitted at the top level, or more generally, supplied
     to a call of ld, is in an event context.

     o A form occurring at the top level of a book is in an event
     context.

     o If (LOCAL x1) is in an event context, then so is x1.

     o If (SKIP-PROOFS x1) is in an event context, then so is x1.

     o If (MAKE-EVENT x ...) is in an event context and its expansion
     x1 is an embedded event form, then x1 is in an event context.

     o If (WITH-OUTPUT ... x1), (WITH-PROVER-STEP-LIMIT ... x1 ...), or
     (WITH-PROVER-TIME-LIMIT ... x1) is in an event context, then so is
     x1.

     o Given a call of PROGN or PROGN! in an event context, each of its
     arguments is in an event context.

     o Given a call of ENCAPSULATE in an event context, each of its
     arguments except the first (the signature list) is in an event
     context.

     o If (RECORD-EXPANSION x1 x2) is in an event context, then x1 and
     x2 are in event contexts.  Note: record-expansion is intended for
     use only by the implementation, which imposes the additional
     restriction that x1 and its subsidiary make-event calls (if any)
     must specify a :check-expansion argument that is a consp.

Low-level remark, for system implementors.  There is the one exception
to the above restriction: a single state-global-let* form immediately
under a progn! call.  For example:

     (progn! (state-global-let* <bindings> (make-event ...)))

However, the following form may be preferable (see PROGN!):

     (progn! :state-global-bindings <bindings> (make-event ...))

See REMOVE-UNTOUCHABLE for an interesting use of this exception.

*Examples illustrating how to access state*

You can modify the ACL2 state by doing your state-changing computation
during the expansion phase, before expansion returns the event that is
submitted.  Here are some examples.

First consider the following.  Notice that expansion modifies state
global my-global during make-event expansion, and then expansion
returns a defun event to be evaluated.

     (make-event
       (er-progn (assign my-global (length (w state)))
                 (value '(defun foo (x) (cons x x)))))

Then we get:

       ACL2 !>(@ my-global)
       72271
       ACL2 !>:pe foo
        L        1:x(MAKE-EVENT (ER-PROGN # #))

       >L            (DEFUN FOO (X) (CONS X X))
       ACL2 !>

Here's a slightly fancier example, where the computation affects the
defun.  In a new session, execute:

     (make-event
       (er-progn (assign my-global (length (w state)))
                 (value `(defun foo (x) (cons x ,(@ my-global))))))

Then:

       ACL2 !>(@ my-global)
       72271
       ACL2 !>:pe foo
        L        1:x(MAKE-EVENT (ER-PROGN # #))

       >L            (DEFUN FOO (X) (CONS X 72271))
       ACL2 !>

Note that ACL2 table events may avoid the need to use state globals.
For example, instead of the example above, consider this example in a
new session.

     (make-event
       (let ((world-len (length (w state))))
         `(progn (table my-table :stored-world-length ,world-len)
                 (defun foo (x) (cons x ,world-len)))))

Then:

       ACL2 !>(table my-table)
        ((:STORED-WORLD-LENGTH . 72271))
       ACL2 !>:pe foo
                 1:x(MAKE-EVENT (LET # #))

       >L            (DEFUN FOO (X) (CONS X 72271))
       ACL2 !>

By the way, most built-in state globals revert after expansion.  But
your own global (like my-global above) can be set during expansion, and
the new value will persist.

MAKE-EVENT-DETAILS    details on make-event expansion

The normal user of make-event can probably ignore this section, but we
include it for completeness.  We assume that the reader has read and
understood the basic documentation for make-event (see
MAKE-EVENT), but we begin below with a summary of expansion.

*Introduction*

Here is a summary of how we handle expansion involving make-event forms.

(make-event form :check-expansion nil)

This shows the :check-expansion default of nil, and is typical user
input.  We compute the expansion exp of form, which is the expansion of
the original make-event expression and is evaluated in place of that
expression.

(make-event form :check-expansion t)

The user presumably wants it checked that the expansion doesn't change
in the future, in particular during include-book.  If the expansion of
form is exp, then we will evaluate exp to obtain the value as before,
but this time we record that the expansion of the original make-event
expression is (make-event form :check-expansion exp) rather than simply
exp.

(make-event form :check-expansion exp) ; exp a cons

This is generated for the case that :check-expansion is t, as explained
above.  Evaluation is handled as described in that above case, except
here we check that the expansion result is the given exp.  (Actually,
the user is also allowed supply such a form.)  The original make-event
expression does not undergo any expansion (intuitively, it expands to
itself).

Now let us take a look at how we expand progn forms (encapsulate is
handled similarly).

(progn ... (make-event form :check-expansion nil) ...)

The expansion is obtained by replacing the make-event form as follows.
Let exp be the expansion of form,  Then replace the above make-event
form, which we denote as F, by (record-expansion F exp).  Here,
record-expansion is a macro that returns its second argument.

(progn ... (make-event form :check-expansion t) ...)

The expansion is of the form (record-expansion F exp) as in the nil
case above, except that this time exp is (make-event form
:check-expansion exp'), where exp' is the expansion of form.

(progn ... (make-event form :check-expansion exp) ...) ; exp a cons

No expansion takes place unless expansion takes place for at least one
of the other subforms of the progn, in which case each such form F is
replaced by (record-expansion F exp) where exp is the expansion of F.

*Detailed semantics*

In our explanation of the semantics of make-event, we assume familiarity
with the notion of "embedded event form" (see
EMBEDDED-EVENT-FORM).

Let's say that the "actual embedded event form" corresponding to a given
form is the underlying call of an ACL2 event: that is, LOCALs are
dropped when ld-skip-proofsp is 'include-book, and macros are expanded
away, thus leaving us with a progn, a make-event, or an event form
(possibly encapsulate), any of which might have surrounding local,
skip-proofs, or with-output calls.

Thus, such an actual embedded event form can be viewed as having the
form (rebuild-expansion wrappers base-form) where base-form is a progn,
a make-event, or an event form (possibly encapsulate), and wrappers are
(as in ACL2 source function destructure-expansion) the result of
successively removing the event form from the result of macroexpansion,
leaving a sequence of (local), (skip-proofs), and (with-output ...)
forms.  In this case we say that the form "destructures into" the
indicated wrappers and base-form, and that it can be "rebuilt from"
those wrappers and base-form.

Elsewhere we define the notion of the "expansion result" from an
evaluation (see MAKE-EVENT), and we mention that when expansion
concludes, the ACL2 logical world and most of the state are restored to
their pre-expansion values.  Specifically, after evaluation of the
argument of make-event (even if it is aborted), the ACL2 logical world
is restored to its pre-evaluation value, as are all state global
variables in the list *protected-system-state-globals*.  Thus,
assignments to user-defined state globals (see ASSIGN) do
persist after expansion, since they are not in that list.

We recursively define the combination of evaluation and expansion of an
embedded event form, as follows.  We also simultaneously define the
notion of "expansion takes place," which is assumed to propagate upward
(in a sense that will be obvious), such that if no expansion takes
place, then the expansion of the given form is considered to be itself.
It is useful to keep in mind a goal that we will consider later: Every
make-event subterm of an expansion result has a :check-expansion field
that is a consp, where for this purpose make-event is viewed as a macro
that returns its :check-expansion field.  (Implementation note: The
latest expansion of a make-event, progn, progn!, or encapsulate is
stored in state global 'last-make-event-expansion, except that if no
expansion has taken place for that form then 'last-make-event-expansion
has value nil.)

     If the given form is not an embedded event form, then simply cause
     a soft error, (mv erp val state) where erp is not nil.  Otherwise:

     If the evaluation of the given form does not take place
     (presumably because local events are being skipped), then no
     expansion takes place.  Otherwise:

     Let x be the actual embedded event form corresponding to the given
     form, which destructures into wrappers W and base-form B.  Then the
     original form is evaluated by evaluating x, and its expansion is as
     follows.

     If B is (make-event form :check-expansion val), then expansion
     takes place if and only if val is not a consp and no error occurs,
     as now described.  Let R be the expansion result from protected
     evaluation of form, if there is no error.  R must be an embedded
     event form, or it is an error.  Then evaluate/expand R, where if
     val is not nil then state global 'ld-skip-proofsp is initialized
     to nil.  (This initialization is important so that subsequent
     expansions are checked in a corresponding environment, i.e., where
     proofs are turned on in both the original and subsquent
     environments.)  It is an error if this evaluation causes an error.
     Otherwise, the evaluation yields a value, which is the result of
     evaluation of the original make-event expression, as well as an
     expansion, E_R.  Let E be rebuilt from W and E_R.  The expansion of
     the original form is E if val is nil, and otherwise is the result
     of replacing the original form's :check-expansion field with E,
     with the added requirement that if val is not t (thus, a consp)
     then E must equal val or else we cause an error.

     If B is either (progn form1 form2 ...) or (encapsulate sigs form1
     form2 ...), then after evaluating B, the expansion of the original
     form is the result of rebuilding from B, with wrappers W, after
     replacing each formi in B for which expansion takes place by
     (record-expansion formi formi'), where formi' is the expansion of
     formi.  Note that these expansions are determined as the formi are
     evaluated in sequence (where in the case of encapsulate, this
     determination occurs only during the first pass).  Except, if no
     expansion takes place for any formi, then the expansion of the
     original form is itself.

     Otherwise, the expansion of the original form is itself.

Similarly to the progn and encapsulate cases above, book certification
causes a book to be replaced by its so-called "book expansion."  There,
each event ev for which expansion took place during the proof pass of
certification -- say, producing ev' -- is replaced by (record-expansion
ev ev').

Implementation Note.  The book expansion is actually implemented by way
of the :expansion-alist field of its certificate, which associates
0-based positions of top-level forms in the book (not including the
initial in-package form) with their expansions.  Thus, the book's
source file is not overwritten; rather, the certificate's
expansion-alist is applied when the book is included or compiled.  End
of Implementation Note.

It is straightforward by computational induction to see that for any
expansion of an embedded event form, every make-event sub-event has a
consp :check-expansion field.  Here, by "sub-event" we mean to expand
macros; and we also mean to traverse progn and encapsulate forms as
well as :check-expansion fields of make-event forms.  Thus, we will
only see make-event forms with consp :check-expansion fields in the
course of include-book forms, the second pass of encapsulate forms, and
raw Lisp.  This fact guarantees that an event form will always be
treated as its original expansion.

*Notes on ttags*

See DEFTTAG for documentation of the notion of "trust tag"
("ttag").  We note here that even if an event (defttag tag-name) for
non-nil tag-name is admitted only during the expansion phase of a
make-event form, then such expansion will nevertheless still cause
tag-name to be recorded in the logical world (assuming that the
make-event form is admitted).  So in order to certify such a book, a
suitable :ttags argument must be supplied; see CERTIFY-BOOK.

ACL2 does provide a way to avoid the need for :ttags arguments in such
cases.  The idea is to certify a book twice, where the results of
make-event expansion are saved from the first call of certify-book and
provided to the second call.  see SET-WRITE-ACL2X.

Finally, we discuss a very unusual case where certification does not
involve trust tags but a subsequent include-book does involve trust
tags: a make-event call specifying :check-expansion t, whose expansion
generates a defttag event during include-book but not certify-book.
Consider the following book.

     (in-package "ACL2")
     (make-event
      (er-progn
       (if (@ skip-notify-on-defttag) ; non-nil when including a certified book
           (pprogn
            (fms "Value of (@ skip-notify-on-defttag): ~x0~|"
                 (list (cons #0 (@ skip-notify-on-defttag)))
                 *standard-co* state nil)
            (encapsulate
             ()
             (defttag :foo)
             (value-triple "Imagine something bad here!")))
         (value nil))
       (value '(value-triple :some-value)))
      :check-expansion t)

This book certifies successfully without the need for a :ttags argument
for certify-book.  Indeed, the above book's certificate does not
specify :foo as a trust tag associated with the book, because no
defttag event was executed during book certification.  Unfortunately, if
we try to include this book without specifying a value of :ttags that
allows :foo, book inclusion will cause executing of the above defttag.
If that inclusion happens in the context of certifying some superior
book and the appropriate :ttags arguments have not been provided, that
certification will fail.

MEMOIZE    turn on memoization for a specified function

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION for a general discussion of memoization and the
related features of hash consing and applicative hash tables.

     Examples:
     (memoize 'foo)                      ; remember the values of calls
                                         ;   of foo
     (memoize 'foo :condition t)         ; same as above
     (memoize 'foo :condition '(test x)) ; memoize for args satisfying
                                         ;   the given condition
     (memoize 'foo :condition-fn 'test)  ; memoize for args satisfying
                                         ;   a call of the given function
     (memoize 'foo :inline nil)          ; do not inline the definition
                                         ;   of foo
     (memoize 'foo :recursive nil)       ; as above, i.e. :inline nil
     (memoize 'foo :aokp t)              ; attachments OK for stored results
     (memoize 'foo :ideal-okp t)         ; memoize even if foo is in :logic mode
                                         ;   but has not been guard-verified

     * Menu:

     Related topics other than immediate subtopics:
     * HONS-AND-MEMOIZATION:: hash cons, function memoization, and applicative hash tables

     General Form:
     (memoize fn                         ; memoizes fn and returns fn
              :condition    condition    ; optional (default t)
              :condition-fn condition-fn ; optional
              :hints        hints        ; optional, for verifying the
                                         ;   guards of condition-fn
              :otf-flg      otf-flg      ; optional, for verifying the
                                         ;   guards of condition-fn
              :inline       inline       ; optional (default t)
              :recursive    inline       ; optional (default t)
              :commutative  t/lemma-name ; optional (default nil)
              :forget       t/nil        ; optional (default nil)
              :memo-table-init-size size ; optional (default *mht-default-size*)
              :aokp         t/nil        ; optional (default nil)
              :ideal-okp    t/:warn/nil  ; optional (default nil)
              :verbose      t/nil        ; optional (default t)
              )

where fn evaluates to a user-defined function symbol; condition is
either t (the default), 't, nil, or 'nil, or else evaluates to an
expression whose free variables are among the formal parameters of fn;
and condition-fn is either nil (the default) or else evaluates to a
legal function symbol.  Further restrictions and options are discussed
below.  Note that all arguments are evaluated (but for the special
handling of value t for :commutative, the argument must literally be t;
see below).

Generally fn must evaluate to a defined function symbol.  However, this
value can be the name of a macro that is associated with such a function
symbol; see MACRO-ALIASES-TABLE.  That associated function
symbol is the one called "memoized" in the discussion below, but we
make no more mention of this subtlety.

In the most common case, memoize takes a single argument, which
evaluates to a function symbol.  We call this function symbol the
"memoized function" because "memos" are saved and re-used, in the
following sense.  When a call of the memoized function is evaluated,
the result is "memoized" by associating the call's arguments with that
result, in a suitable table.  But first an attempt is made to avoid
such evaluation, by doing a lookup in that table on the given arguments
for the result, as stored for a previous call on those arguments.  If
such a result is found, then it is returned without further
computation.  This paragraph also applies if :condition is supplied but
is t or 't.

If keyword argument :condition-fn is supplied, but :condition is not,
then the result of evaluating :condition-fn must be a defined function
symbol whose formal parameter list and guard are the same as for the
function being memoized.  If fn is in :logic mode, then guards must
have been verified for :condition-fn.  Such a "condition function" will
be run whenever the memoized function is called, on the same
parameters, and the lookup or table store described above are only
performed if the result from the condition function call is non-nil.

Suppose however that :condition is supplied.  If the value supplied is
t or 't, then the lookup and table store described above are always
done.  If the value is nil or 'nil, then this lookup and table store
are never done, although statistics may be gathered; see
PROFILE.  Now consider other values for :condition.  An attempt will
be made to define a condition function whose guard and formal
parameters list are the same as those of the memoized function, and
whose body is the result, r, of evaluating the given condition.  The
name of that condition function is the result of evaluating
:condition-fn if supplied, else is the result of concatenating the
string "-MEMOIZE-CONDITION" to the end of the name of the memoized
function.  The condition function will be defined with guard
verification turned off, but that definition will be followed
immediately by a verify-guards event; and this is where the optional
:hints and :otf-flg are attached.  At evaluation time the condition
function is used as described in the preceding paragraph; so in effect,
the condition (r, above) is evaluated, with its variables bound to the
corresponding actuals of the memoized function call, and the memoized
function attempts a lookup or table store if and only if the result of
that evaluation is non-nil.

Note that fn can be either a :logic mode function or a :program mode
function.  However, only the corresponding raw Lisp function is
actually memoized, so guard violations can defeat memoization, and
:logic mode functions without their guards verified will only be
memoized when called by :program mode functions.  (See
GUARDS-AND-EVALUATION for more information about guards and
evaluation in ACL2.)  If fn is a :logic mode function and :condition is
supplied and not t or nil, then the condition must be a guard-verified
function.

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

Suppose that a function is already memoized.  Then it is illegal to
memoize that function.  Moreover, if the function was memoized with an
associated condition (i.e., was memoized with keyword :condition or
:condition-fn having value other than t or nil), then it is also
illegal to convert the function from :program to :logic mode (see
VERIFY-TERMINATION).  To turn off memoization, see UNMEMOIZE.

Memoize is illegal for a function if its arguments include state or if
it returns any stobjs.  Also, memoize never allows attachments to be
used (see DEFATTACH); if an attachment is used during
evaluation, then the evaluation result will not be stored.

We conclude with by documenting keyword parameters not discussed above.

Keyword parameter :recursive is a synonym for :inline.  Each must be
given the same Boolean value, and both are t by default.  When either is
supplied the value nil, then memoize does not use the definitional body
of fn in the body of the new, memoized definition of fn.  Instead,
memoize lays down a call to the symbol-function for fn that was in
effect prior to memoization.  Use value nil for :inline or :recursive
to avoid memoizing recursive calls to fn directly from within fn.

If :trace has a non-nil value, then memoize also traces in a
traditional Lisp style.  If :trace has value notinline or notinline,
then a corresponding declaration is added at the beginning of the new
definition of fn.

A non-nil value for :commutative can be supplied if fn is a binary
function in :logic mode.  If the memoize event is successful, then
subsequently: whenever each argument to fn is either a rational number
or a hons, then when the evaluation of fn on those arguments is
memoized, the evaluation of fn on the swap of those arguments is, in
essence, also memoized.  If :commutative is supplied and is not nil or
t, then it should be the name of a previously-proved theorem whose
formula states the commutativity of fn, i.e., is the formula (equal (fn
x y) (fn y x)) for a pair {x,y} of distinct variables.  If :commutative
is t -- but not merely an expression that evaluates to t -- then an
attempt to prove such a lemma will be made on-the-fly.  The name of the
lemma is the symbol in the same package as fn, obtained by adding the
suffix "-COMMUTATIVE" to the symbol-name of fn.  If the proof attempt
fails, then you may want first to prove the lemma yourself with
appropriate hints and perhaps supporting lemmas, and then supply the
name of that lemma as the value of :commutative.

If :commutative is supplied, and a non-commutative condition is provided
by :condition or :condition-fn, then although the results will be
correct, the extra memoization afforded by :commutative is unspecified.

If :memo-table-init-size is supplied, then it should be a positive
integer specifying the initial size of an associated hash table.

Argument :aokp is relevant only when attachments are used; see
DEFATTACH for background on attachments.  When :aokp is nil, the
default, computed values are not stored when an attachment was used, or
even when an attachment may have been used because a function was
called that had been memoized using :aokp t.  Otherwise, computed
values are always stored, but saved values are not used except when
attachments are allowed.  To summarize:

       aokp=nil (default): ``Pure'', i.e., values do not depend on attachments
       - Fetch: always legal
       - Store: only store resulting value when attachments were not used

       aokp=t: ``Impure'', i.e., values may depend on attachments
       - Fetch: only legal when attachments are allowed (e.g., not during proofs)
       - Store: always legal

If :ideal-okp is supplied and not nil, then it is permitted to memoize
an "ideal-mode" function: one in :logic mode whose guards have not been
verified.  In general, it is ill-advised to memoize an ideal-mode
function, because its calls are typically evaluated "in the logic"
without calling a memoized "raw Lisp" version of the function.
However, if the function is called by a :program mode function,
evaluation can transfer to raw Lisp before reaching the call of the
memoized function, in which case memoization will take place.  For such
situations you can provide value :warn or t for keyword parameter
:ideal-okp.  Both of these values allow memoization of ideal-mode
functions, but if :warn is supplied then a warning will take place.
Note that you may set the key :memoize-ideal-okp of the
acl2-defaults-table to value t or :warn to change the default, but if
parameter :ideal-okp is supplied, the acl2-defaults-table value is
ignored.

If :verbose is supplied, it should either be nil, which will inhibit
proof, event, and summary output (see WITH-OUTPUT), or else t
(the default), which does not inhibit output.  If the output baffles
you, try

     :trans1 (memoize ...)

to see the single-step macroexpansion of your memoize call.

The default for :forget is nil.  If :forget is supplied, and not nil,
then it must be t, which causes all memoization done for a top-level
call of fn to be forgotten when that top-level call exits.

MUTUAL-RECURSION    define some mutually recursive functions

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

     General Form:
     (mutual-recursion def1 ... defn)
     where each defi is a call of defun, defund, defun-nx,
     or defund-nx.

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

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

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

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

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

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

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

Technical Note: Each defi above must be a call of defun, defund,
defun-nx, or defund-nx.  In particular, it is not permitted for a defi
to be an arbitrary form that macroexpands into a defun form.  This is
because mutual-recursion is itself a macro, and since macroexpansion
occurs from the outside in, at the time (mutual-recursion def1 ...
defk) is expanded the defi have not yet been macroexpanded.

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

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

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

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

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

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

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

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

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

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

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

PROFILE    turn on profiling for one function

NOTE: An alternative to this utility, which has a lot less
functionality but doesn't depend on the experimental extension of ACL2
mentioned just below, may be found in distributed book
books/misc/profiling.lisp.

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION for a general discussion of memoization, on
which this profile utility is built, and the related features of hash
consing and applicative hash tables.

Profile can be useful in Common Lisp debugging and performance analysis,
including examining the behavior of ACL2 functions.

     Example:
     (profile 'fn)       ; keep count of the calls of fn
     (profile 'fn        ; as above, with with some memoize options
              :trace t
              :forget t)
     (memsum) ; report statistics on calls of memoized functions (e.g., fn)
     (clear-memoize-statistics) ; clear memoization (and profiling) statistics

Evaluation of (profile 'fn) redefines fn so that a count will be kept
of the calls of FN.  The information recorded may be displayed, for
example, by invoking (memoize-summary) or (equivalently) (memsum).  If
you wish to gather fresh statistics for the evaluation of a top-level
form, see CLEAR-MEMOIZE-STATISTICS.

Profile is just a macro that calls memoize to do its work.  Profile
gives the two keyword parameters :CONDITION and :INLINE of memoize the
value nil.  Other keyword parameters for memoize, which must not
include :CONDITION, :CONDITION-FN, or :INLINE, are passed through.  To
eliminate profiling, use unmemoize; for example, to eliminate profiling
for function fn, evaluate (unmemoize 'fn).

You may find raw Lisp functions profile-all and profile-acl2 to be
useful.  Please contact the ACL2 developers if you want versions of
these functions to be executable from inside the ACL2 read-eval-print
loop.

PROGN    evaluate some events

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

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

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

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

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

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

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

PROGN!    evaluate some forms, not necessarily events

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

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

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

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

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

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

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

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

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

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

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

is treated as follows:

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

However, in raw Lisp the former is just:

     (progn form1 form2 ... formk)

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

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

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

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

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

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

REGENERATE-TAU-DATA-BASE    regenerate the tau data base relative to the current enabled theory

     Example:
     (regenerate-tau-data-base)

     General Form:
     (regenerate-tau-data-base :doc doc-string)

where doc-string is an optional documentation string not beginning with
":Doc-Section ...".

The tau data base is regenerated by scanning the current logical world
and re-processing every event in it relative to the current enabled
theory and current tau auto mode settings.

BECAUSE NO UNIQUE name is associated with a regenerate-tau-data-base
event, there is no way we can store the documentation string doc-string
in our il[documentation] data base.  Hence, we actually prohibit
doc-string from having the form of an ACL2 documentation string; see
DOC-STRING.

See TAU-SYSTEM.

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

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

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

where keyword is a keywordp.

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

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

RESTORE-MEMOIZATION-SETTINGS    restore the saved memoization settings

For background on memoization, see MEMOIZE.

     General Form:
     (restore-memoization-settings)

Calls of this macro restore the memoization settings saved by
save-and-clear-memoization-settings.

Related topics other than immediate subtopics:

SAVE-AND-CLEAR-MEMOIZATION-SETTINGS    save and remove the current memoization settings

For background on memoization, see MEMOIZE.

     General Form:
     (save-and-clear-memoization-settings)

Calls of this macro achieve two changes.  The first copies the current
memoization settings into an ACL2 table, and the second unmemoizes all
functions that were memoized by calls of memoize.  Also see
RESTORE-MEMOIZATION-SETTINGS.

Related topics other than immediate subtopics:

SET-BODY    set the definition body

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

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

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

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

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

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

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

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

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

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

The default setting is nil.

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

TABLE    user-managed tables

     Examples:
     (table tests 1 '(...))                ; set contents of tests[1] to '(...)
     (table tests 25)                      ; get contents of tests[25]
     (table tests)                         ; return table tests as an alist
     (table tests nil nil :clear)          ; clear table tests
     (table tests nil '((foo . 7)) :clear) ; set table tests to ((foo . 7))
     (table tests nil nil :guard)          ; fetch the table guard
     (table tests nil nil :guard term)     ; set the table guard

     * Menu:

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

     General Form:
     (table table-name key-term value-term op term)

where table-name is a symbol that is the name of a (possibly new)
table, key-term and value-term, if present, are arbitrary terms
involving (at most) the single variable world, op, if present, is one
of the table operations below, and term, if present, is a term.  Table
returns an ACL2 "error triple" (see PROGRAMMING-WITH-STATE).
The effect of table on state depends on op and how many arguments are
presented.  Some invocations actually have no effect on the ACL2 world
and hence an invocation of table is not always an "event".  We explain
below, after giving some background information.

Important Note: The table forms above are calls of a macro that expand
to involve the special variable state.  This will prevent you from
accessing a table from within a hint or theory where you do not have the
state variable.  However, the form

     (table-alist 'tests world)

returns the alist representation of the table named test in the given
world.  Often you have access to world.

The ACL2 system provides "tables" by which the user can associate one
object with another.  Tables are in essence just conventional
association lists -- lists of pairs -- but the ACL2 environment
provides a means of storing these lists in the "ACL2 world" of the
current state.  The ACL2 user could accomplish the same ends by using
ACL2 "global variables;" however, limitations on global variable names
are imposed to ensure ACL2's soundness.  By convention, no table is
important to ACL2's soundness, even though some features of the system
use tables, and the user is invited to make free use of tables.
Because tables are stored in the ACL2 world they are restored by
include-book and undone by :ubt.  Many users of Nqthm requested a
facility by which user data could be saved in Nqthm "lib files" and
tables are ACL2's answer to that request.

Abstractly, each table is an association list mapping "keys" to
"values." In addition, each table has a ":guard," which is a term that
must be true of any key and value used.  By setting the :guard on a
table you may enforce an invariant on the objects in the table, e.g.,
that all keys are positive integers and all values are symbols.  Each
table has a "name," which must be a symbol.  Given a table name, the
following operations can be performed on the table.

:put -- associate a value with a key (possibly changing the value
currently associated with that key).

:get -- retrieve the value associated with a key (or nil if no value
has been associated with that key).

:alist -- return an alist showing all keys and non-nil values in the
table.

:clear -- clear the table (so that every value is nil), or if val is
supplied then set table to that value (which must be an alist).

:guard -- fetch or set the :guard of the table.

When the operations above suggest that the table or its :guard are
modified, what is actually meant is that the current state is redefined
so that in it, the affected table name has the appropriate properties.
in such cases, the table form is an event (see EVENTS).  In the
:put case, if the key is already in the table and associated with the
proposed value, then the table event is redundant (see
REDUNDANT-EVENTS).

Table forms are commonly typed by the user while interacting with the
system.  :Put and :get forms are especially common.  Therefore, we have
adopted a positional syntax that is intended to be convenient for most
applications.  Essentially, some operations admit a "short form" of
invocation.

     (table name key-term value-term :put)   ; long form
     (table name key-term value-term)        ; short form

evaluates the key- and value-terms, obtaining two objects that we call
key and value, checks that the key and value satisfy the :guard on the
named table and then "modifies" the named table so that the value
associated with key is value.  When used like this, table is actually
an event in the sense that it changes the ACL2 world.  In general, the
forms evaluated to obtain the key and value may involve the variable
world, which is bound to the then-current world during the evaluation
of the forms.  However, in the special case that the table in question
is named acl2-defaults-table, the key and value terms may not contain
any variables.  Essentially, the keys and values used in events setting
the acl2-defaults-table must be explicitly given constants.  See
ACL2-DEFAULTS-TABLE.

     (table name key-term nil :get)          ; long form
     (table name key-term)                   ; short form

evaluates the key-term (see note below), obtaining an object, key, and
returns the value associated with key in the named table (or, nil if
there is no value associated with key).  When used like this, table is
not an event; the value is simply returned.

     (table name nil nil :alist)             ; long form
     (table name)                            ; short form

returns an alist representing the named table; for every key in the
table with a non-nil associated value, the alist pairs the key and its
value.  The order in which the keys are presented is unspecified.  When
used like this, table is not an event; the alist is simply returned.

     (table name nil val :clear)

sets the named table to the alist val, making the checks that :put
makes for each key and value of val.  When used like this, table is an
event because it changes the ACL2 world.

     (table name nil nil :guard)

returns the translated form of the guard of the named table.

     (table name nil nil :guard term)

Provided the named table is empty and has not yet been assigned a
:guard and term (which is not evaluated) is a term that mentions at
most the variables key, val and world, this event sets the :guard of
the named table to term.  Whenever a subsequent :put occurs, term will
be evaluated with key bound to the key argument of the :put, val bound
to the val argument of the :put, and world bound to the then current
world.  An error will be caused by the :put if the result of the
evaluation is nil.

Note that it is not allowed to change the :guard on a table once it has
been explicitly set.  Before the :guard is explicitly set, it is
effectively just t.  After it is set it can be changed only by undoing
the event that set it.  The purpose of this restriction is to prevent
the user from changing the :guards on tables provided by other people
or the system.

The intuition behind the :guard mechanism on tables is to enforce
invariants on the keys and values in a table, so that the values, say,
can be used without run-time checking.  But if the :guard of a table is
sensitive to the ACL2 world, it may be possible to cause some value in
the table to cease satisfying the :guard without doing any operations
on the table.  Consider for example the :guard "no value in this table
is the name of an event." As described, that is enforced each time a
value is stored.  Thus, 'bang can be :put in the table provided there
is no event named bang.  But once it is in the table, there is nothing
to prevent the user from defining bang as a function, causing the table
to contain a value that could not be :put there anymore.  Observe that
not all state-sensitive :guards suffer this problem.  The :guard "every
value is an event name" remains invariant, courtesy of the fact that
undoing back through an event name in the table would necessarily undo
the :put of the name into the table.

Table was designed primarily for convenient top-level use.  Tables are
not especially efficient.  Each table is represented by an alist stored
on the property list of the table name.  :Get is just a getprop and
assoc-equal.  :Put does a getprop to the get the table alist, a
put-assoc-equal to record the new association, and a putprop to store
the new table alist -- plus the overhead associated with :guards and
undoable events, and checking (for redundancy) if the key is already
bound to its proposed value.  Note that there are never duplicate keys
in the resulting alist; in particular, when the operation :clear is
used to install new alist, duplicate keys are removed from that alist.

A table name may be any symbol whatsoever.  Symbols already in use as
function or theorem names, for example, may be used as table names.
Symbols in use only as table names may be defined with defun, etc.
Because there are no restrictions on the user's choice of table names,
table names are not included among the logical names.  Thus, :pe name
will never display a table event (for a logical name other than :here).
Either :pe name will display a "normal" event such as (defun name ...)
or (defthm name ...) or else :pe name will cause an error indicating
that name is not a logical name.  This happens even if name is in use
as a table name.  Similarly, we do not permit table names to have
documentation strings, since the same name might already have a
documentation string.  If you want to associate a documentation string
with a table name that is being used no other way, define the name as a
label and use the :doc feature of deflabel (see DEFLABEL); also
see DEFDOC.

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

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

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

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

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

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

Related topics other than immediate subtopics:

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

       (table number-table 'data nil)

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

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

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

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

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

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

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

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

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

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

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

THEORY-INVARIANT    user-specified invariants on theories

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

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

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

where:

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

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

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

Theory-invariant is an event that adds to or modifies the table of
user-supplied theory invariants that are checked each time a theory
expression is evaluated.

The theory invariant mechanism is provided via a table (see
TABLE) named theory-invariant-table.  In fact, the theory-invariant
"event" is just a macro that expands into a use of the table event.
More general access to the theory-invariant table is provided by table
itself.  For example, the table can be inspected or cleared with table;
you can clear an individual theory invariant by setting the invariant
to t, or eliminate all theory invariants with the command (table
theory-invariant-table nil nil :clear).

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

Theory invariants are particularly useful in the context of large rule
sets intended for re-use.  Such sets often contain conflicting rules,
e.g., rules that are to be enabled when certain function symbols are
disabled, rules that rewrite in opposite directions and thus loop if
simultaneously enabled, groups of rules which should be enabled in
concert, etc.  The developer of such rule sets understands these
restrictions and probably documents them.  The theory invariant
mechanism allows the developer to codify his restrictions so that the
user is alerted when they are violated.

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

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

would subsequently cause an error any time the current theory contained
both of the two runes shown.  Of course, incompatible is just defined as
a macro.  Its definition may be inspected with :pe incompatible.

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

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

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

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

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

UNMEMOIZE    turn off memoization for the specified function

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

     * Menu:

     Related topics other than immediate subtopics:
     * HONS-AND-MEMOIZATION:: hash cons, function memoization, and applicative hash tables

     General Form:
     (unmemoize fn)

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

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

To remove the effects of all memoize events, evaluate:
(clear-memo-table).  To save and restore memoization, see
SAVE-AND-CLEAR-MEMOIZATION-SETTINGS and see
RESTORE-MEMOIZATION-SETTINGS.

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

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

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

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

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

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

VERIFY-GUARDS    verify the guards of a function

See GUARD for a general discussion of guards.

Before discussing the verify-guards event, we first discuss guard
verification, which can take place at definition time or, later, using
verify-guards.  Typically, guard verification takes place at definition
time if a guard (or type, or stobjs) has been supplied explicitly unless
:verify-guards nil has been specified; see DEFUN and see
XARGS, and see SET-VERIFY-GUARDS-EAGERNESS for how to change
this default.  The point of guard verification is to ensure that during
evaluation of an expression without free variables, no guard violation
takes place.

Guard verification is intended to guarantee that for any call of a given
function, if its guard holds for that call then the guard will hold for
every function call in the body of that function.  Moreover, in order to
avoid guard violations during evaluation of the function's guard itself,
guard verification also is intended to guarantee that the guards are
satisfied for all calls in the guard itself.  Consider the following
simple example.

     (defun f (x)
       (declare (xargs :guard (and (consp x)
                                   (integerp (car x)))))
       (if (rationalp (cdr x))
           (+ (car x) (cdr x))
         17))

If you evaluate (f t), for example, in the top-level loop, you will (by
default) get a guard error.  The point of guard verification is to
guarantee the absence of guard errors, and we start by using this
example to illustrate the proof obligations that guarantee such absence.

The body of the above definition has the following function calls,
where the first is the entire body.

       (if (rationalp (cdr x))
           (< (car x) (cdr x))
         17)
       (rationalp (cdr x)) ; the test of the top-level IF call
       (cdr x)             ; from (rationalp (cdr x))
       (< (car x) (cdr x)) ; the true branch of the top-level IF call
       (car x)             ; from (< (car x) (cdr x))
       (cdr x)             ; from (< (car x) (cdr x))

We thus see potentially six conditions to prove, one for each call.  The
guards of the function symbols of those calls are t for if and
rationalp, (or (consp x) (equal x nil)) for both (car x) and (cdr x),
and finally that both arguments are rationals for <.  Moreover, we can
take advantage of "contextual assumptions": the if-test conditions and
the top-level :guard.  Thus, for verify-guards the proof obligation
from the body of f is as follows.

     (implies
      (and (consp x) (integerp (car x))) ; from the :guard
      (and t ; from the top-level IF call
           t ; from (rationalp (cdr x))
           (or (consp x) (equal x nil)) ; from the first (cdr x)
           (implies
            (rationalp (cdr x)) ; IF-test for calls in the true branch
            (and (or (consp x) (equal x nil)) ; from (car x)
                 (or (consp x) (equal x nil)) ; from the second (cdr x)
                 (and (rationalp (car x)) (rationalp (cdr x))) ; from the < call
                 ))))

But the :guard itself generates a similar sort of proof obligation.
Note that the guard (and (consp x) (integerp (car x))) is really an
abbreviation (i.e. via the macro AND) for the term (if (consp x)
(integerp (car x)) nil).  The guard proof obligation for the guard
itself is thus as follows.

     (and t ; from (consp x)
          (implies (consp x)
                   (and t         ; from (integerp (car x)) ;
                        (consp x) ; from (car x) ;
                        )))

All of the above proof obligations are indeed theorems, and guard
verification succeeds for the above definition of f.

The example above illustrates the general procedure for generating the
guard proof obligation.  Each function call is considered in the body
or guard of the function, and it is required that the guard is met for
that call, under certain "contextual assumptions", which are as
follows.  In the case of the body of the named function, it is assumed
that the guard holds for that function on its formal parameters.  And
in both cases -- the body of the named function and also its guard --
the governing tests from superior calls of IF are also assumed.

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

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

We turn now to the verify-guards event as a way of verifying the guards
for a function or theorem.

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

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

In the General Form above, name is the name of a :logic function (see
DEFUN-MODE) or of a theorem or axiom.  In the most common case
name is the name of a function that has not yet had its guards
verified, each subroutine of which has had its guards verified.  The
values hints, otf-flg, and guard-debug are as described in the
corresponding documentation entries; and doc-string, if supplied, is a
string *not* beginning with ":Doc-Section".  The four keyword arguments
above are all optional.  To admit this event, the conjunction of the
guard proof obligations must be proved.  If that proof is successful,
name is considered to have had its guards verified.

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

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

If name is a theorem or axiom name, verify-guards verifies the guards
of the associated formula.  When a theorem has had its guards verified
then you know that the theorem will evaluate to non-nil in all Common
Lisps, without causing a runtime error (other than possibly a resource
error).  In particular, you know that the theorem's validity does not
depend upon ACL2's arbitrary completion of the domains of partial
Common Lisp functions.

For example, if app is defined as

     (defun app (x y)
       (declare (xargs :guard (true-listp x)))
       (if (endp x)
           y
           (cons (car x) (app (cdr x) y))))

then we can verify the guards of app and we can prove the theorem:

     (defthm assoc-of-app
       (equal (app (app a b) c) (app a (app b c))))

However, if you go into almost any Common Lisp in which app is defined
as shown and evaluate

     (equal (app (app 1 2) 3) (app 1 (app 2 3)))

we get an error or, perhaps, something worse like nil!  How can this
happen since the formula is an instance of a theorem?  It is supposed
to be true!

It happens because the theorem exploits the fact that ACL2 has completed
the domains of the partially defined Common Lisp functions like car and
cdr, defining them to be nil on all non-conses.  The formula above
violates the guards on app.  It is therefore "unreasonable" to expect
it to be valid in Common Lisp.

But the following formula is valid in Common Lisp:

     (if (and (true-listp a)
              (true-listp b))
         (equal (app (app a b) c) (app a (app b c)))
         t)

That is, no matter what the values of a, b and c the formula above
evaluates to t in all Common Lisps (unless the Lisp engine runs out of
memory or stack computing it).  Furthermore the above formula is a
theorem:

     (defthm guarded-assoc-of-app
       (if (and (true-listp a)
                (true-listp b))
           (equal (app (app a b) c) (app a (app b c)))
           t))

This formula, guarded-assoc-of-app, is very easy to prove from
assoc-of-app.  So why prove it?  The interesting thing about
guarded-assoc-of-app is that we can verify the guards of the formula.
That is, (verify-guards guarded-assoc-of-app) succeeds.  Note that it
has to prove that if a and b are true lists then so is (app a b) to
establish that the guard on the outermost app on the left is satisfied.
By verifying the guards of the theorem we know it will evaluate to true
in all Common Lisps.  Put another way, we know that the validity of the
formula does not depend on ACL2's completion of the partial functions
or that the formula is "well-typed."

One last complication:  The careful reader might have thought we could
state guarded-assoc-of-app as

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

rather than using the if form of the theorem.  We cannot!  The reason
is technical:  implies is defined as a function in ACL2.  When it is
called, both arguments are evaluated and then the obvious truth table
is checked.  That is, implies is not "lazy."  Hence, when we write the
guarded theorem in the implies form we have to prove the guards on the
conclusion without knowing that the hypothesis is true.  It would have
been better had we defined implies as a macro that expanded to the if
form, making it lazy.  But we did not and after we introduced guards we
did not want to make such a basic change.

Recall however that verify-guards is almost always used to verify the
guards on a function definition rather than a theorem.  We now return
to that discussion.

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

Verify-guards must often be used when the value of a recursive call of
a defined function is given as an argument to a subroutine that is
guarded.  An example of such a situation is given below.  Suppose app
(read "append") has a guard requiring its first argument to be a
true-listp.  Consider

     (defun rev (x)
       (declare (xargs :guard (true-listp x)))
       (cond ((endp x) nil)
             (t (app (rev (cdr x)) (list (car x))))))

Observe that the value of a recursive call of rev is being passed into
a guarded subroutine, app.  In order to verify the guards of this
definition we must show that (rev (cdr x)) produces a true-listp, since
that is what the guard of app requires.  How do we know that (rev (cdr
x)) is a true-listp?  The most elegant argument is a two-step one,
appealing to the following two lemmas: (1) When x is a true-listp, (cdr
x) is a true-listp.  (2) When z is a true-listp, (rev z) is a
true-listp.  But the second lemma is a generalized property of rev, the
function we are defining.  This property could not be stated before rev
is defined and so is not known to the theorem prover when rev is
defined.

Therefore, we might break the admission of rev into three steps: define
rev without addressing its guard verification, prove some general
properties about rev, and then verify the guards.  This can be done as
follows:

     (defun rev (x)
       (declare (xargs :guard (true-listp x)
                       :verify-guards nil))    ; Note this additional xarg.
       (cond ((endp x) nil)
             (t (app (rev (cdr x)) (list (car x))))))

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

     (verify-guards rev)

The ACL2 system can actually admit the original definition of rev,
verifying the guards as part of the defun event.  The reason is that,
in this particular case, the system's heuristics just happen to hit
upon the lemma true-listp-rev.  But in many more complicated functions
it is necessary for the user to formulate the inductively provable
properties before guard verification is attempted.

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

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

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

     Example:
     (verify-termination fact)

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

where fn and the fni are function symbols having :program mode (see
DEFUN-MODE) and all of the dcls are either declare forms or
documentation strings.  The first form above is an abbreviation for

     (verify-termination (fn dcl ... dcl))

so we limit our discussion to the second form.  Each of the fni must be
in the same clique of mutually recursively defined functions, but not
every function in the clique need be among the fni.

Verify-termination attempts to establish the admissibility of the fni.
Verify-termination retrieves their definitions, creates modified
definitions using the dcls supplied above, and resubmits these
definitions.  You could avoid using verify-termination by typing the new
definitions yourself.  So in that sense, verify-termination adds no new
functionality.  But if you have prototyped your system in :program mode
and tested it, you can use verify-termination to resubmit your
definitions and change their defun-modes to :logic, addings hints
without having to retype or recopy the code.

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

For example, suppose that fact was introduced with:

     (defun fact (n)
       (declare (type integer n)
                (xargs :mode :program))
       (if (zp n) 1 (* n (fact (1- n))))).

Suppose later we do (verify-termination fact).  Then the following
definition is submitted.

     (defun fact (n)
       (declare (type integer n))
       (if (zp n) 1 (* n (fact (1- n))))).

Observe that this is the same definition as the original one, except
the old specification of the :mode has been deleted so that the
defun-mode now defaults to :logic.  Although the termination proof
succeeds, ACL2 also tries to verify the guard, because we have
(implicitly) provided a guard, namely (integerp n), for this function.
(See GUARD for a general discussion of guards, and see
TYPE-SPEC for a discussion of how type declarations are used in
guards.)  Unfortunately, the guard verification fails, because the
subterm (zp n) requires that n be nonnegative, as can be seen by
invoking :args zp.  (For a discussion of termination issues relating to
recursion on the naturals, see ZERO-TEST-IDIOMS.)  So we might
be tempted to submit the following:

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

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

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

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

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

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

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

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

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

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

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

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

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

_A Quick Introduction to Forward Chaining Reports_

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

     (reset-fc-reporting)

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

     (set-fc-criteria t)

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

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

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

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

After the proof attempt has terminated, you can execute:

     (fc-report k)

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

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

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

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

     (set-fc-criteria nil)

_How To Read FC Reports_

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

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

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

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

_How to Read Activation Reports_

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

     Activations: (_act1_ _act2_ ...)

Each _acti_ is of the form:

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

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

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

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

If outcome-part1 is SUCCESS then _inst-term_ is the instantiated
conclusion produced by the rule.  _Outcome-part2_ is APPROVED if the
instantiated conclusion was acceptable to our heuristics designed to
prevent looping and not already known in the evolving context.
_Outcome-part2_ is REJECTED if the instantiated conclusion was not
approved by our heuristics.  _Outcome-part2_ is REDUNDANT if the
instantiated conclusion was approved by the heuristics but already
known true in the current evolving context.  If APPROVED, the truth of
the instantiated conclusion is added to the evolving context.
Otherwise, it is not.

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

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

_Specifying the Tracking Criteria_

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Observe that the triple

     (t t t)

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

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

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

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

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

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

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

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

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

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

     Example: (fc-report 15)

     General Form: (fc-report k)

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

See FORWARD-CHAINING-REPORTS for details.

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

     Example:  (reset-fc-reporting)

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

See FORWARD-CHAINING-REPORTS for details.

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

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

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

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

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

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

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

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

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

See FORWARD-CHAINING-REPORTS for details.

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

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

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

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

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

See FORWARD-CHAINING-REPORTS for details.

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

     Example:  (show-fc-criteria)

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

See FORWARD-CHAINING-REPORTS for details.

HISTORY    functions that display or change history

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

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

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

OOPS    undo a :u or :ubt

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

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

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

                  *
                w0
              /    \
            w3      w1
              \    /
                w2

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

                w0
              /    \
           *w0'     w1
              \    /
                w2

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

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

                  *
                w0
              /    \
            w0'     w1
              \    /
                w2

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

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

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

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

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

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

PBT    print the commands back through a command descriptor

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

See COMMAND-DESCRIPTOR.

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

PC    print the command described by a command descriptor

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

See COMMAND-DESCRIPTOR.

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

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

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

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

For example, :pcs 52 54 will print something like

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

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

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

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

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

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

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

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

Thus, the display

      PLd     52 (DEFUN FOO (X) X)

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

The display

      P d     52 (DEFUN FOO (X) X)

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

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

      L d     52 (DEFUN FOO (X) X)

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

Finally, for the experimental HONS version only (see
HONS-AND-MEMOIZATION), a fourth character is printed, indicating
whether functions are memoized.  A symbol may be memoized if it is a
function symbol that is not constrained (i.e., introduced by defchoose
or in the signature of an encapsulate event).  If the command
introduces no symbol that may be memoized, then a space is printed.
Otherwise, if every memoizable symbol is memoized, an "M" is printed.
Otherwise, an "m" is printed.

PCB    print the command block described by a command descriptor

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

See COMMAND-DESCRIPTOR.

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

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

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

See COMMAND-DESCRIPTOR.

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

PCS    print the sequence of commands between two command descriptors

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

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

PE    print the events named by a logical name

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

See LOGICAL-NAME.

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

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

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

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

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

PE!    deprecated (see PE)

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

PF    print the formula corresponding to the given name

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

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

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

PL    print the rules for the given name or term

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

Also see PL2, which restricts output to rules that you specify
for a given term.

Pl takes one argument, which should be a symbol or a term.

First suppose that the argument is a symbol.  Then it should be either a
function symbol or else a macro alias for a function symbol (see
MACRO-ALIASES-TABLE), which is treated as the corresponding function
symbol.  In this case :pl displays rules that apply to terms whose top
function symbol is the one specified, specifically, rules of class
:rewrite, :definition, :meta, :linear, :type-prescription,
:forward-chaining, :elim, and :induction.

Otherwise the argument should be a term (in user syntax, so that for
example macros are permitted).  In this case, :pl displays the
:rewrite, :definition, and :meta rules that rewrite the specified term,
followed by the applicable :type-prescription rules.  Each rule is
displayed with additional information, such as the hypotheses that
remain after applying some simple techniques to discharge them that are
likely to apply in any context.  Note that for :meta rules, only those
are displayed that meet two conditions: the application of the
metafunction returns a term different from the input term, and if there
is a hypothesis metafunction then it also returns a term.  (A subtlety:
In the case of extended metafunctions (see
EXTENDED-METAFUNCTIONS), a trivial metafunction context is used for
the application of the metafunction.)

Note that some rule classes are not handled by :pl.  In particular, if
you want to see all :clause-processor rules, issue the command
:print-clause-processor-rules, and for trusted clause-processors,
(table trusted-clause-processor-table); see CLAUSE-PROCESSOR and
see DEFINE-TRUSTED-CLAUSE-PROCESSOR.

PL2    print rule(s) for the given form

     Examples:
     :pl2 (+ x y) nil ; prints rules that apply to (+ x y)
     :pl2 (+ x y) foo ; prints rules named foo that apply to (+ x y)
     :pl2 (+ x y) (:rewrite foo) ; if the rule with rune (:rewrite foo) applies
                                 ;   to (+ x y), then print it
     :pl2 (+ x y) (:type-prescription foo)
                                 ; as above, but for the indicated
                                 ;   type-prescription rule

Pl2 takes two arguments.  The first is a term.  The second is either
nil or a "rule-id" that is either a symbol or a rune.  The result is to
print rules of class :rewrite, :definition, :meta, :linear, and
:type-prescription that apply to the given term.  Indeed, :pl2 prints
exactly what is printed by applying :pl to the first argument -- see
PL -- except that if the second argument is not nil then it is
used to filter the rules printed, as follows.

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

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

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

     Examples:

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

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

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

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

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

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

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

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

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

     Examples:

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

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

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

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

PUFF    replace a compound command by its immediate subevents

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

     General Form:
     :puff cd

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

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

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

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

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

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

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

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

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

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

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

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

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

PUFF*    replace a compound command by its subevents

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

     General Form:
     :puff* cd

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

TAU-DATA    to see what tau knows about a function symbol

     Examples:
     (tau-data binary-+)

     General Form:
     (tau-data fn)

This macro returns a list structure that indicates what facts about the
function symbol fn are known to the tau system.

The list structure should be self-explanatory given the following brief
comments.  The "index" of a function, when non-nil, means the function
is a monadic Boolean function treated by the tau system as a "type."

The "positive" and "negative implicants" are conjunctions that indicate
the "types" implied by the given one or its negation.

The "signatures" entry is a formula indicating all the known signatures.
If the signatures formula is T it means there are no known signatures.
(Signatures is the conjunction of all signature rules and the empty
conjunction is T.)

If you wish to see a long list of all the runes from which some tau
information has been gleaned, evaluate (global-val 'tau-runes (w
state)).

TAU-DATA-BASE    to see the tau data base as a (very large) object

     Example:
     (tau-data-base (w state))

This function returns a large list object that shows in a
human-readable way what the tau system knows about every function
symbol.  It is supposed to be self-explanatory.

If it is not, please contact the implementors and we will improve the
output or the documentation.

U    undo last command, without a query

     Example:
     :u

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

UBT    undo the commands back through a command descriptor

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

See COMMAND-DESCRIPTOR.

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

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

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

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

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

UBT!    undo commands, without a query or an error

     Example:
     :ubt! :x-4

The keyword command :ubt! is the same as :ubt, but with related queries
suppressed appropriately, and with a guarantee that it is "error-free."
More precisely, the value returned by :ubt!  will always be of the form
(mv nil val state).  :Oops will undo the last :ubt!.  See UBT,
see UBU, and see U.

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

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

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

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

See COMMAND-DESCRIPTOR.

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

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

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

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

UBU!    undo commands, without a query or an error

     Example:
     :ubu! :x-4

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

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

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

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

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

     ACL2_HONS=h

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

     make large DOC ACL2_HONS=h

of X with T, without duplication.

alist.

alists.

fast-alists.

produces normed, fast alists.

definition for hons-get.

the underlying Hons Space.

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

its arguments are normed.

its arguments are normed.

fast-alists.

tables that govern which ACL2 Objects are considered normed.

from an alist or to copy fast-alists.

that produces a normed result.

the current Hons Space.

objects (CCL Only).

returning alist itself or, in some cases, a new object equal to it.

certain sense.

sense of equal

Related topics other than immediate subtopics:

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

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

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

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

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

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

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

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

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

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

     ACL2 !>(time$ (fib 40))
     ; (EV-REC *RETURN-LAST-ARG3* ...) took
     ; 0.99 seconds realtime, 0.98 seconds runtime
     ; (1,296 bytes allocated).
     102334155
     ACL2 !>(memoize 'fib)

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

     Summary
     Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
     Rules: NIL
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      FIB
     ACL2 !>(time$ (fib 40))
     ; (EV-REC *RETURN-LAST-ARG3* ...) took
     ; 0.00 seconds realtime, 0.00 seconds runtime
     ; (2,864 bytes allocated).
     102334155
     ACL2 !>(time$ (fib 100))
     ; (EV-REC *RETURN-LAST-ARG3* ...) took
     ; 0.00 seconds realtime, 0.00 seconds runtime
     ; (7,024 bytes allocated).
     354224848179261915075
     ACL2 !>(unmemoize 'fib)

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

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

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

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

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

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

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

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

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

      For linux:

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

      For an x86 Macintosh running the Darwin OS:

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

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

        cd ccl
        svn update

      Whether obtaining a fresh CCL or just updating, finally issue these
      commands.

        ./lx86cl64
        (rebuild-ccl :full t)
        (quit)
        ./lx86cl64
        (rebuild-ccl :full t)
        (quit)

REFERENCES

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

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

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

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

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

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

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

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

CLEAR-HASH-TABLES    deprecated feature

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

CLEAR-MEMOIZE-STATISTICS    clears all profiling info displayed by (memoize-summary)

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

Logically, this function just returns nil.  It clears all profiling info
displayed by (memoize-summary)

CLEAR-MEMOIZE-TABLE    forget values remembered for the given function

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

This function returns its argument, fn, unchanged.  The values memoized
for fn are forgotten.

CLEAR-MEMOIZE-TABLES    forget values remembered for all the memoized functions

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

Clear-memoize-tables is a logical no-op.  All memoized values are
forgotten.  It returns nil, invoking clear-memoize-table for each
memoized function.

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

FAST-ALISTS    alists with hidden hash tables for faster execution

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

Performance Notes

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

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

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

FLUSH-HONS-GET-HASH-TABLE-LINK    deprecated feature

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

Deprecated.  Alias for fast-alist-free.

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

What might this involve?

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

Hash Table Creation

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

1.  As a size hint

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

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

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

2.  As an alist name

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

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

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

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

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

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

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

What might this involve?

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

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

HONS-NOTE    notes about HONS, especially pertaining to expensive resizing operations

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

Certain "Hons-Notes" are printed to the terminal to report
implementation-level information about the management of HONS
structures.  Some of these may be low-level and of interest mainly to
system developers.  But below we discuss what users can learn from a
particular hons-note, "ADDR-LIMIT reached".  In short: If you are
seeing a lot of such hons-notes, then you may be using a lot of memory.
(Maybe you can reduce that memory; for certain BDD operations, for
example (as defined in distributed books books/centaur/ubdds/),
variable ordering can make a big difference.)

By way of background:

     The ADDR-HT is the main hash table that lets us look up normed
     conses, i.e., honses.  It is an ordinary Common Lisp hash table,
     so when it starts to get too full the Lisp will grow it.  It can
     get really big.  (It has been seen to take more than 10 GB of
     memory just for the hash table's array, not to mention the actual
     conses!)

     Hons-Notes may be printed when the ADDR-HT is getting really full.
     This growth can be expensive and can lead to memory problems.
     Think about what it takes to resize a hash table:

     (1) allocate a new, bigger array
     (2) rehash elements, copying them into the new array
     (3) free the old array

     Until you reach step (3) and a garbage collection takes place, you
     have to have enough memory to have both the old and new arrays
     allocated.  If the old array was 10 GB and we want to allocate a
     new one that's 15 GB, this can get pretty bad.  Also, rehashing
     the elements is expensive time-wise when there are lots of
     elements.

     Since resizing a hash table is expensive, we want to avoid it.
     There's a hons-resize command for this.  You may want your books
     to start with something like the following.

            (value-triple (set-max-mem (* 30 (expt 2 30))))      ; 30 GB heap
            (value-triple (hons-resize :addr-ht #u_100_000_000)) ; 100M honses

     Basically, if you roughly know how many honses your book will
     need, you can just get them up front and then never to resize.

The Hons-Notes about "ADDR-LIMIT reached" are basically there to warn
you that the ADDR-HT is being resized.  This can help you realize that
your hons-resize command had too small of an ADDR-HT size, or might
suggest that your book should have a hons-resize command.  There are
also commands like (hons-summary) and, defined in distributed book
books/centaur/misc/memory-mgmt-logic.lisp, (hons-analyze-memory nil).
These can show you how many honses you currently have, how much space
they are taking, and that sort of thing.  (A nice trick is to call
hons-summary at the end of a book, to get an idea of how many honses
you should ask for in your hons-resize command).

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

General form:

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

Example:

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

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

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

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

You may wish to call this function for two reasons.

1.  Improving Performance by Resizing Up

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

2.  Reducing Memory Usage by Resizing Down

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

Advice for using hons-resize.

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

The alist argument need not be a fast alist.

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

MAKE-FAST-ALIST    (make-fast-alist alist) creates a fast-alist from the input alist,
returning alist itself or, in some cases, a new object equal to it.

Note: it is often better to use with-fast-alist; see the distributed
book books/centaur/misc/hons-extra.lisp for more information.

Logically, make-fast-alist is the identity function.

Under the hood, we construct and return an object that is equal to
alist and which is a fast alist.  If alist is already a fast alist,
almost no work is required: we simply return it unchanged.

When alist is not fast, we must minimally construct a hash table for its
bindings.  It is often possible to bind this new hash table to alist
itself.  But in certain cases when the alist keys are not normed, a new
alist must be constructed, also, and so we may return an equal but not
eq alist.  (In these cases, we still try to avoid at least some consing
by reusing the "longest normed tail" of the alist.)

MEMOIZE-SUMMARY    display all collected profiling and memoization table info

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

Logically, this function just returns nil, but it displays profiling and
memoization table information.  The profiling statistics may be cleared
with (clear-memoize-statistics).

MEMSUM    display all collected profiling and memoization info

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

This macro is an abbreviation for memoize-summary.  Logically, it just
returns nil.

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

The Meaning of Normed in Common Lisp.

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

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

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

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

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

Notes about Garbage Collection.

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

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

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

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

SLOW-ALIST-WARNING    warnings issued when fast-alists are used inefficiently

This documentation topic relates to the experimental extension of ACL2
supporting hash cons, fast alists, and memoization; see
HONS-AND-MEMOIZATION.

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

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

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

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

IO    input/output facilities in ACL2

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

Also see FILE-READING-EXAMPLE.

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

For a discussion of formatted printing, see FMT.

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

To redirect output to a file, see OUTPUT-TO-FILE.

Related topics other than immediate subtopics:

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

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

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

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

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

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

Common Lisp permits one to open a stream for several different kinds of
io, e.g. character or byte.  ACL2 permits an additional type called
"object".  In ACL2 an "io-type" is a keyword, either :character, :byte,
or :object.  When one opens a file, one specifies a type, which
determines the kind of io operations that can be done on the channel
returned.  The types :character and :byte are familiar.  Type :object
is an abstraction not found in Common Lisp.  An :object file is a file
of Lisp objects.  One uses read-object to read from :object files and
print-object$ (or print-object$-ser) to print to :object files.  (The
reading and printing are really done with the Common Lisp read and
print functions.  For those familiar with read, we note that the
recursive-p argument is nil.)  The function read-object-suppress is
logically the same as read-object except that read-object-suppress
throws away the second returned value, i.e. the value that would
normally be read, simply returning (mv eof state); under the hood,
read-object-suppress avoids errors, for example those caused by
encountering symbols in packages unknown to ACL2.

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

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

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

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

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

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

The macro get-output-stream-string$ returns the string accumulated into
the given channel.  By default, a call of this macro closes the supplied
output channel.  However, a third argument is optional (default t), and
if it evaluates to nil then the channel remains open.  The fourth
argument is an optional context, which generally evaluates to a symbol,
for error reporting.  The following example illustrates.

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

Also see PRINTING-TO-STRINGS for a discussion of formatted
printing functions such as fmt-to-string that do not take a channel or
state argument and return a string.

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

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

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

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

*STANDARD-CI*    an ACL2 character-based analogue of CLTL's *standard-input*

The value of the ACL2 constant *standard-ci* is an open character input
channel that is synonymous to Common Lisp's *standard-input*.

ACL2 character input from *standard-ci* is actually obtained by reading
characters from the stream named by Common Lisp's *standard-input*.
That is, by changing the setting of *standard-input* in raw Common Lisp
you can change the source from which ACL2 reads on the channel
*standard-ci*.  See *STANDARD-CO*.

*STANDARD-CO*    the ACL2 analogue of CLTL's *standard-output*

The value of the ACL2 constant *standard-co* is an open character
output channel that is synonymous to Common Lisp's *standard-output*.

ACL2 character output to *standard-co* will go to the stream named by
Common Lisp's *standard-output*.  That is, by changing the setting of
*standard-output* in raw Common Lisp you can change the actual
destination of ACL2 output on the channel named by *standard-co*.
Observe that this happens without changing the logical value of
*standard-co* (which is some channel symbol).  Changing the setting of
*standard-output* in raw Common Lisp essentially just changes the map
that relates ACL2 to the physical world of terminals, files, etc.

To see the value of this observation, consider the following.  Suppose
you write an ACL2 function which does character output to the constant
channel *standard-co*.  During testing you see that the output actually
goes to your terminal.  Can you use the function to output to a file?
Yes, if you are willing to do a little work in raw Common Lisp: open a
stream to the file in question, set *standard-output* to that stream,
call your ACL2 function, and then close the stream and restore
*standard-output* to its nominal value.  Similar observations can be
made about the two ACL2 input channels, *standard-oi* and
*standard-ci*, which are analogues of *standard-input*.

Another reason you might have for wanting to change the actual streams
associated with *standard-oi* and *standard-co* is to drive the ACL2
top-level loop, ld, on alternative input and output streams.  This end
can be accomplished easily within ACL2 by either calling ld on the
desired channels or file names or by resetting the ACL2 state global
variables 'standard-oi and 'standard-co which are used by ld.  See
STANDARD-OI and see STANDARD-CO.

*STANDARD-OI*    an ACL2 object-based analogue of CLTL's *standard-input*

The value of the ACL2 constant *standard-oi* is an open object input
channel that is synonymous to Common Lisp's *standard-input*.

ACL2 object input from *standard-oi* is actually obtained by reading
from the stream named by Common Lisp's *standard-input*.  That is, by
changing the setting of *standard-input* in raw Common Lisp you can
change the source from which ACL2 reads on the channel *standard-oi*.
See *STANDARD-CO*.

CHARACTER-ENCODING    how bytes are parsed into characters

When the Common Lisp reader comes across bytes in a file or at the
terminal, they are parsed into characters.  The simplest case is when
each byte that is read is a standard character (see
STANDARD-CHAR-P).  It is actually quite common that each byte that is
read corresponds to a single character.  The parsing of bytes into
characters is based on a _character encoding_, that is, a mapping that
associates one or more bytes with each legal character.

In order to help guarantee the portability of files (including books),
ACL2 installs a common character encoding for reading files, often
known as iso-8859-1 or latin-1.  For some host Lisps this character
encoding is also used for reading from the terminal; but, sadly, this
may not hold for all host Lisps, and may not even be possible for some
of them.

The use of the above encoding could in principle cause problems if one's
editor produces files using an encoding other than iso-8859-1, at least
if one uses non-standard characters.  In particular, the default Emacs
buffer encoding may be utf-8.  If your file has non-standard
characters, then in Emacs you can evaluate the form

     (setq save-buffer-coding-system 'iso-8859-1)

before saving the buffer into a file.  This will happen automatically
for users who load distributed file emacs/emacs-acl2.el into their Emacs
sessions.

For an example of character encodings in action, see the distributed
book books/misc/character-encoding-test.lisp.

EVISC-TUPLE    control suppression of details when printing

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

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

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

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

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

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

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

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

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

EXTERNAL-FORMAT    See CHARACTER-ENCODING.

IPRINT    See SET-IPRINT.

IPRINTING    See SET-IPRINT.

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

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

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

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

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

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

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

     (in-package "ACL2")

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

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

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

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

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

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

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

     (defthm bad nil :rule-classes nil)