This is documentation for ACL2 Version 3.3
Copyright (C) 2007  University of Texas at Austin

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

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

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

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

USING-COMPUTED-HINTS-6    Using the computed-hint-replacement feature

So far none of our computed hints have used the
:COMPUTED-HINT-REPLACEMENT feature.  We now illustrate that.

The :computed-hint-replacement feature can easily lead to loops.  So as
you experiment with the examples in this section and your own hints
using this feature, be ready to interrupt the theorem prover and abort!

A non-looping use of the :computed-hint-replacement feature would be a
hint like this:

     (if (certain-terms-present clause)
         '(:computed-hint-replacement t
           :in-theory (enable lemma25))
         '(:computed-hint-replacement t
           :in-theory (disable lemma25)))

In this hint, if certain terms are present in clause, as determined by
the function with the obvious name (here undefined), then this hint
enables lemma25 and otherwise disables it.  Lemma25 might be a very
expensive lemma, e.g., one that matches frequently and has an expensive
and rarely established hypothesis.  One might wish it enabled only
under certain conditions.  Recall that theories are inherited by
children.  So once lemma25 is enabled it "stays" enabled for the
children, until disabled; and vice versa.  If the
:computed-hint-replacement feature were not present and computed hints
were always deleted after they had been used, then lemma25 would be
left enabled (or disabled) for all the childen produced by the first
firing of the hint.  But with the arrangement here, every subgoal gets
a theory deemed suitable by the hint, and the hint persists.

Now we will set up a toy to allow us to play with computed hints to
understand them more deeply.  To follow the discussion it is best to
execute the following events.

     (defstub wrapper (x) t)
     (defaxiom wrapper-axiom (wrapper x) :rule-classes nil)

Now submit the following event and watch what happens.

     (thm (equal u v)
       :hints (`(:use (:instance wrapper-axiom (x a)))))

The theorem prover adds (wrapper a) to the goal and then abandons the
proof attempt because it cannot prove the subgoal.  Since the computed
hint is deleted upon use, the hint is not applied to the subgoal (i.e.,
the child of the goal).

What happens if we do the following?

     (thm (equal u v)
       :hints (`(:computed-hint-replacement t
                 :use (:instance wrapper-axiom (x a)))))

As one might expect, this loops forever: The hint is applied to the
child and adds the hypothesis again.  When the hint fires, nothing is
actually changed, since (wrapper a) is already in the subgoal.

So let's change the experiment a little.  Let's make the hint add the
hypothesis (wrapper p) where p is the first literal of the clause.
This is silly but it allows us to explore the behavior of computed
hints a little more.

     (thm (equal u v)
       :hints (`(:use (:instance wrapper-axiom (x ,(car clause))))))

So in this case, the theorem prover changes the goal to

     (IMPLIES (WRAPPER (EQUAL U V)) (EQUAL U V))

which then simplifies to

     (IMPLIES (WRAPPER NIL) (EQUAL U V))

because the concluding equality can be assumed false in the hypothesis
(e.g., think of the contrapositive version).  Nothing else happens
because the hint has been removed and so is not applicable to the child.

Now consider the following - and be ready to interrupt it and abort!

     (thm (equal u v)
       :hints (`(:computed-hint-replacement t
                 :use (:instance wrapper-axiom (x ,(car clause))))))

This time the hint is not removed and so is applied to the child.  So
from Goal we get

     Goal'
     (IMPLIES (WRAPPER (EQUAL U V))
              (EQUAL U V))

and then

     Goal''
     (IMPLIES (AND (WRAPPER (NOT (WRAPPER (EQUAL U V))))
                   (WRAPPER (EQUAL U V)))
              (EQUAL U V))

etc.

First, note that the hint is repeatedly applied to its children.  That
is because we wrote :computed-hint-replacement t.  But second, note
that Goal' is not even being simplified before Goal" is produced from
it.  If it were being simplified, the (equal u v)'s in the hypotheses
would be replaced by nil.  This is a feature.  It means after a
computed hint has fired, other hints are given a chance at the result,
even the hint itself unless it is removed from the list of hints.

As an exercise, let's arrange for the hint to stay around and be
applied indefinitely but with a simplification between each use of the
the hint.  To do this we need to pass information from one application
of the hint to the next, essentially to say "stay around but don't
fire."

First, we will define a function to use in the hint.  This is more than
a mere convenience; it allows the hint to "reproduce itself" in the
replacement.

     (defun wrapper-challenge (clause parity)
       (if parity
           `(:computed-hint-replacement ((wrapper-challenge clause nil))
             :use (:instance wrapper-axiom (x ,(car clause))))
           `(:computed-hint-replacement ((wrapper-challenge clause t)))))

Note that this function is not recursive, even though it uses its own
name.  That is because the occurrence of its name is in a quoted
constant.

Now consider the following.  What will it do?

     (thm (equal u v)
       :hints ((wrapper-challenge clause t)))

First, observe that this is a legal hint because it is a term that
mentions only the free variable CLAUSE.  When defining hint functions
you may sometimes think their only arguments are the four variables id,
clause, world, and stable-under-simplificationp.  That is not so.  But
in your hints you must call those functions so that those are the only
free variables.  Note also that the occurrence of clause inside the
:computed-hint-replacement is not an occurrence of the variable clause
but just a constant.  Just store this note away for a moment.  We'll
return to it momentarily.

Second, the basic cleverness of this hint is that every time it fires
it reproduces itself with the opposite parity.  When the parity is t it
actually changes the goal by adding a hypothesis.  When the parity is
nil it doesn't change the goal and so allows simplification to proceed
- but it swaps the parity back to t.  What you can see with this simple
toy is that we can use the computed hints to pass information from
parent to child.

Ok, so what happens when the event above is executed?  Try it.  You will
see that ACL2 applied the hint the first time.  It doesn't get around to
printing the output because an error is caused before it can print.
But here is a blow-by-blow description of what happens.  The hint is
evaluated on Goal with the clause ((equal u v)).  It produces a hint
exactly as though we had typed:

     ("Goal" :use (:instance wrapper-axiom (x (equal u v))))

which is applied to this goal. In addition, it produces the new hints
argument

     :hints ((wrapper-challenge clause nil)).

By applying the "Goal" hint we get the new subgoal

     Goal'
     (implies (wrapper (equal u v))
              (equal u v))

but this is not printed because, before printing it, the theorem prover
looks for hints to apply to it and finds

     (wrapper-challenge clause nil)

That is evaluated and produces a hint exactly as though we had typed:

     ("Goal'" )

and the new hints argument:

     :hints ((wrapper-challenge clause nil)).

But if you supply the hint ("Goal'" ), ACL2 will signal an error
because it does not allow you to specify an empty hint!

So the definition of wrapper-challenge above is almost correct but
fatally flawed.  We need a non-empty "no-op" hint.  One such hint is to
tell the system to expand a term that will always be expanded anyway.
So undo wrapper-challenge, redefine it, and try the proof again.  Now
remember the observation about clause that we asked you to "store"
above.  The new definition of wrapper-challenge illustrates what we
meant.  Note that the first formal parameter of wrapper-challenge,
below, is no longer named clause but is called cl instead.  But the
"call" of wrapper-challenge in the replacements is on clause.  This may
seem to violate the rule that a function definition cannot use
variables other than the formals.  But the occurrences of clause below
are not variables but constants in an object that will eventually be
treated as hint term.

     :ubt wrapper-challenge

     (defun wrapper-challenge (cl parity)
       (if parity
           `(:computed-hint-replacement ((wrapper-challenge clause nil))
             :use (:instance wrapper-axiom (x ,(car cl))))
           `(:computed-hint-replacement ((wrapper-challenge clause t))
             :expand ((atom zzz)))))

     (thm (equal u v)
       :hints ((wrapper-challenge clause t)))

This time, things go as you might have expected!  Goal' is produced and
simplified, to

     Goal''
     (implies (wrapper nil)
              (equal u v)).

Simplification gets a chance because when the new hint
(wrapper-challenge clause nil) is fired it does not change the goal.
But it does change the parity in the hints argument so that before
Goal" is simplified again, the hint fires and adds the hypothesis:

     Goal'''
     (IMPLIES (AND (WRAPPER (NOT (WRAPPER NIL)))
                   (WRAPPER NIL))
              (EQUAL U V)).

This simplifies, replacing the first (NOT (WRAPPER NIL)) by NIL, since
(WRAPPER NIL) is known to be true here.  Thus the goal simplifies to

     Goal'4'
     (IMPLIES (WRAPPER NIL) (EQUAL U V)).

The process repeats indefinitely.

So we succeeded in getting a hint to fire indefinitely but allow a full
simplification between rounds.

USING-COMPUTED-HINTS-7    Using the stable-under-simplificationp flag

A problem with the example in using-computed-hints-6 is that exactly
one simplification occurs between each (effective) firing of the hint.
Much more commonly we wish to fire a hint once a subgoal has become
stable under simplification.

A classic example of this is when we are dealing with an interpreter
for some state machine.  We typically do not want the "step" function
to open up on the symbolic representation of a state until that state
has been maximally simplified.  We will illustrate with a simple state
machine.

Let us start by defining the step function, stp, and the corresponding
run function that applies it a given number of times.

     (defun stp (s)
       (+ 1 s))

     (defun run (s n)
       (if (zp n)
           s
           (run (stp s) (- n 1))))

The step function here is trivial:  a state is just a number and the
step function increments it.  In this example we will not be interested
in the theorems we prove but in how we prove them.  The formula we will
focus on is

     (thm (equal (run s 7) xxx))

This is not a theorem, of course.  But we want to test our advice on
non-theorems because we do not want the advice to work only for proofs
that succeed.  (In the past, we gave advice about using computed hints
and that advice caused the theorem prover to run forever when given
formulas that it couldn't prove - but most of the time the system is
presented with formulas it cannot prove!)

Furthermore, without some kind of additional rules, the (run s 7)
expression in the conjecture above will not expand at all, because
ACL2's heuristics do not approve.

In fact, we do not want to take chances that run will be expanded - we
want to control its expansion completely.  Therefore, disable run.

     (in-theory (disable run))

Now, what do we want?  (That is always a good question to ask!)  We want
(run s 7) to expand "slowly."  In particular, we want it to expand
once, to (run (stp s) 6).  Then we want the stp to be expanded and
fully simplified before the run expression is expanded again.  That is,
we want to force the expansion of run whenever the goal is stable under
simplification.  This is sometimes called "staged simplification."

We can achieve staged simplification for any given function symbol by
defining the functions shown below and then using a simple computed
hint:

     (thm (equal (run s 7) xxx)
          :hints ((stage run)))

By inspecting how stage is defined you can see how to extend it, but we
explain as we go.  To experiment, you can just paste the definitions
(and defmacro) below into your ACL2 shell and then try the thm command.

First, define this pair of mutually recursive functions.
Find-first-call finds the first call of the function symbol fn in a
given term.

     (mutual-recursion
      (defun find-first-call (fn term)
      ; Find the first call of fn in term.
       (cond ((variablep term) nil)
             ((fquotep term) nil)
             ((equal (ffn-symb term) fn)
              term)
             (t (find-first-call-lst fn (fargs term)))))
      (defun find-first-call-lst (fn lst)
      ; Find the first call of fn in a list of terms.
       (cond ((endp lst) nil)
             (t (or (find-first-call fn (car lst))
                    (find-first-call-lst fn (cdr lst)))))))

We will arrange for the computed hint to generate an :EXPAND hint for
the first call of fn, whenever the goal becomes stable under
simplification.  If no call is found, the hint will do nothing.  To
make sure the hint will not loop indefinitely (for example, by forcing
fn to expand only to have the rewriter "fold" it back up again), we
will provide the hint with a bound that stops it after some number of
iterations.  Here is the basic function that creates the expand hint
and replaces itself to count down.

     (defun stage1 (fn max clause flg)
     ; If the clause is stable under simplification and there is a call of
     ; fn in it, expand it.  But don't do it more than max times.
      (let ((temp (and flg
                       (find-first-call-lst fn clause))))
        (if temp
            (if (zp max)
                (cw "~%~%HINT PROBLEM:  The maximum repetition count of ~
                     your STAGE hint been reached without eliminating ~
                     all of the calls of ~x0.  You could supply a larger ~
                     count with the optional second argument to STAGE ~
                     (which defaults to 100).  But think about what is ~
                     happening! Is each stage permanently eliminating a ~
                     call of ~x0?~%~%"
                    fn)
              `(:computed-hint-replacement
                 ((stage1 ',fn ,(- max 1)
                          clause
                          stable-under-simplificationp))
                :expand (,temp)))
          nil)))

Suppose that when stage1 is called, fn is the function we want to
expand, max is the maximum number of iterations of this expansion,
clause is the current goal clause, and flg is the value of the
stable-under-simplificationp flag.  Then if clause is stable and we can
find a call of fn in it, we ask whether max is exhausted.  If so, we
print an "error message" to the comment window with cw and return nil
(the value of cw).  That nil means the hint does nothing.  But if max
is not yet exhausted, we return a new hint.  As you can see above, the
hint replaces itself with another stage1 hint with the same fn and a
decremented max to be applied to the new clause and the then-current
value of stable-under-simplificationp.  The hint also contains an
:expand directive for the call of fn found.

Thus, if the computed hint was:

     (stage1 'run 5 clause stable-under-simplificationp)

and (run s 7) occurs in the clause, then it will generate

     (:computed-hint-replacement
       ((stage1 'run 4 clause stable-under-simplificationp))
      :expand ((run s 7)))

which will in turn replace the old stage1 hint with the new one and
will apply :expand ((run s 7)) to the current goal.

We can make this more convenient by defining the macro:

     (defmacro stage (fn &optional (max '100))
      `(stage1 ',fn ,max clause stable-under-simplificationp))

Note that the macro allows us to either provide the maximum bound or
let it default to 100.

Henceforth, we can type

     (thm (equal (run s 7) xxx)
          :hints ((stage run)))

to stage the opening of run up to 100 times, or we can write

     (thm (equal (run s 7) xxx)
          :hints ((stage run 5)))

to stage it only 5 times.  In the latter example, the system with print
a "error message" after the fifth expansion.

Note that if we executed

     (set-default-hints '((stage run)))

then we could attack all theorems (involving run) with staged
simplification (up to bound 100), without typing an explicit hint.

     (thm (equal (run s 7) xxx))

Using techniques similar to those above we have implemented "priority
phased simplification" and provided it as a book.  See
books/misc/priorities.lisp.  This is an idea suggested by Pete
Manolios, by which priorities may be assigned to rules and then the
simplifier simplifies each subgoal maximally under the rules of a given
priority before enabling the rules of the next priority level.  The
book above documents both how we implement it with computed hints and
how to use it.

Here is another example of using the stable-under-simplificationp flag
to delay certain actions.  It defines a default hint, see
DEFAULT-HINTS, which will enable non-linear-arithmetic on precisely
those goals which are stable-under-simplificationp.  It also uses the
HISTORY and PSPV variables to determine when toggling
non-linear-arithmetic is appropriate.  These variables are documented
only in the source code.  If you start using these variables
extensively, please contact the developers of ACL2 or Robert Krug
(rkrug@cs.utexas.edu) and let us know how we can help.

     (defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
       (cond (stable-under-simplificationp
              (if (not (access rewrite-constant
                               (access prove-spec-var pspv :rewrite-constant)
                               :nonlinearp))
                  '(:computed-hint-replacement t
                    :nonlinearp t)
                nil))
             ((access rewrite-constant
                      (access prove-spec-var pspv :rewrite-constant)
                      :nonlinearp)
              (if (not (equal (caar hist) 'SETTLED-DOWN-CLAUSE))
                  '(:computed-hint-replacement t
                    :nonlinearp nil)
                nil))
             (t
              nil)))

USING-COMPUTED-HINTS-8    Some Final Comments

None of the examples show the use of the variable WORLD, which is
allowed in computed hints.  There are some (undocumented) ACL2
utilities that might be useful in programming hints, but these
utilities need access to the ACL2 logical world (see WORLD).

A very useful fact to know is that (table-alist name world) returns an
alist representation of the current value of the table named name.

The ACL2 source code is littered with :program mode functions for
manipulating world.  In our source code, the world is usually bound a
variable named wrld; so searching our code for that name might be
helpful.

Using these utilities to look at the WORLD one can, for example,
determine whether a symbol is defined recursively or not, get the body
and formals of a defined function, or fetch the statement of a given
lemma.  Because these utilities are not yet documented, we do not
expect users to employ WORLD in computed hints.  But experts might and
it might lead to the formulation of a more convenient language for
computed hints.

None of our examples illustrated the 7 argument form of a computed hint,
(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX).  When
used, the variables HIST, PSPV, and CTX, are bound to the clause
history, the package of "special variables" governing the clause, and
the "error message context."  These variables are commonly used
throughout our source code but are, unfortunately, undocumented.
Again, we expect a few experts will find them useful in developing
computed hints.

If you start using computed hints extensively, please contact the
developers of ACL2 and let us know what you are doing with them and how
we can help.

VERSION    ACL2 Version Number

To determine the version number of your copy of ACL2, evaluate the form
(@ acl2-version).  The value will be a string.  For example,

     ACL2 !>(@ acl2-version)
     "ACL2 Version 3.3"

The part of the string after "ACL2 Version " is of the form x.y or
x.y.z, optionally followed by a succession of values in parentheses,
where x, y, and z are natural numbers.  If z is omitted then it is
implicitly 0.  We refer to X, y, and z as the "major", "minor", and
"incrl" fields, respectively.  The incrl field is used for incremental
releases.  The discussion just below assumes that incremental releases
are not employed at the user's site, i.e., the incrl fields are always
0.  We remove this assumption when we discuss incremental releases at
the end of this documenttation topic.

Books are considered certified only in the same version of ACL2 in
which the certification was done.  The certificate file records the
version number of the certifying ACL2 and include-book considers the
book uncertified if that does not match the current version number.
Thus, each time we release a new version of ACL2, previously certified
books should be recertified.

Note that there are over 150 constants in the system, most having to do
with the fact that ACL2 is coded in ACL2.  Many of these, for example
*common-lisp-specials-and-constants* and *acl2-exports*, may change
from version to version, and this can cause unsoundness.  For example,
the symbol 'set-difference-eq was added to *acl2-exports* in
Version_2.9, so we can certify a book in Version_2.8 containing the
following theorem, which is false in Version_2.9.

     (null (member 'set-difference-eq *acl2-exports*))

Therefore, we need to disallow inclusion of such a book in a Version_2.9
session, which otherwise would allow us to prove nil.  Furthermore, it
is possible that from one version of the system to another we might
change, say, the default values on some system function or otherwise
make "intentional" changes to the axioms.  It is even possible one
version of the system is discovered to be unsound and we release a new
version to correct our error.

Therefore we adopted the draconian policy that books are certified by a
given version of ACL2 and "must" be recertified to be used in other
versions.  We put "must" in quotes because in fact, ACL2 allows a book
that was certified in one ACL2 version to be included in a later
version, using include-book.  But ACL2 does not allow certify-book to
succeed when such an include-book is executed on its behalf.  Also, you
may experience undesirable behavior if you avoid recertification when
moving to a different version.  Hence we recommend that you stick to
the draconion policy of recertifying books when updating to a new ACL2
version.

The string (@ acl2-version) can contain implementation-specific
information in addition to the version number.  For example, in
Macintosh Common Lisp (MCL) (char-code #Newline) is 13, while as far as
we know, it is 10 in every other Common Lisp.  Our concern is that one
could certify a book in an MCL-based ACL2 with the theorem

     (equal (char-code #Newline) 13)

and then include this book in another Lisp and thereby prove nil.  So,
when a book is certified in an MCL-based ACL2, the book's certificate
mentions "MCL" in its version string.  Moreover, (@ acl2-version)
similarly mentions "MCL" when the ACL2 image has been built on top of
MCL.  Thus, an attempt to include a book in an MCL-based ACL2 that was
certified in a non-MCL-based ACL2, or vice-versa, will be treated like
an attempt to include an uncertified book.

_Incremental releases._

From time to time, so-called "incremental releases" of ACL2 are made
available.  These releases are thoroughly tested on at least two
platforms; "normal" releases, on the other hand, are thoroughly tested
on many more platforms (perhaps a dozen or so) and are accompanied by
updates to the ACL2 home page.  We provide incremental releases in
order to provide timely updates for ACL2 users who want them, without
imposing unnecessary burdens on either on the ACL2 implementors or on
ACL2 users who prefer to update less frequently.  The implementors
expect users to update their copies of ACL2 when normal releases are
made available, but not necessarily when incremental releases are made
available.

Incremental releases are accompanied by a bump in the incrl field of the
version field, while normal releases are accompanied by a bump in the
minor or (much less frequently) major field and zeroing out of the
incrl field.

Note that LOGICALLY SPEAKING, INCREMENTAL RELEASES ARE FULL-FLEDGE
RELEASES.  However, ACL2 users may wish to experiment with incremental
releases without recertifying all of their existing ACL2 books (see
CERTIFY-BOOK).  In order to learn how to avoid such
recertification, see SET-TAINTED-OKP.  The basic idea is that
if certification may depend on including books from an ACL2 version
with a different incrl field, the book's certificate is marked with a
"tainted" version, i.e., a version with "(tainted" as a substring.
Subsequent inclusion of any such book is restricted to sessions in
which the user explicitly invokes (set-tainted-okp t), which is
intended as an acknowledgment that including such a book may render the
ACL2 session unsound.

WHY-BRR    an explanation of why ACL2 has an explicit brr mode

Why isn't brr mode automatically disabled when there are no monitored
runes?  The reason is that the list of monitored runes is kept in a
wormhole state.

See WORMHOLE for more information on wormholes in general.  But
the fundamental property of the wormhole function is that it is a
logical no-op, a constant function that does not take state as an
argument.  When entering a wormhole, arbitrary information can be
passed in (including the external state).  That information is used to
construct a near copy of the external state and that "wormhole state"
is the one with respect to which interactions occur during breaks.  But
no information is carried by ACL2 out of a wormhole -- if that were
allowed wormholes would not be logical no-ops.  The only information
carried out of a wormhole is in the user's head.

Break-rewrite interacts with the user in a wormhole state because the
signature of the ACL2 rewrite function does not permit it to modify
state.  Hence, only wormhole interaction is possible.  (This has the
additional desirable property that the correctness of the rewriter does
not depend on what the user does during interactive breaks within it;
indeed, it is logically impossible for the user to affect the course of
rewrite.)

Now consider the list of monitored runes.  Is that kept in the external
state as a normal state global or is it kept in the wormhole state?  If
it is in the external state then it can be inspected within the
wormhole but not changed.  This is unacceptable; it is common to change
the monitored rules as the proof attempt progresses, installing
monitors when certain rules are about to be used in certain contexts.
Thus, the list of monitored runes must be kept as a wormhole variable.
Hence, its value cannot be determined outside the wormhole, where the
proof attempt is ongoing.

This raises another question: If the list of monitored runes is unknown
to the rewriter operating on the external state, how does the rewriter
know when to break?  The answer is simple: it breaks every time, for
every rune, if brr mode is enabled.  The wormhole is entered
(silently), computations are done within the wormhole state to
determine if the user wants to see the break, and if so, interactions
begin.  For unmonitored runes and runes with false break conditions,
the silent wormhole entry is followed by a silent wormhole exit and the
user perceives no break.

Thus, the penalty for running with brr mode enabled when there are no
monitored runes is high: a wormhole is entered on every application of
every rune and the user is simply unware of it.  The user who has
finally unmonitored all runes is therefore strongly advised to carry
this information out of the wormhole and to do :brr nil in the external
state when the next opportunity arises.

WORLD    ACL2 property lists and the ACL2 logical data base

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

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

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

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

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

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

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

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

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

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