This is documentation for ACL2 Version 4.3
Copyright (C) 2011  University of Texas at Austin

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

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

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

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

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

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

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

     (accumulated-persistence nil)            ; Deactivate.

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

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

Related topics other than immediate subtopics:

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

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

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

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

     ACL2 !>(accumulated-persistence t)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     (accumulated-persistence :all)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     ; Assume p0.  We want to prove p1.

     ; Key rule:
     p0 -> p1 = t

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

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

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

The following event captures the rules described above.

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

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

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

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

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

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

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

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

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

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

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

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

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

     :defun-mode

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

     :enforce-redundancy

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

     :ignore-doc-string-error

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

     :verify-guards-eagerness

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

     :compile-fns

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

     :measure-function

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

     :well-founded-relation

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

     :bogus-defun-hints-ok

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

     :bogus-mutual-recursion-ok

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

     :irrelevant-formals-ok

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

     :ignore-ok

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

     :inhibit-warnings

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

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

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

     :bdd-constructors

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

     :ttag

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

     :state-ok

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

     :backchain-limit

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

     :default-backchain-limit

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

     :step-limit

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

     :rewrite-stack-limit

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

     :let*-abstractionp

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

     :nu-rewriter-mode

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

     :case-split-limitations

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

     :include-book-dir-alist

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

     :match-free-default

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

     :match-free-override

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

     :match-free-override-nume

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

     :non-linearp

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

     :ruler-extenders

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

     :memoize-ideal-okp

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

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

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

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

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

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

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

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

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

     (in-package "ACL2")

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

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

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

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

     (in-package "ACL2")

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

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

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

The text

     (in-package "ACL2")

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

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

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

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

ACL2-HELP    the acl2-help mailing list

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

ASSIGN    assign to a global variable in state

     Examples:
     (assign x (expt 2 10))
     (assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))

     General Form:
     (assign symbol term)

where symbol is any symbol (with certain enforced exclusions to avoid
overwriting ACL2 system "globals") and term is any ACL2 term that could
be evaluated at the top-level.  Assign evaluates the term, stores the
result as the value of the given symbol in the global-table of state,
and returns the result.  (Note:  the actual implementation of the
storage of this value is much more efficient than this discussion of
the logic might suggest.)  Assign is a macro that effectively expands
to the more complicated but understandable:

     (pprogn (f-put-global 'symbol term state)
             (mv nil (f-get-global 'symbol state) state)).

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

BREAK$    cause an immediate Lisp break

ACL2 users are generally advised to avoid breaking into raw Lisp.
Advanced users may, on occasion, see the need to do so.  Evaluating
(break$) will have that effect.  (Exception: break$ is disabled after
evaluation of (set-debugger-enable :never); see
SET-DEBUGGER-ENABLE.)

CERTIFY-BOOK!    a variant of certify-book

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

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

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

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

CW-GSTACK    debug a rewriting loop or stack overflow

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

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

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

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

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

     (cw-gstack)

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

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

     (si::use-fast-links nil)

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

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

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

DMR    dynamically monitor rewrites and other prover activity

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

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

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

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

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

     Control-t 1

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

     (dmr-start)

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

     Control-t 2

At the ACL2 level you can disable monitoring as follows:

     (dmr-stop)

_Interpreting the dmr buffer display._

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

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

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

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

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

Now consider the next two lines:

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

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

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

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

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

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

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

     User-settable dmr variables

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

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

DYNAMICALLY-MONITOR-REWRITES    See DMR.

EXIT    quit entirely out of Lisp

Same as good-bye.

GOOD-BYE    quit entirely out of Lisp

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

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

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

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

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

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

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

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

GUARD-OBLIGATION    the guard proof obligation

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

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

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

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

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

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

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

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

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

IN-PACKAGE    select current package

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

     General Form:
     (in-package str)

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

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

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

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

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

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

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

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

See REBUILD for a variant of ld that skips proofs.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     ACL2 !>(foo 3)

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

     ACL2 !>

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

     ACL2 !>(print-gv)

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

     ACL2 !>

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

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

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

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

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

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

PROPS    print the ACL2 properties on a symbol

     Example:
     :props assoc-eq

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

PSO    show the most recently saved output

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

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

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

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

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

PSOG    show the most recently saved output in gag-mode

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

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

PSTACK    seeing what is the prover up to

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

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

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

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

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

clausify: splitting a goal into subgoals

ev-fncall: evaluating a function on explicit arguments

ev-fncall-meta:  evaluating a metafunction

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

induct: finding an induction scheme

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

process-assumptions:  creating forcing rounds

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

process-equational-polys:  deducing interesting equations

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

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

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

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

waterfall: top-level proof control

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

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

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

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

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

     Example:
     ACL2 !>:Q

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

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

QUIT    quit entirely out of Lisp

Same as good-bye.

REBUILD    a convenient way to reconstruct your old state

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

*Notes*:

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

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

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

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

     Examples:

     ACL2 !>(defpkg "FOO" nil)

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

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

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

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

SHARP-DOT-READER    read-time evaluation of constants

     Example:

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

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

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

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

SHOW-ACCUMULATED-PERSISTENCE    See ACCUMULATED-PERSISTENCE.

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

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

     General Form:
     (skip-proofs form)

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

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

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

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

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

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

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

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

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

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

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

THM    prove a theorem

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

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

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

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

TIME$    time an evaluation

Semantically, (time$ x ...) equals x.  However, its evaluation may
write timing output to the trace output (which is usually the
terminal), as explained further below.

     Examples:

     ; Basic examples:

     (time$ (foo 3 4))
     (time$ (mini-proveall))
     (defun bar (x) (time$ (f x)))

     ; Custom examples, which use a custom timing message rather than a built-in
     ; message from Lisp:

     ; Report only if real time is at least 1/2 second (two equivalent forms).
     (time$ (foo) :mintime 1/2)
     (time$ (foo) :real-mintime 1/2)

     ; Report only if allocation is at least 1000 bytes (and if the Lisp supports
     ; :minalloc).
     (time$ (foo) :minalloc 1000)

     ; Report only if real time is at least 1/2 second and (if the Lisp supports
     ; :minalloc) allocation is at least 931 bytes.
     (time$ (foo) :real-mintime 1/2 :minalloc 931)

     ; Print "Hello Moon, Goodbye World" instead of any timing data.
     (time$ (foo)
            :msg "Hello ~s0, ~s1 World."
            :args (list "Moon" "Goodbye"))

     ; Print default custom timing message (same as omitting :mintime 0):
     (time$ (foo)
            :mintime 0)

     ; Print supplied custom timing message.
     (let ((bar ...))
       (time$ (foo)
              :msg "The execution of ~xf took ~st seconds of real ~
                    time and ~sc seconds of run time (cpu time), and ~
                    allocated ~sa bytes.  In an unrelated note, bar ~
                    currently has the value ~x0.~%"
              :args (list bar)))

     General Forms:
     (time$ form)
     (time$ form ; arguments below are optional
            :real-mintime  <rational number of seconds>
            :run-mintime   <rational number of seconds>
            :minalloc      <number of bytes>
            :msg           <fmt string>
            :args          <list of arguments for msg>
            )
     ; Note: :real-mintime can be replaced by :mintime

where form is processed as usual except that the host Common Lisp times
its evaluation.

The simplest form is (time$ x), which will call the time utility in the
underlying Lisp, and will print a small default message.  If you want to
see a message printed by the host Lisp, use (time$ x :mintime nil)
instead, which may provide detailed, implementation-specific data such
as the amounts of time spent in user and system mode, the gc time, the
number of page faults encountered, and so on.  Of you can create a
custom message, configured using the :msg and :args parameters.  Time$
can also be made to report timing information only conditionally: the
:real-mintime (or equivalently, :mintime), :run-mintime, and :minalloc
arguments can be used to avoid reporting timing information for
computations that take a small amount of time (perhaps as might be
expected in ordinary cases), but to draw the user's attention to
computations that take longer or allocate more memory than expected.

We next document the keyword arguments in some detail.

     Keyword arguments :real-mintime (or :mintime) and :run-mintime can
     be used to specify a minimum time threshold for time reporting.
     That is, no timing information will be printed if the execution of
     form takes less than the specified number of seconds of real
     (total) time or run (cpu) time, respectively.  Note that rational
     numbers like 1/2 may be used to specify a fractional amount of
     seconds.  It is an error to specify both :real-mintime and its
     synonym, :mintime.

     Keyword argument :minalloc is not supported on all Lisps.  When it
     is not supported, it is ignored.  But on supported Lisps,
     :minalloc can be used to specify a minimum memory allocation
     threshold.  If form results in fewer than this many bytes being
     allocated, then no timing information will be reported.

     Keyword argument :msg, when provided, should be a string accepted
     by the fmt family of functions (see FMT), and it may refer
     to the elements of :args by their positions, just as for cw (see
     CW).

The following directives allow you to report timing information using
the :msg string.  The examples at the top of this documentation topic
illustrate the use of these directives.

     ~xf -- the form that was executed

     ~sa -- the amount of memory allocated, in bytes (in supported
     Lisps)

     ~st -- the real time taken, in seconds

     ~sc -- the run time (cpu time) taken, in seconds

We turn now to an example that illustrates how time$ can be called in
function bodies.  Consider the following definition of the Fibonacci
function, followed by the definition of a function that times k calls of
this function.

     (defun fib (n)
       (if (zp n)
           1
         (if (= n 1)
             1
           (+ (fib (- n 1))
              (fib (- n 2))))))

     (defun time-fib (k)
       (if (zp k)
           nil
         (prog2$
          (time$ (fib k)
                 :mintime 1/2
                 :msg "(fib ~x0) took ~st seconds, ~sa bytes allocated.~%"
                 :args (list k))
          (time-fib (1- k)))))

The following log shows a sample execution of the function defined just
above.

     ACL2 !>(time-fib 36)
     (fib 36) took 3.19 seconds, 1280 bytes allocated.
     (fib 35) took 1.97 seconds, 1280 bytes allocated.
     (fib 34) took 1.21 seconds, 1280 bytes allocated.
     (fib 33) took 0.75 seconds, 1280 bytes allocated.
     NIL
     ACL2 !>

Notes:

(1) Common Lisp specifies that the time utility prints to "trace
output", and time$ follows this convention.  Thus, if you have opened a
trace file (see OPEN-TRACE-FILE), then you can expect to find
the time$ output there.

(2) Unless the :msg argument is supplied, an explicit call of time$ in
the top-level loop will show that the form being timed is a call of the
ACL2 evaluator function ev-rec.  This is normal; the curious are
invited, at their own risk, to see RETURN-LAST for an
explanation.

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

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

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

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

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

TRANS    print the macroexpansion of a form

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

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

     => *

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

     => STATE

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

     => (MV $MEM * * STATE)

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

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

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

For more, see TERM.

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

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

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

TRANS1    print the one-step macroexpansion of a form

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

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

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

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

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

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

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

WALKABOUT    explore an ACL2 cons tree

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

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

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

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

The following example illustrates the commands described above.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     Examples:

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

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

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

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

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

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

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

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

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

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

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

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

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

     - Otherwise there is no limit.

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

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

     Examples:

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

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

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

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

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

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

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

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

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

If you find that the time limit appears to be implemented too loosely,
you are encouraged to email an example to the ACL2 implementors with
instructions on how to observe the undesirable behavior.  This
information can probably be used to improve ACL2 by the insertion of
more checks for expiration of the time limit.

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

PARALLELISM    experimental extension for evaluating forms in parallel

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

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

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

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

Related topics other than immediate subtopics:

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

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

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

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

COMPILING-ACL2P    compiling ACL2(p)

This documentation topic relates to the experimental extension of ACL2
supporting parallel evaluation and proof; see PARALLELISM.  See
PARALLEL and see PARALLELISM-TUTORIAL for an
introduction to parallel programming in ACL2 using primitives plet,
pargs, pand, por, and spec-mv-let.

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

     * CCL (OpenMCL)

     * Lispworks 6.0

     * SBCL with threads (feature :sb-thread)

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

     make ACL2_PAR=t LISP=ccl

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

     make large DOC ACL2_PAR=t LISP=ccl

EARLY-TERMINATION    early termination for pand and por.

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

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

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

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

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

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

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

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

GRANULARITY    limit the amount of parallelism

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

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

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

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

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

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

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

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

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

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

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

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

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

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

PAND    parallel, Boolean version of and

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

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

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

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

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

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

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

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

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

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

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

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

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

PARALLEL    evaluating forms in parallel

See PARALLELISM.

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

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

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

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

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

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

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

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

Calls of parallelism primitives made explicitly in the ACL2 top-level
loop, as opposed to inside function bodies, will never cause parallel
evaluation.  Such calls will either execute with serial evaluation or
will cause an error; see SET-PARALLEL-EVALUATION.

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

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

expands into:

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

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

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

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

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

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

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

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

PARALLELISM-BUILD    building an ACL2 executable with parallel evaluation enabled

See COMPILING-ACL2P.

PARALLELISM-PERFORMANCE    performance issues for parallel evaluation

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

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

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

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

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

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

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

Serial Fibonacci

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

Introducing Pargs

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

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

Introducing the Granularity Problem

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

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

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

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

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

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

Explicit Programming for the Granularity Problem

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

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

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

     (declare (granularity <form>))

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

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

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

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

Another Granularity Issue Related to Thread Limitations

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

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

Possible solutions may include reworking of algorithms (for example to
be tree-based rather than list-based) or using appropriate granularity
forms.  We hope that future implementations will allow thread
"re-deployment" in order to mitigate this problem.

Introducing Plet

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

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

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

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

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

Introducing Pand (By Way of a Tree Validation Example)

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

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

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

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

We also define a parallel version.

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

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

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

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

We can time our functions with the forms:

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

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

Demonstrating Early Termination with an Invalid Tree

Now observe this magic:

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

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

Granularity with Pand

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

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

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

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

Introducing Por

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

PARGS    parallel evaluation of arguments in a function call

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

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

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

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

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

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

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

PLET    parallel version of let

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

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

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

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

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

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

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

POR    parallel, Boolean version of or

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

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

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

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

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

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

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

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

SET-PARALLEL-EVALUATION    enabling parallel evaluation for four of the parallelism primitives

This documentation topic relates to the experimental extension of ACL2
supporting parallel evaluation and proof; see PARALLELISM.  See
PARALLEL and see PARALLELISM-TUTORIAL for an
introduction to parallel evaluation in ACL2 using parallelism
primitives pand, por, plet, and pargs.

     General Forms:
     (set-parallel-evaluation nil) ; default for images not built for parallelism
     (set-parallel-evaluation t)   ; default for images built for parallelism
     (set-parallel-evaluation :bogus-parallelism-ok)

Set-parallel-evaluation takes an argument that specifies the enabling or
disabling of parallel evaluation for the primitives pand, por, plet,
and pargs (but not spec-mv-let, whose parallel evaluation remains
enabled).  However, without using top-level, calls of parallelism
primitives made explicitly in the ACL2 top-level loop, as opposed to
inside function bodies, will never cause parallel evaluation; see
PARALLELISM-AT-THE-TOP-LEVEL.  Parallel evaluation is determined by
the value of the argument to set-parallel-evaluation, as follows.

Value t:
All parallelism primitives used in bodies of function definitions are
given the opportunity to execute in parallel.  However, the use of
parallelism primitives directly in the ACL2 top-level loop causes an
error.

Value :bogus-parallelism-ok:
Parallel evaluation is enabled, as for value t.  However, the use of
parallelism primitives directly in the ACL2 top-level loop does not
cause an error, but rather, simply results in serial evaluation for
these primitives.

Value nil:
All parallelism primitives will degrade to their serial equivalents,
include their calls made directly in the ACL2 top-level loop, which
does not cause an error.

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

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

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

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

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

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

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

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

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

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

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

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

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

While we support clause-processors, we do not support those that modify
state.  At this time, such an attempt to modify state may result in a
sub-optimal error message.

Computed hints are supported, as long as they don't modify state.
Computed hints may in principle read state, but support for such hints
may be incomplete.

Custom-keyword-hints are unsupported, though they may work on occasion.

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

The standard process for book certification will not use
waterfall-parallelism (see SET-WATERFALL-PARALLELISM), which is
disabled by default.  See BOOK-MAKEFILES, which explains that
acl2-customization files are ignored during that process unless
specified explicitly on the command line or in the environment.

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

Gag-mode isn't supported.  However, ACL2(p) also prints key checkpoints
(for example see INTRODUCTION-TO-KEY-CHECKPOINTS), but with a
notion of "key checkpoint" that does not take into account whether the
goal is later proved by induction.

The :brr utility is not supported.

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

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

When waterfall-parallelism is enabled (see
SET-WATERFALL-PARALLELISM), the use of set-inhibit-output-lst may not
fully inhibit proof output.

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

If the host Lisp is Lispworks, you may see messages about misaligned
conses.  The state of the system may be corrupted after such a message
has been printed.

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

See SET-WATERFALL-PARALLELISM.

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

See SET-WATERFALL-PRINTING.

PROGRAMMING    built-in ACL2 functions

The built-in ACL2 functions that one typically uses in writing programs
are listed below.  See their individual documentations.  We do not
bother to document some of the more obscure functions provided by ACL2
that do not correspond to functions of Common Lisp.

Related topics other than immediate subtopics:

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

*    multiplication macro

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

     (* x y 4 z)

represents the same term as

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

See BINARY-*.

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

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

+    addition macro

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

     (+ x y 4 z)

represents the same term as

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

See BINARY-+.

-    macro for subtraction and negation

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

Note that - represents subtraction as follows:

     (- x y)

represents the same term as

     (+ x (- y))

which is really

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

Also note that - represents arithmetic negation as follows:

     (- x)

expands to

     (unary-- x).

/    macro for division and reciprocal

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

Note that / represents division as follows:

     (/ x y)

represents the same term as

     (* x (/ y))

which is really

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

Also note that / represents reciprocal as follows:

     (/ x)

expands to

     (unary-/ x).

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

/=    test inequality of two numbers

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

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

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

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

1+    increment by 1

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

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

1-    decrement by 1

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

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

<    less-than

Completion Axiom (completion-of-<):

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

Guard for (< x y):

     (and (rationalp x) (rationalp y))

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

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

<=    less-than-or-equal test

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

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

=    test equality of two numbers

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

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

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

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

>    greater-than test

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

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

>=    greater-than-or-equal test

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

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

ABS    the absolute value of a real number

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

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

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

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

ACL2-NUMBERP    recognizer for numbers

(acl2-numberp x) is true if and only if x is a number, i.e., a rational
or complex rational number.

ACL2-USER    a package the ACL2 user may prefer

This package imports the standard Common Lisp symbols that ACL2
supports and also a few symbols from package "ACL2" that are commonly
used when interacting with ACL2.  You may prefer to select this as your
current package so as to avoid colliding with ACL2 system names.

This package imports the symbols listed in
*common-lisp-symbols-from-main-lisp-package*, which contains hundreds
of CLTL function and macro names including those supported by ACL2 such
as cons, car, and cdr.  It also imports the symbols in *acl2-exports*,
which contains a few symbols that are frequently used while interacting
with the ACL2 system, such as implies, defthm, and rewrite.  It imports
nothing else.

Thus, names such as alistp, member-equal, and type-set, which are
defined in the "ACL2" package are not present here.  If you find
yourself frequently colliding with names that are defined in "ACL2" you
might consider selecting "ACL2-USER" as your current package (see
IN-PACKAGE).  If you select "ACL2-USER" as the current package, you
may then simply type member-equal to refer to acl2-user::member-equal,
which you may define as you see fit.  Of course, should you desire to
refer to the "ACL2" version of member-equal, you will have to use the
"ACL2::" prefix, e.g., acl2::member-equal.

If, while using "ACL2-USER" as the current package, you find that there
are symbols from "ACL2" that you wish we had imported into it (because
they are frequently used in interaction), please bring those symbols to
our attention.  For example, should union-theories and universal-theory
be imported?  Except for stabilizing on the "frequently used" names
from "ACL2", we intend never to define a symbol whose
symbol-package-name is "ACL2-USER".

ACONS    constructor for association lists

(Acons key datum alist) equals the result of consing the pair (cons key
datum) to the front of the association list alist.

(Acons key datum alist) has a guard of (alistp alist).  Acons is a
Common Lisp function.  See any Common Lisp documentation for more
information.

ADD-TO-SET    add a symbol to a list

     General Forms:
     (add-to-set x lst)
     (add-to-set x lst :test 'eql)   ; same as above (eql as equality test)
     (add-to-set x lst :test 'eq)    ; same, but eq is equality test
     (add-to-set x lst :test 'equal) ; same, but equal is equality test

For a symbol x and an object lst, (add-to-set-eq x lst) is the result
of consing x on to the front of lst, unless x is already a member of
lst, in which case the result is lst. The optional keyword, :TEST, has
no effect logically, but provides the test (default eql) used for
comparing x with successive elements of lst.

The guard for a call of add-to-set depends on the test.  In all cases,
the second argument must satisfy true-listp.  If the test is eql, then
either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
add-to-set and its variants:

     (add-to-set-eq x lst) is equivalent to (add-to-set x lst :test
     'eq);

     (add-to-set-equal x lst) is equivalent to (add-to-set x lst :test
     'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function add-to-set-equal.

ADD-TO-SET-EQ    See ADD-TO-SET.

ADD-TO-SET-EQL    See ADD-TO-SET.

ADD-TO-SET-EQUAL    See ADD-TO-SET.

ALISTP    recognizer for association lists

(alistp x) is true if and only if x is a list of cons pairs.

(alistp x) has a guard of t.

ALLOCATE-FIXNUM-RANGE    set aside fixnums in GCL

(Allocate-fixnum-range fixnum-lo fixnum-hi) causes Gnu Common Lisp
(GCL) to create a persistent table for the integers between fixnum-lo
and fixnum-hi (both bounds inclusive). This table is referenced first
when any integer is boxed and the existing box in the table is used if
the integer is in bounds.  This can speed up GCL considerably by
avoiding wasteful fixnum boxing.  Here, fixnum-lo and fixnum-hi should
be fixnums, more specifically of type (signed-byte 30), with fixnum-lo
<= fixnum-hi.

When this function is executed in a Lisp implementation other than GCL,
it has no side effect.  This function always returns nil.

ALPHA-CHAR-P    recognizer for alphabetic characters

(Alpha-char-p x) is true if and only if x is a alphabetic character,
i.e., one of the characters #a, #b, ..., #z, #A, #B, ..., #Z.

The guard for alpha-char-p requires its argument to be a character.

Alpha-char-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

ALPHORDER    total order on atoms

Alphorder is a non-strict total order, a "less than or equal," on
atoms.  By "non-strict total order" we mean a function that always
returns t or nil and satisfies the following properties.

     o Antisymmetry:  XrY & YrX -> X=Y

     o Transitivity:  XrY & YrZ -> XrZ

     o Trichotomy:  XrY v YrX

Also see LEXORDER, which extends alphorder to all objects.

(Alphorder x y) has a guard of (and (atom x) (atom y)).

Within a single type: rationals are compared arithmetically, complex
rationals are compared lexicographically, characters are compared via
their char-codes, and strings and symbols are compared with alphabetic
ordering.  Across types, rationals come before complexes, complexes
come before characters, characters before strings, and strings before
symbols.  We also allow for "bad atoms," i.e., atoms that are not legal
Lisp objects but make sense in the ACL2 logic; these come at the end,
after symbols.

AND    conjunction

And is the macro for conjunctions.  And takes any number of arguments.
And returns nil if one of the arguments is nil, but otherwise returns
the last argument.  If there are no arguments, and returns t.

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

APPEND    concatenate zero or more lists

Append, which takes zero or more arguments, expects all the arguments
except perhaps the last to be true (null-terminated) lists.  It returns
the result of concatenating all the elements of all the given lists
into a single list.  Actually, in ACL2 append is a macro that expands
into calls of the binary function binary-append if there are at least
two arguments; if there is just one argument then the expansion is that
argument; and finally, (append) expands to nil.

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

ASH    arithmetic shift operation

(ash i c) is the result of taking the two's complement representation
of the integer i and shifting it by c bits:  shifting left and padding
with c 0 bits if c is positive, shifting right and dropping (abs c)
bits if c is negative, and simply returning i if c is 0.

The guard for ash requires that its arguments are integers.

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

ASSERT$    cause a hard error if the given test is false

     General Form:
     (assert$ test form)

where test returns a single value and form is arbitrary.  Semantically,
this call of assert$ is equivalent to form.  However, it causes a hard
error if the value of test is nil.  That hard error invokes the
function illegal, which has a guard that is equal to nil; so if you use
assert$ in code for which you verify guards, then a proof obligation
will be that the occurrence of test is never nil.

ASSOC    look up key in association list

     General Forms:
     (assoc x alist)
     (assoc x alist :test 'eql)   ; same as above (eql as equality test)
     (assoc x alist :test 'eq)    ; same, but eq is equality test
     (assoc x alist :test 'equal) ; same, but equal is equality test

(Assoc x alist) is the first member of alist whose car is x, or nil if
no such member exists.  The optional keyword, :TEST, has no effect
logically, but provides the test (default eql) used for comparing x
with the cars of successive elements of alist.

The guard for a call of assoc depends on the test.  In all cases, the
second argument must satisfy alistp.  If the test is eql, then either
the first argument must be suitable for eql (see EQLABLEP) or
the second argument must satisfy eqlable-alistp.  If the test is eq,
then either the first argument must be a symbol or the second argument
must satisfy symbol-alistp.

See EQUALITY-VARIANTS for a discussion of the relation between
assoc and its variants:

     (assoc-eq x alist) is equivalent to (assoc x alist :test 'eq);

     (assoc-equal x alist) is equivalent to (assoc x alist :test
     'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function assoc-equal.

Assoc is defined by Common Lisp.  See any Common Lisp documentation for
more information.

ASSOC-EQ    See ASSOC.

ASSOC-EQUAL    See ASSOC.

ASSOC-KEYWORD    look up key in a keyword-value-listp

If l is a list of even length of the form (k1 a1 k2 a2 ... kn an),
where each ki is a keyword, then (assoc-keyword key l) is the first
tail of l starting with key if key is some ki, and is nil otherwise.

The guard for (assoc-keyword key l) is (keyword-value-listp l).

ASSOC-STRING-EQUAL    look up key, a string, in association list

(Assoc-string-equal x alist) is similar to assoc-equal.  However, for
string x and alist alist, the comparison of x with successive keys in
alist is done using string-equal rather than equal.

The guard for assoc-string-equal requires that x is a string and alist
is an alist.

ATOM    recognizer for atoms

(atom x) is true if and only if x is an atom, i.e., not a cons pair.

Atom has a guard of t, and is a Common Lisp function.  See any Common
Lisp documentation for more information.

ATOM-LISTP    recognizer for a true list of atoms

The predicate atom-listp tests whether its argument is a true-listp of
atoms, i.e., of non-conses.

Also see GOOD-ATOM-LISTP.

BINARY-*    multiplication function

Completion Axiom (completion-of-*):

     (equal (binary-* x y)
            (if (acl2-numberp x)
                (if (acl2-numberp y)
                    (binary-* x y)
                  0)
              0))

Guard for (binary-* x y):

     (and (acl2-numberp x) (acl2-numberp y))

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

Calls of the macro * expand to calls of binary-*; see *.

BINARY-+    addition function

Completion Axiom (completion-of-+):

     (equal (binary-+ x y)
            (if (acl2-numberp x)
                (if (acl2-numberp y)
                    (binary-+ x y)
                  x)
              (if (acl2-numberp y)
                  y
                0)))

Guard for (binary-+ x y):

     (and (acl2-numberp x) (acl2-numberp y))

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

Calls of the macro + expand to calls of binary-+; see +.

BINARY-APPEND    concatenate two lists

This binary function implements append, which is a macro in ACL2.  See
APPEND

The guard for binary-append requires the first argument to be a
true-listp.

BOOLE$    perform a bit-wise logical operation on 2 two's complement integers

When integers x and y are viewed in their two's complement
representation, (boole$ op x y) returns the result of applying the
bit-wise logical operation specified by op.  The following table is
adapted from documentation for analogous Common Lisp function boole in
the Common Lisp HyperSpec
(`http://www.lisp.org/HyperSpec/Body/fun_boole.html#boole').  Note that
the values of op for boole$ are ACL2 constants, rather than
corresponding values of op for the Common Lisp function boole.

     op               result
     -----------      ---------
     *boole-1*        x
     *boole-2*        y
     *boole-andc1*    and complement of x with y
     *boole-andc2*    and x with complement of y
     *boole-and*      and
     *boole-c1*       complement of x
     *boole-c2*       complement of y
     *boole-clr*      the constant 0 (all zero bits)
     *boole-eqv*      equivalence (exclusive nor)
     *boole-ior*      inclusive or
     *boole-nand*     not-and
     *boole-nor*      not-or
     *boole-orc1*     or complement of x with y
     *boole-orc2*     or x with complement of y
     *boole-set*      the constant -1 (all one bits)
     *boole-xor*      exclusive or

The guard of boole$ specifies that op is the value of one of the
constants above and that x and y are integers.

See any Common Lisp documentation for analogous information about
Common Lisp function boole.

BOOLEANP    recognizer for booleans

(Booleanp x) is t if x is t or nil, and is nil otherwise.

See GENERALIZED-BOOLEANS for a discussion of a potential
soundness problem for ACL2 related to the question:  Which Common Lisp
functions are known to return Boolean values?

BUTLAST    all but a final segment of a list

(Butlast l n) is the list obtained by removing the last n elements from
the true list l.  The following is a theorem (though it takes some
effort, including lemmas, to get ACL2 to prove it).

     (implies (and (integerp n)
                   (<= 0 n)
                   (true-listp l))
              (equal (length (butlast l n))
                     (if (< n (length l))
                         (- (length l) n)
                       0)))

For related functions, see TAKE and see NTHCDR.

The guard for (butlast l n) requires that n is a nonnegative integer
and lst is a true list.

Butlast is a Common Lisp function.  See any Common Lisp documentation
for more information.  Note:  In Common Lisp the second argument of
butlast is optional, but in ACL2 it is required.

CAAAAR    car of the caaar

See any Common Lisp documentation for details.

CAAADR    car of the caadr

See any Common Lisp documentation for details.

CAAAR    car of the caar

See any Common Lisp documentation for details.

CAADAR    car of the cadar

See any Common Lisp documentation for details.

CAADDR    car of the caddr

See any Common Lisp documentation for details.

CAADR    car of the cadr

See any Common Lisp documentation for details.

CAAR    car of the car

See any Common Lisp documentation for details.

CADAAR    car of the cdaar

See any Common Lisp documentation for details.

CADADR    car of the cdadr

See any Common Lisp documentation for details.

CADAR    car of the cdar

See any Common Lisp documentation for details.

CADDAR    car of the cddar

See any Common Lisp documentation for details.

CADDDR    car of the cdddr

See any Common Lisp documentation for details.

CADDR    car of the cddr

See any Common Lisp documentation for details.

CADR    car of the cdr

See any Common Lisp documentation for details.

CAR    returns the first element of a non-empty list, else nil

Completion Axiom (completion-of-car):

     (equal (car x)
            (cond
             ((consp x)
              (car x))
             (t nil)))

Guard:

     (or (consp x) (equal x nil))

Notice that in the ACL2 logic, car returns nil for every atom.

CASE    conditional based on if-then-else using eql

     Example Form:
     (case typ
       ((:character foo)
        (open file-name :direction :output))
       (bar (open-for-bar file-name))
       (otherwise
        (my-error "Illegal.")))

is the same as

     (cond ((member typ '(:character foo))
            (open file-name :direction :output))
           ((eql typ 'bar)
            (open-for-bar file-name))
           (t (my-error "Illegal.")))

which in turn is the same as

     (if (member typ '(:character foo))
         (open file-name :direction :output)
         (if (eql typ 'bar)
             (open-for-bar file-name)
             (my-error "Illegal.")))

Notice the quotations that appear in the example above: '(:character
foo) and 'bar.

     General Forms:
     (case expr
       (x1 val-1)
       ...
       (xk val-k)
       (otherwise val-k+1))

     (case expr
       (x1 val-1)
       ...
       (xk val-k)
       (t val-k+1))

     (case expr
       (x1 val-1)
       ...
       (xk val-k))

where each xi is either eqlablep or a true list of eqlablep objects.
The final otherwise or t case is optional.

Case is defined in Common Lisp.  See any Common Lisp documentation for
more information.

CASE-MATCH    pattern matching or destructuring

     General Form:
     (case-match x
       (pat1 dcl1 body1)
       ...
       (patk dclk bodyk))

where x is a variable symbol, the pati are structural patterns as
described below, the dcli are optional declare forms and the bodyi are
terms.  Return the value(s) of the bodyi corresponding to the first
pati matching x, or nil if none matches.

Pattern Language:
With the few special exceptions described below, matching requires that
the cons structure of x be isomorphic to that of the pattern, down to
the atoms in the pattern.  Non-symbol atoms in the pattern match only
themselves.  Symbols in the pattern denote variables which match
anything and which are bound by a successful match to the corresponding
substructure of x.  Variables that occur more than once must match the
same (EQUAL) structure in every occurrence.

     Exceptions:
     &               Matches anything and is not bound.  Repeated
                       occurrences of & in a pattern may match different
                       structures.
     nil, t, *sym*   These symbols cannot be bound and match only their
                       global values.
     !sym            where sym is a symbol that is already bound in the
                       context of the case-match, matches only the
                       current binding of sym.
     'obj            Matches only itself.

Some examples are shown below.

Below we show some sample patterns and examples of things they match
and do not match.

     pattern       matches         non-matches
     (x y y)       (ABC 3 3)       (ABC 3 4)    ; 3 is not 4
     (fn x . rst)  (P (A I) B C)   (ABC)        ; NIL is not (x . rst)
                   (J (A I))                    ; rst matches nil
     ('fn (g x) 3) (FN (H 4) 3)    (GN (G X) 3) ; 'fn matches only itself
     (& t & !x)    ((A) T (B) (C))              ; provided x is '(C)

Consider the two binary trees that contain three leaves.  They might be
described as (x . (y . z)) and ((x . y) . z), where x, y, and z are
atomic.  Suppose we wished to recognize those trees.  The following
case-match would do:

     (case-match tree
       ((x . (y . z))
        (and (atom x) (atom y) (atom z)))
       (((x . y) . z)
        (and (atom x) (atom y) (atom z))))

Suppose we wished to recognize such trees where all three tips are
identical.  Suppose further we wish to return the tip if the tree is
one of those recognized ones and to return the number 7 otherwise.

     (case-match tree
       ((x . (x . x))
        (if (atom x) x 7))
       (((x . x) . x)
        (if (atom x) x 7))
       (& 7))

Note that case-match returns nil if no pati matches.  Thus if we must
return 7 in that case, we have to add as the final pattern the &, which
always matches anything.

CDAAAR    cdr of the caaar

See any Common Lisp documentation for details.

CDAADR    cdr of the caadr

See any Common Lisp documentation for details.

CDAAR    cdr of the caar

See any Common Lisp documentation for details.

CDADAR    cdr of the cadar

See any Common Lisp documentation for details.

CDADDR    cdr of the caddr

See any Common Lisp documentation for details.

CDADR    cdr of the cadr

See any Common Lisp documentation for details.

CDAR    cdr of the car

See any Common Lisp documentation for details.

CDDAAR    cdr of the cdaar

See any Common Lisp documentation for details.

CDDADR    cdr of the cdadr

See any Common Lisp documentation for details.

CDDAR    cdr of the cdar

See any Common Lisp documentation for details.

CDDDAR    cdr of the cddar

See any Common Lisp documentation for details.

CDDDDR    cdr of the cdddr

See any Common Lisp documentation for details.

CDDDR    cdr of the cddr

See any Common Lisp documentation for details.

CDDR    cdr of the cdr

See any Common Lisp documentation for details.

CDR    returns the second element of a cons pair, else nil

Completion Axiom (completion-of-cdr):

     (equal (cdr x)
            (cond
             ((consp x)
              (cdr x))
             (t nil)))

Guard:

     (or (consp x) (equal x nil))

Notice that in the ACL2 logic, cdr returns nil for every atom.

CEILING    division returning an integer by truncating toward positive infinity

     Example Forms:
     ACL2 !>(ceiling 14 3)
     5
     ACL2 !>(ceiling -14 3)
     -4
     ACL2 !>(ceiling 14 -3)
     -4
     ACL2 !>(ceiling -14 -3)
     5
     ACL2 !>(ceiling -15 -3)
     5

(Ceiling i j) is the result of taking the quotient of i and j and
returning the smallest integer that is at least as great as that
quotient.  For example, the quotient of -14 by 3 is -4 2/3, and the
smallest integer at least that great is -4.

The guard for (ceiling i j) requires that i and j are rational (real,
in ACL2(r)) numbers and j is non-zero.

Ceiling is a Common Lisp function.  See any Common Lisp documentation
for more information.  However, note that unlike Common Lisp, the ACL2
ceiling function returns only a single value,

CHAR    the nth element (zero-based) of a string

(Char s n) is the nth element of s, zero-based.  If n is greater than
or equal to the length of s, then char returns nil.

(Char s n) has a guard that n is a non-negative integer and s is a
stringp.

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

CHAR-CODE    the numeric code for a given character

Completion Axiom (completion-of-char-code):

     (equal (char-code x)
            (if (characterp x)
                (char-code x)
              0))

Guard for (char-code x):

     (characterp x)

This function maps all non-characters to 0.

CHAR-DOWNCASE    turn upper-case characters into lower-case characters

(Char-downcase x) is equal to #a when x is #A, #b when x is #B, ...,
and #z when x is #Z, and is x for any other character.

The guard for char-downcase requires its argument to be a standard
character (see STANDARD-CHAR-P).

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

CHAR-EQUAL    character equality without regard to case

For characters x and y, (char-equal x y) is true if and only if x and y
are the same except perhaps for their case.

The guard on char-equal requires that its arguments are both standard
characters (see STANDARD-CHAR-P).

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

CHAR-UPCASE    turn lower-case characters into upper-case characters

(Char-upcase x) is equal to #A when x is #a, #B when x is #b, ..., and
#Z when x is #z, and is x for any other character.

The guard for char-upcase requires its argument to be a standard
character (see STANDARD-CHAR-P).

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

CHAR<    less-than test for characters

(char< x y) is true if and only if the character code of x is less than
that of y.  See CHAR-CODE.

The guard for char< specifies that its arguments are characters.

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

CHAR<=    less-than-or-equal test for characters

(char<= x y) is true if and only if the character code of x is less
than or equal to that of y.  See CHAR-CODE.

The guard for char<= specifies that its arguments are characters.

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

CHAR>    greater-than test for characters

(char> x y) is true if and only if the character code of x is greater
than that of y.  See CHAR-CODE.

The guard for char> specifies that its arguments are characters.

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

CHAR>=    greater-than-or-equal test for characters

(char>= x y) is true if and only if the character code of x is greater
than or equal to that of y.  See CHAR-CODE.

The guard for char>= specifies that its arguments are characters.

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

CHARACTER-ALISTP    recognizer for association lists with characters as keys

(Character-alistp x) is true if and only if x is a list of pairs of the
form (cons key val) where key is a characterp.

CHARACTER-LISTP    recognizer for a true list of characters

The predicate character-listp tests whether its argument is a true list
of characters.

CHARACTERP    recognizer for characters

(characterp x) is true if and only if x is a character.

CHARACTERS    characters in ACL2

ACL2 accepts 256 distinct characters, which are the characters obtained
by applying the function code-char to each integer from 0 to 255.
Among these, Common Lisp designates certain ones as _standard
characters_, namely those of the form (code-char n) where n is from 33
to 126, together with #\Newline and #\Space.  The actual standard
characters may be viewed by evaluating the defconst *standard-chars*.

To be more precise, Common Lisp does not specify the precise
relationship between code-char and the standard characters.  However,
we check that the underlying Common Lisp implementation uses a
particular relationship that extends the usual ASCII coding of
characters.  We also check that Space, Tab, Newline, Page, and Rubout
correspond to characters with respective char-codes 32, 9, 10, 12, and
127.

Code-char has an inverse, char-code.  Thus, when char-code is applied
to an ACL2 character, c, it returns a number n between 0 and 255
inclusive such that (code-char n) = c.

The preceding paragraph implies that there is only one ACL2 character
with a given character code.  CLTL allows for "attributes" for
characters, which could allow distinct characters with the same code,
but ACL2 does not allow this.

_The Character Reader_

ACL2 supports the `#\' notation for characters provided by Common Lisp,
with some restrictions.  First of all, for every character c, the
notation

     #\c

may be used to denote the character object c.  That is, the user may
type in this notation and ACL2 will read it as denoting the character
object c.  In this case, the character immediately following c must be
one of the following "terminating characters": a Tab, a Newline, a Page
character, a space, or one of the characters:

     "  '  (  )  ;  `  ,

Other than the notation above, ACL2 accepts alternate notation for five
characters.

     #\Space
     #\Tab
     #\Newline
     #\Page
     #\Rubout

Again, in each of these cases the next character must be from among the
set of "terminating characters" described in the single-character case.
Our implementation is consistent with IS0-8859, even though we don't
provide #\ syntax for entering characters other than that described
above.

Finally, we note that it is our intention that any object printed by
ACL2's top-level-loop may be read back into ACL2.  Please notify the
implementors if you find a counterexample to this claim.

CLOSE-INPUT-CHANNEL    See IO.

CLOSE-OUTPUT-CHANNEL    See IO.

CODE-CHAR    the character corresponding to a given numeric code

Completion Axiom (completion-of-code-char):

     (equal (code-char x)
            (if (and (integerp x)
                     (>= x 0)
                     (< x 256))
                (code-char x)
              (code-char 0)))

Guard for (code-char x):

     (and (integerp x)
          (>= x 0)
          (< x 256))

ACL2 supports 8-bit characters.  Inputs not between 0 and 255 are
treated as 0.

COERCE    coerce a character list to a string and a string to a list

Completion Axiom (completion-of-coerce):

     (equal (coerce x y)
            (cond
             ((equal y 'list)
              (if (stringp x)
                  (coerce x 'list)
                nil))
             (t
              (coerce (make-character-list x) 'string))))

Guard for (coerce x y):

     (if (equal y 'list)
         (stringp x)
       (if (equal y 'string)
           (character-listp x)
         nil))

Also see distributed book books/misc/fast-coerce.lisp, contributed by
Jared Davis, for a version of coerce that may be faster for Common Lisp
implementations other than CCL 1.3 or later, if the second argument is
'list (for coercing a string to a list).

COMPILATION    compiling ACL2 functions

ACL2 has several mechanisms to speed up the evaluation of function
calls by _compiling_ functions: see COMP, see
SET-COMPILE-FNS, and see CERTIFY-BOOK.  The intention is that
compilation never changes the value returned by a function call, though
it could cause the call to succeed rather than fail, for example by
avoiding a stack overflow.

The state global variable 'compiler-enabled is set automatically when
the system is built, and may depend on the underlying Lisp
implementation.  (In order to disable the compiler at build time, which
will defeat the speed-up but usually be pretty harmless when the host
Lisp is CCL or SBCL, see the discussion of ACL2_COMPILER_DISABLED in
distributed file GNUmakefile.)  The value of 'compiler-enabled, as
returned by (@ compiler-enabled), can be t, :books, or nil.  If the
value is nil, then include-book and certify-book coerce their arguments
:load-compile-file and compile-flg arguments (respectively) to nil.
Otherwise, the value is :books or t and there is no such coercion; but
if the value is not t, then comp and set-compile-fns are no-ops, which
is probably desirable for Lisps such as CCL and SBCL that compile
on-the-fly even when the compiler is not explicitly invoked.

However, you may have reason to want to change the above (default)
behavior.  To enable compilation by default for certify-book and
include-book but not for comp or set-compile-fns:

     (set-compiler-enabled :books state)

To enable compilation not only as above but also for comp and
set-compile-fns:

     (set-compiler-enabled t state)

To suppress compilation and loading of compiled files by include-book:

     (set-compiler-enabled nil state)

See BOOK-COMPILED-FILE for more discussion about compilation and
books.

COMPLEX    create an ACL2 number

     Examples:
     (complex x 3) ; x + 3i, where i is the principal square root of -1
     (complex x y) ; x + yi
     (complex x 0) ; same as x, for rational numbers x

The function complex takes two rational number arguments and returns an
ACL2 number.  This number will be of type (complex rational) [as
defined in the Common Lisp language], except that if the second
argument is zero, then complex returns its first argument.  The
function complex-rationalp is a recognizer for complex rational
numbers, i.e. for ACL2 numbers that are not rational numbers.

The reader macro #C (which is the same as #c) provides a convenient way
for typing in complex numbers.  For explicit rational numbers x and y,
#C(x y) is read to the same value as (complex x y).

The functions realpart and imagpart return the real and imaginary parts
(respectively) of a complex (possibly rational) number.  So for
example, (realpart #C(3 4)) = 3, (imagpart #C(3 4)) = 4, (realpart 3/4)
= 3/4, and (imagpart 3/4) = 0.

The following built-in axiom may be useful for reasoning about complex
numbers.

     (defaxiom complex-definition
       (implies (and (real/rationalp x)
                     (real/rationalp y))
                (equal (complex x y)
                       (+ x (* #c(0 1) y))))
       :rule-classes nil)

A completion axiom that shows what complex returns on arguments
violating its guard (which says that both arguments are rational
numbers) is the following, named completion-of-complex.

     (equal (complex x y)
            (complex (if (rationalp x) x 0)
                     (if (rationalp y) y 0)))

COMPLEX-RATIONALP    recognizes complex rational numbers

     Examples:
     (complex-rationalp 3)       ; nil, as 3 is rational, not complex rational
     (complex-rationalp #c(3 0)) ; nil, since #c(3 0) is the same as 3
     (complex-rationalp t)       ; nil
     (complex-rationalp #c(3 1)) ; t, as #c(3 1) is the complex number 3 + i

See COMPLEX for more about complex rationals in ACL2.

COMPLEX/COMPLEX-RATIONALP    recognizer for complex numbers

For most ACL2 users, this is a macro abbreviating complex-rationalp;
see COMPLEX-RATIONALP.  In  ACL2(r) (see REAL), a
complex number x may have irrational real and imaginary parts.  This
macro abbreviates the predicate complexp in ACL2(r), which holds for
such x.  Most ACL2 users can ignore this macro and use complex-rationalp
instead.  Some books in the ACL2 distribution use
complex/complex-rationalp so that they are suitable for ACL2(r) as well.

CONCATENATE    concatenate lists or strings together

     Examples:
     (concatenate 'string "ab" "cd" "ef")     ; equals "abcdef"
     (concatenate 'string "ab")               ; equals "ab"
     (concatenate 'list '(a b) '(c d) '(e f)) ; equals '(a b c d e f)
     (concatenate 'list)                      ; equals nil

     General Form:
     (concatenate result-type x1 x2 ... xn)

where n >= 0 and either:  result-type is 'string and each xi is a
string; or result-type is 'list and each xi is a true list.
Concatenate simply concatenates its arguments to form the result string
or list.  Also see APPEND and see STRING-APPEND.  (The
latter immediately generates a call to concatenate when applied to
strings.)

Note:  We do *not* try to comply with the Lisp language's insistence
that concatenate copies its arguments.  Not only are we in an
applicative setting, where this issue shouldn't matter for the logic,
but also we do not actually modify the underlying lisp implementation
of concatenate; we merely provide a definition for it.

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

COND    conditional based on if-then-else

Cond is the construct for IF, THEN, ELSE IF, ...  The test is against
nil.  The argument list for cond is a list of "clauses", each of which
is a list.  In ACL2, clauses must have length 1 or 2.

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

CONJUGATE    complex number conjugate

Conjugate takes an ACL2 number as an argument, and returns its complex
conjugate (i.e., the result of negating its imaginary part.).

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

CONS    pair and list constructor

(cons x y) is a pair whose first component is x and second component is
y.  If y is a list, then (cons x y) is a list that has an addtional
element x on the front.

CONSP    recognizer for cons pairs

(consp x) is true if and only if x is a cons pair.

COUNT    count the number of occurrences of an item in a string or true-list

     Example Forms:
     (count #\D "DabcDefcDe")                 ; = 3
     (count #\D "DabcDefcDe" :start 1)        ; = 2
     (count #\D "DabcDefcDe" :start 1 :end 5) ; = 1
     (count #\D "DabcDefcDe" :start 1 :end 4) ; = 0
     (count #\z "DabcDefcDe")                 ; = 0
     (count '(a b) '(17 (a b) 23 (a b) (c d)))   ; = 2

     General Form:
     (count item sequence &key start end)

(Count item sequence) returns the number of times item occurs in
sequence.  The guard for calls of count (which is actually a macro in
ACL2) specifies that sequence is a string or a true-list, and that
start, which defaults to 0, and end, which defaults to the length of
sequence, are valid indices into sequence.

See any Common Lisp documentation for more information about count,
which is a Common Lisp utility.  At this time ACL2 does not support
keyword arguments for count other than :start and :end; we may add
support for the :from-end keyword upon request.

CPU-CORE-COUNT    the number of cpu cores

Unless the ACL2 executable supports parallel evaluation (see
PARALLELISM), this function returns (mv 1 state).  Otherwise:

(Cpu-core-count state) returns (mv core-count state), where core-count
is the number of cpu cores if ACL2 can get that information from the
underlying Common Lisp implementation.  Otherwise an error occurs,
unless global 'cpu-core-count is assigned to a positive integer value
(see ASSIGN), in which case that value is returned as the
core-count.

     Example:
     (cpu-core-count state) ==> (mv 4 state)
.

CW    print to the comment window

Example:

     (cw "The goal is ~p0 and the alist is ~x1.~%"
         (untranslate term t nil)
         unify-subst)

Logically, this expression is equivalent to nil.  However, it has the
effect of first printing to the so-called "comment window" the fmt
string as indicated.  Thus, cw is like fmt (see FMT) except in
three important ways.  First, it is a macro whose calls expand to calls
of a :logic mode function.  Second, it neither takes nor returns the
ACL2 state; logically cw simply returns nil, although it prints to a
_comment window_ that just happens to share the terminal screen with
the standard character output *standard-co*.  Third, its fmt args are
positional references, so that for example

     (cw "Answers: ~p0 and ~p1" ans1 ans2)

prints in the same manner as:

     (fmt "Answers: ~p0 and ~p1"
          (list (cons #\0 ans1) (cons #\1 ans2))
          *standard-co* state nil)

Typically, calls of cw are embedded in prog2$ forms, e.g.,

     (prog2$ (cw ...)
             (mv a b c))

which has the side-effect of printing to the comment window and
logically returning (mv a b c).

     General Form:
     (cw fmt-string arg1 arg2 ... argn)

where n is between 0 and 9 (inclusive).  The macro uses
fmt-to-comment-window, passing it the column 0 and evisc-tuple nil,
after assembling the appropriate alist binding the fmt vars #\0 through
#\9; see FMT.  If you want

     (a) more than 10 vars,
     (b) vars other than the digit chars,
     (c) a different column, or
     (d) a different evisc-tuple,

then call fmt-to-comment-window instead.

Also see CW!, which is useful if you want to be able to read
the printed forms back in.

Finally, we discuss another way to create formatted output that also
avoids the need to pass in the ACL2 state.  The idea is to use
wormholes; see WORMHOLE.  Below is a function you can write,
along with some calls, providing an illustration of this approach.

     (defun my-fmt-to-comment-window (str alist)
       (wormhole 'my-fmt-to-comment-window
                 '(lambda (whs) whs)
                 (list str alist)
                 '(pprogn
                   (fms (car (@ wormhole-input))
                        (cadr (@ wormhole-input))
                        *standard-co*
                        state
                        nil)
                   (value :q))
                 :ld-verbose nil
                 :ld-error-action :return ; harmless return on error
                 :ld-prompt nil))

     ; A non-erroneous call:
     (my-fmt-to-comment-window "Here is ~x0 for your inspection~%"
                               (list (cons #\0 'foo)))

     ; An error inside the fmt string (unbound fmt var); note that even
     ; with the error, the wormhole is exited.
     (my-fmt-to-comment-window "Here is ~x1 for your inspection~%"
                               (list (cons #\0 'foo)))

     ; A guard violation in the binding; note that even with the error,
     ; the wormhole is exited.
     (my-fmt-to-comment-window "Here is ~x0 for your inspection~%"
                               (list (cons #\0 (car 'foo))))

CW!    print to the comment window

This is the same as cw, except that cw inserts backslash (\) characters
when forced to print past the right margin, in order to make the output
a bit clearer in that case.  Use cw! instead if you want to be able to
read the forms back in.

DECLARE    declarations

     Examples:
     (declare (ignore x y z))
     (declare (ignorable x y z)
              (type integer i j k)
              (type (satisfies integerp) m1 m2))
     (declare (xargs :guard (and (integerp i)
                                 (<= 0 i))
                     :guard-hints (("Goal" :use (:instance lemma3
                                                   (x (+ i j)))))))

     General Form:
     (declare d1 ... dn)
     where, in ACL2, each di is of one of the following forms:

       (ignore v1 ... vn) -- where each vi is a variable introduced in
       the immediately superior lexical environment.  These variables must not
       occur free in the scope of the declaration.

       (ignorable v1 ... vn) -- where each vi is a variable introduced in
       the immediately superior lexical environment.  These variables need not
       occur free in the scope of the declaration.  This declaration can be useful
       for inhibiting compiler warnings.

       (type type-spec v1 ... vn) -- where each vi is a variable introduced in the
       immediately superior lexical environment and type-spec is a type specifier
       (as described in the documentation for type-spec).

       (xargs :key1 val1 ... :keyn valn) -- where the legal values of the keyi's
       and their respective vali's are described in the documentation for
       xargs.

       (optimize ...) -- for example, (optimize (safety 3)).  This is allowed
       only at the top level of defun forms.  See any Common Lisp
       documentation for more information.

Declarations in ACL2 may occur only where dcl occurs below:

       (DEFUN name args doc-string dcl ... dcl body)
       (DEFMACRO name args doc-string dcl ... dcl body)
       (LET ((v1 t1) ...) dcl ... dcl body)
       (MV-LET (v1 ...) term dcl ... dcl body)

Of course, if a form macroexpands into one of these (as let* expands
into nested lets and our er-let* expands into nested mv-lets) then
declarations are permitted as handled by the macros involved.

Declare is defined in Common Lisp.  See any Common Lisp documentation
for more information.

DEFMACRO-LAST    define a macro that returns its last argument, but with side effects

This is an advanced feature that requires a trust tag.  For explanation,
including an example, see RETURN-LAST.

DEFN    definition with guard t

Defn is defun with guard t.

DELETE-ASSOC    modify an association list by associating a value with a key

     General Forms:
     (delete-assoc key alist)
     (delete-assoc key alist :test 'eql)   ; same as above (eql as equality test)
     (delete-assoc key alist :test 'eq)    ; same, but eq is equality test
     (delete-assoc key alist :test 'equal) ; same, but equal is equality test

(Delete-assoc key alist) returns an alist that is the same as the list
alist, except that the first pair in alist with a car of key is
deleted, if there is one; otherwise alist is returned.  Note that the
order of the elements of alist is unchanged (though one may be deleted).

The guard for a call of delete-assoc depends on the test.  In all
cases, the second argument must satisfy alistp.  If the test is eql,
then either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-alistp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-alistp.

See EQUALITY-VARIANTS for a discussion of the relation between
delete-assoc and its variants:

     (delete-assoc-eq key alist) is equivalent to (delete-assoc key
     alist :test 'eq);

     (delete-assoc-equal key alist) is equivalent to (delete-assoc key
     alist :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function delete-assoc-equal.

DELETE-ASSOC-EQ    See DELETE-ASSOC.

DELETE-ASSOC-EQUAL    See DELETE-ASSOC.

DENOMINATOR    divisor of a ratio in lowest terms

Completion Axiom (completion-of-denominator):

     (equal (denominator x)
            (if (rationalp x)
                (denominator x)
              1))

Guard for (denominator x):

     (rationalp x)

DIGIT-CHAR-P    the number, if any, corresponding to a given character

(digit-char-p ch) is the integer corresponding to the character ch in
base 10.  For example, (digit-char-p #\3) is equal to the integer 3.
More generally, an optional second argument specifies the radix
(default 10, as indicated above).

The guard for digit-char-p (more precisely, for the function
our-digit-char-p that calls of this macro expand to) requires its
second argument to be an integer between 2 and 36, inclusive, and its
first argument to be a character.

Digit-char-p is a Common Lisp function, though it is implemented in the
ACL2 logic as an ACL2 macro.  See any Common Lisp documentation for
more information.

DIGIT-TO-CHAR    map a digit to a character

     Example:
     ACL2 !>(digit-to-char 8)
     #\8

For an integer n from 0 to 15, (digit-to-char n) is the character
corresponding to n in hex notation, using uppercase letters for digits
exceeding 9.  If n is in the appropriate range, that result is of course
also the binary, octal, and decimal digit.

The guard for digit-to-char requires its argument to be an integer
between 0 and 15, inclusive.

E0-ORD-<    the old ordering function for ACL2 ordinals

See O< for the current new ordering function for ACL2 ordinals.

The functions e0-ordinalp and e0-ord-< were replaced in ACL2
Version_2.8 by o-p and o<, respectively.  However, books created before
that version used the earlier functions for termination proofs; the old
functions might be of use in these cases.  To use the old functions in
termination proofs, include the book books/ordinals/e0-ordinal and
execute the event (set-well-founded-relation e0-ord-<) (see
SET-WELL-FOUNDED-RELATION).  For a more thorough discussion of these
functions, see the documentation at the end of
books/ordinals/e0-ordinal.lisp.

E0-ORDINALP    the old recognizer for ACL2 ordinals

See O-P for the current recognizer for ACL2 ordinals.

The functions e0-ordinalp and e0-ord-< were replaced in ACL2
Version_2.8 by o-p and o<, respectively.  However, books created before
that version used the earlier functions for termination proofs; the old
functions might be of use in these cases.  To use the old functions in
termination proofs, include the book books/ordinals/e0-ordinal and
execute the event (set-well-founded-relation e0-ord-<) (see
SET-WELL-FOUNDED-RELATION).  For a more thorough discussion of these
functions, see the documentation at the end of
books/ordinals/e0-ordinal.lisp.

EC-CALL    execute a call in the ACL2 logic instead of raw Lisp

The name "ec-call" represents "executable-counterpart call."  This
utility is intended for users who are familiar with guards.  See
GUARD for a general discussion of guards.

Logically, ec-call behaves like the identity macro; during proofs,
(ec-call TERM) is typically replaced quickly by TERM during a proof
attempt.  However, ec-call causes function calls to be evaluated in the
ACL2 logic rather than raw Lisp, as explained below.

     General Form:
     (ec-call (fn term1 ... termk))

where fn is a known function symbol other than those in the list that is
the value of the constant *ec-call-bad-ops*.  In particular, fn is not
a macro.  Semantically, (ec-call (fn term1 ... termk)) equals (fn term1
... termk).  However, this use of ec-call has two effects.

     (1) Guard verification generates no proof obligations from the
     guard of fn for this call.  Indeed, guards need not have been
     verified for fn.

     (2) During evaluation, after the arguments of fn are evaluated as
     usual, the executable counterpart of fn is called, rather than fn
     as defined in raw Lisp.  That is, the call of fn is made on its
     evaluated arguments as though this call is being made in the ACL2
     top-level loop, rather than in raw Lisp.  In particular, the guard
     of fn is checked, at least by default (see
     SET-GUARD-CHECKING.

Note that in the term (ec-call (fn term1 ... termk)), only the indicated
call of fn is made in the logic; each termi is evaluated in the normal
manner.  If you want an entire term evaluated in the logic, wrap
ec-call around each function call in the term (other than calls of if
and ec-call).

*Technical Remark* (probably best ignored).  During evaluation of a call
of defconst or defpkg in raw Lisp, a form (ec-call (fn term1 ...
termk)) is treated as (fn term1 ... termk), that is, without calling
the executable counterpart of fn.  This situation occurs when loading a
compiled file (or expansion file) on behalf of an include-book event.
The reason is technical: executable counterparts are defined below a
book's events in the book's compiled file.  End of Technical Remark.

Here is a small example.  We define foo recursively but with guard
verification inhibited on the recursive call, which is to be evaluated
in the ACL2 logic.

     ACL2 !>(defun foo (x y)
             (declare (xargs :guard (consp y)))
             (if (consp x)
                 (cons (car x) (ec-call (foo (cdr x) (cdr y))))
               (car y)))

     The admission of FOO is trivial, using the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  We could deduce no constraints on the type of FOO.

     Computing the guard conjecture for FOO....

     The guard conjecture for FOO is trivial to prove.  FOO is compliant
     with Common Lisp.

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO
     ACL2 !>(foo '(2 3 4 5) '(6 7))

     ACL2 Error in TOP-LEVEL:  The guard for the function call (FOO X Y),
     which is (CONSP Y), is violated by the arguments in the call
     (FOO '(4 5) NIL).  To debug see :DOC print-gv, see :DOC trace, and
     see :DOC wet.  See :DOC set-guard-checking for information about suppressing
     this check with (set-guard-checking :none), as recommended for new
     users.

     ACL2 !>

The error above arises because eventually, foo recurs down to a value of
parameter y that violates the guard.  This is clear from tracing (see
TRACE$ and see TRACE).  Each call of the executable
counterpart of foo (the so-called "*1*" function for foo) checks the
guard and then invokes the raw Lisp version of foo.  The raw Lisp
version calls the executable counterpart on the recursive call.  When
the guard check fails we get a violation.

     ACL2 !>(trace$ foo)
      ((FOO))
     ACL2 !>(foo '(2 3 4 5) '(6 7))
     1> (ACL2_*1*_ACL2::FOO (2 3 4 5) (6 7))
       2> (FOO (2 3 4 5) (6 7))
         3> (ACL2_*1*_ACL2::FOO (3 4 5) (7))
           4> (FOO (3 4 5) (7))
             5> (ACL2_*1*_ACL2::FOO (4 5) NIL)

     ACL2 Error in TOP-LEVEL:  The guard for the function call (FOO X Y),
     which is (CONSP Y), is violated by the arguments in the call
     (FOO '(4 5) NIL).  To debug see :DOC print-gv, see :DOC trace, and
     see :DOC wet.  See :DOC set-guard-checking for information about suppressing
     this check with (set-guard-checking :none), as recommended for new
     users.

     ACL2 !>

If we turn off guard errors then we can see the trace as above, but
where we avoid calling the raw Lisp function when the guard fails to
hold.

     ACL2 !>:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(foo '(2 3 4 5) '(6 7))
     1> (ACL2_*1*_ACL2::FOO (2 3 4 5) (6 7))
       2> (FOO (2 3 4 5) (6 7))
         3> (ACL2_*1*_ACL2::FOO (3 4 5) (7))
           4> (FOO (3 4 5) (7))
             5> (ACL2_*1*_ACL2::FOO (4 5) NIL)
               6> (ACL2_*1*_ACL2::FOO (5) NIL)
                 7> (ACL2_*1*_ACL2::FOO NIL NIL)
                 <7 (ACL2_*1*_ACL2::FOO NIL)
               <6 (ACL2_*1*_ACL2::FOO (5))
             <5 (ACL2_*1*_ACL2::FOO (4 5))
           <4 (FOO (3 4 5))
         <3 (ACL2_*1*_ACL2::FOO (3 4 5))
       <2 (FOO (2 3 4 5))
     <1 (ACL2_*1*_ACL2::FOO (2 3 4 5))
     (2 3 4 5)
     ACL2 >

EIGHTH    eighth member of the list

See any Common Lisp documentation for details.

ENDP    recognizer for empty lists

In the ACL2 logic, (endp x) is the same as (atom x).  See ATOM.

Unlike atom, the guard for endp requires that x is a cons pair or is
nil.  Thus, endp is typically used as a termination test for functions
that recur on a true-listp argument.  See GUARD for general
information about guards.

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

EQ    equality of symbols

Eq is the function for determining whether two objects are identical
(i.e., have the exact same store address in the current von Neumann
implementation of Common Lisp).  It is the same as equal in the ACL2
logic.

Eq is a Common Lisp function.  In order to ensure conformance with
Common Lisp, the ACL2 guard on eq requires at least one of the
arguments to eq to be a symbol.  Common Lisp guarantees that if x is a
symbol, then x is eq to y if and only if x is equal to y.  Thus, the
ACL2 user should think of eq as nothing besides a fast means for
checking equal when one argument is known to be a symbol.  In
particular, it is possible that an eq test will not even require the
cost of a function call but will be as fast as a single machine
instruction.

EQL    test equality (of two numbers, symbols, or characters)

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

Unlike equal, eql has a guard requiring at least one of its arguments
to be a number, a symbol, or a character.  Generally, eql is executed
more efficiently than equal.

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

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

EQLABLE-ALISTP    recognizer for a true list of pairs whose cars are suitable for eql

The predicate eqlable-alistp tests whether its argument is a true-listp
of consp objects whose cars all satisfy eqlablep.

EQLABLE-LISTP    recognizer for a true list of objects each suitable for eql

The predicate eqlable-listp tests whether its argument is a true-listp
of objects satisfying eqlablep.

EQLABLEP    the guard for the function eql

The predicate eqlablep tests whether its argument is suitable for eql,
at least one of whose arguments must satisfy this predicate in Common
Lisp.  (Eqlablep x) is true if and only if its argument is a number, a
symbol, or a character.

EQUAL    true equality

(equal x y) is equal to t or nil, according to whether or not x and y
are the same value.

For a discussion of the various idioms for testing against 0, See
ZERO-TEST-IDIOMS.

EQUALITY-VARIANTS    versions of a function using different equality tests

The ACL2 environment includes not only a logic but also a programming
language, which is based on Common Lisp.  Execution efficiency may be
increased by using fast equality tests: eq for symbols and eql for
numbers, symbols, and characters (see EQLABLEP).  Several
list-processing functions built into ACL2 thus have three variants,
depending on whether the equality function used is eq, eql, or equal; a
list is provided below.  ACL2 has taken measures to ensure that one can
reason about a single logical function even when one uses these
different variants.

Consider for example the case of list membership.  Common Lisp provides
a utility for this purposes, member, which can take a :TEST keyword
argument, default eql.  So for example, one might write

     (member a x :TEST 'eq)

if either a is a symbol or x is a list of symbols, so that the fastest
equality test (eq) may be used when comparing a to successive elements
of the list, x.  One might elsewhere write (member b (foo y)), which is
equivalent to (member b (foo y) :TEST 'eql), for example if b is a
number.  If one wants to reason about both (member a x :TEST 'eq) and
(member b y), it might be helpful for both calls of member to be the
same logically, even though Common Lisp will execute them differently
(using eq or eql, respectively).  ACL2 arranges that in fact, both
references to member generate calls of member-equal in the theorem
prover.

In fact, since member can take the optional :TEST keyword argument,
then in ACl2 it must be defined as a macro, not a function (see
DEFUN).  ACL2 arranges that a call of member generates a
corresponding call of the function member-equal, regardless of the
value of TEST, in a manner that produces member-equal in prover output.
More generally, you can expect ACL2 to treat your use of member as
though you had written member-equal, for example in the way it stores
rewrite rules and other kinds of rules as well (see
RULE-CLASSES).  We say little here about how this is all arranged by
ACL2, other than to mention that mbe is utilized (so, you might see
mention in proof logs) of the function return-last that implements mbe.
Such details, which probably can be ignored by most users, may be found
elsewhere; see EQUALITY-VARIANTS-DETAILS.

As a convenience to the user, the macro member-eq is provided that
expands to a corresponding call of member with :TEST 'eq, as follows.

     ACL2 !>:trans1 (member-eq (foo x) (bar y))
      (MEMBER (FOO X) (BAR Y) :TEST 'EQ)
     ACL2 !>

For efficiency we recommend using the -equal equality variant, for
example member-equal or ... :TEST 'equal, in certain contexts:
defmacro, defpkg, defconst, and value-triple forms.  However, the
implementation of equality variants has been designed so that when
defining a function, one may choose freely in a definition an equality
variant of primitive F, to get efficient execution but where subsequent
reasoning is about F-equal.  For details about the above recommendation
and for a discussion of the implementation, see
EQUALITY-VARIANTS-DETAILS.

The following alphabetical list includes all primitives that have
equality variants.  Each macro F listed below takes an optional :TEST
keyword argument of 'eq, 'eql, or 'equal, where 'eql is the default.
For each such F, a function F-equal is defined such that for logical
purposes (in particular theorem proving), each call of F expands to a
corresponding call of F-equal.  For convenience, a macro F-eq is also
defined, so that a call of F-eq expands to a corresponding call of F
with :TEST 'eq.

     add-to-set
     assoc
     delete-assoc
     intersection$ ; (see Note below)
     intersectp
     member
     no-duplicatesp
     position-ac
     position
     put-assoc
     rassoc
     remove-duplicates
     remove1
     remove
     set-difference$ ; (see Note below)
     subsetp
     union$ ; (see Note below)

Note: Three of the macros above have names ending with the character,
`$': intersection$, set-difference$, and union$.  In each case there is
a corresponding Common Lisp primitive without the trailing `$':
intersection, set-difference, and union.  However, Common Lisp does not
specify the order of elements in the list returned by those primitives,
so ACL2 has its own.  Nevertheless, the only use of the trailing `$' is
to distinguish the primitives; associated functions and macros, for
example union-eq and intersection-equal, do not include the `$'
character in their names.

EQUALITY-VARIANTS-DETAILS    details about equality-variants

Here we present details about equality variants, none of which is likely
to be important to the majority of ACL2 users.  Please see
EQUALITY-VARIANTS for relevant background.

We begin by presenting events that implement the equality variants for
member, as these illustrate the events introduced for all macros having
equality variants.  The definition of member, just below, calls the
macro let-mbe, which in turn is just an abbreviation for a combination
of let and mbe.

     (defmacro let-mbe (bindings &key logic exec)
       `(let ,bindings
          (mbe :logic ,logic
               :exec ,exec)))

This use of let arranges that each argument of a call of member is
evaluated only once.

     (defmacro member (x l &key (test ''eql))
       (declare (xargs :guard (or (equal test ''eq)
                                  (equal test ''eql)
                                  (equal test ''equal))))
       (cond
        ((equal test ''eq)
         `(let-mbe ((x ,x) (l ,l))
                   :logic (member-equal x l)
                   :exec  (member-eq-exec x l)))
        ((equal test ''eql)
         `(let-mbe ((x ,x) (l ,l))
                   :logic (member-equal x l)
                   :exec  (member-eql-exec x l)))
        (t ; (equal test 'equal)
         `(member-equal ,x ,l))))

Inspection of the definition above shows that every call of member
expands to one that is logically equivalent to the corresponding call of
member-equal, which is defined as follows.

     (defun member-equal (x lst)
       (declare (xargs :guard (true-listp lst)))
       (cond ((endp lst) nil)
             ((equal x (car lst)) lst)
             (t (member-equal x (cdr lst)))))

The following two definitions model equality variants of member for
tests eq and eql, respectively.

     (defun member-eq-exec (x lst)
       (declare (xargs :guard (if (symbolp x)
                                  (true-listp lst)
                                (symbol-listp lst))))
       (cond ((endp lst) nil)
             ((eq x (car lst)) lst)
             (t (member-eq-exec x (cdr lst)))))

     (defun member-eql-exec (x lst)
       (declare (xargs :guard (if (eqlablep x)
                                  (true-listp lst)
                                (eqlable-listp lst))))
       (cond ((endp lst) nil)
             ((eql x (car lst)) lst)
             (t (member-eql-exec x (cdr lst)))))

At this point the user can write (member x y) or (member-equal x y) to
call equality variants of member with test eql or equal, respectively.
We thus provide the following macro for the eq variant.

     (defmacro member-eq (x lst)
       `(member ,x ,lst :test 'eq))

Guard proof obligations generated by calls of member will include those
based on its use of mbe, and are supported by the following two lemmas.

     (defthm member-eq-exec-is-member-equal
       (equal (member-eq-exec x l)
              (member-equal x l)))

     (defthm member-eql-exec-is-member-equal
       (equal (member-eql-exec x l)
              (member-equal x l)))

Finally, the following two events arrange that in certain contexts such
as theories (including the use of in-theory in events and hints),
member-eq and member are treated as references to member-equal.

     (add-macro-alias member-eq member-equal)
     (add-macro-alias member member-equal)

We conclude this topic by exploring the following recommendation made
in the documentation for equality-variants.

     For efficiency we recommend using the -equal equality variant, for
     example member-equal or ... :TEST 'equal, in certain contexts:
     defmacro, defpkg, defconst, and value-triple forms.

ACL2 reliies on the underlying Common Lisp for evaluation.  It also
processes events in the ACL2 logic.  In order to guarantee consistency
of its logical and Common Lisp evaluations, ACL2 uses a "safe mode" to
avoid ill-guarded calls.  In particular, consider the use of mbe in
execution of a call of an equality variant of a primitive, F, other
than its F-equal variant.  The mbe call discussed above requires a
connection to be established between the :logic and :exec forms.  For
example, if F is called with :TEST 'eql (either explicitly or as the
default), then ACL2 will call both F-eql-exec and F-equal, and check
that the two results are equal.

The following partial log illustrates the point above.  We define a
macro that calls member, and when a call of this macro is expanded
during processing of a subsequent definition, we see that two
membership functions are called on the same arguments.

     ACL2 !>(defmacro mac (lst)
              (list 'quote (and (true-listp lst)
                                (member 'c lst :test 'eq))))

     Summary
     Form:  ( DEFMACRO MAC ...)
     Rules: NIL
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      MAC
     ACL2 !>(trace$ member-equal member-eq-exec)
      ((MEMBER-EQUAL) (MEMBER-EQ-EXEC))
     ACL2 !>(defun f () (mac (a b c d)))
     1> (ACL2_*1*_ACL2::MEMBER-EQ-EXEC C (A B C D))
       2> (MEMBER-EQ-EXEC C (A B C D))
       <2 (MEMBER-EQ-EXEC (C D))
     <1 (ACL2_*1*_ACL2::MEMBER-EQ-EXEC (C D))
     1> (ACL2_*1*_ACL2::MEMBER-EQUAL C (A B C D))
       2> (MEMBER-EQUAL C (A B C D))
       <2 (MEMBER-EQUAL (C D))
     <1 (ACL2_*1*_ACL2::MEMBER-EQUAL (C D))

     Since F is non-recursive, its admission is trivial.

If performance is an issue then we can avoid such a problem, for
example as follows.  In a fresh session, let us define a suitable
wrapper for calling member with :TEST 'eq.  This time, the trace in our
partial log shows that we have avoided calling two membership functions.

     ACL2 !>(defun mem-eq (x lst)
              (declare (xargs :guard (if (symbolp x)
                                         (true-listp lst)
                                       (symbol-listp lst))))
              (member x lst :test 'eq))
     [[ ... output omitted here ... ]]
      MEM-EQ
     ACL2 !>(defmacro mac (lst)
              (list 'quote (and (true-listp lst)
                                (mem-eq 'c lst))))

     Summary
     Form:  ( DEFMACRO MAC ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      MAC
     ACL2 !>(trace$ member-equal member-eq-exec mem-eq)
      ((MEMBER-EQUAL)
       (MEMBER-EQ-EXEC)
       (MEM-EQ))
     ACL2 !>(defun f () (mac (a b c d)))
     1> (ACL2_*1*_ACL2::MEM-EQ C (A B C D))
       2> (MEM-EQ C (A B C D))
       <2 (MEM-EQ (C D))
     <1 (ACL2_*1*_ACL2::MEM-EQ (C D))

     Since F is non-recursive, its admission is trivial.

ER    print an error message and "cause an error"

     Example Forms:
     (er hard  'top-level "Illegal inputs, ~x0 and ~x1." a b)
     (er hard? 'top-level "Illegal inputs, ~x0 and ~x1." a b)
     (er soft  'top-level "Illegal inputs, ~x0 and ~x1." a b)

The examples above all print an error message to standard output saying
that a and b are illegal inputs.  However, the first two abort
evaluation after printing an error message, while the third returns (mv
t nil state) after printing an error message.  The result in the third
case can be interpreted as an "error" when programming with the ACL2
state, something most ACL2 users will probably not want to do; see
LD-ERROR-TRIPLES and see ER-PROGN.

The difference between the hard and hard? forms is one of guards.  Use
hard if you want the call to generate a (clearly impossible) guard
proof obligation of (essentially) NIL.  But use hard? if you want to be
able to call this function in guard-verified code, since the call
generates a (trivially satisfied) guard proof obligation of T.

Er is a macro, and the above three examples expand to calls of ACL2
functions, as shown below.  See ILLEGAL, see
HARD-ERROR, and see ERROR1.  The first two have guards of
(essentially) NIL and T, respectively, while error1 is in :program mode.

     General forms:
     (er hard  ctx fmt-string arg1 arg2 ... argk)
       ==> {macroexpands, in essence, to:}
     (ILLEGAL    CTX FMT-STRING
                 (LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))

     (er hard? ctx fmt-string arg1 arg2 ... argk)
       ==> {macroexpands, in essence, to:}
     (HARD-ERROR CTX FMT-STRING
                 (LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))

     (er soft  ctx fmt-string arg1 arg2 ... argk)
       ==> {macroexpands, in essence, to:}
     (ERROR1     CTX FMT-STRING
                 (LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))

ER-PROGN    perform a sequence of state-changing "error triples"

     Example:
     (er-progn (check-good-foo-p (f-get-global 'my-foo state) state)
               (value (* (f-get-global 'my-foo state)
                         (f-get-global 'bar state))))

This sequencing primitive is only useful when programming with state,
something that very few users will probably want to do.  See
STATE.

Er-progn is used much the way that progn is used in Common Lisp, except
that it expects each form within it to evaluate to an "error triple" of
the form (mv erp val state).  The first such form, if any, that
evaluates to such a triple where erp is not nil yields the error triple
returned by the er-progn.  If there is no such form, then the last form
returns the value of the er-progn form.

We intend to write more about this topic, especially if there are
requests to do so.

ERROR1    print an error message and cause a "soft error"

(Error1 ctx str alist) returns (mv t nil state).  An error message is
first printed using the the "context" ctx, as well as the string str
and alist alist that are of the same kind as expected by fmt.  See
FMT.

Error1 can be interpreted as causing an "error" when programming with
the ACL2 state, something most ACL2 users will probably not want to do;
see LD-ERROR-TRIPLES and see ER-PROGN.  In order to
cause errors with :logic mode functions, see HARD-ERROR and see
ILLEGAL.  Better yet, see ER for a macro that provides
a unified way of signaling errors.

As mentioned above, error1 always returns (mv t nil state).  But if a
call (error1 ctx str alist) is encountered during evaluation, then the
string str is first printed using the association list alist (as in
fmt).  Here is a trivial, contrived example.

     ACL2 !>(error1 'my-context
                    "Printing 4: ~n0"
                    (list (cons #\0 4))
                    state)

     ACL2 Error in MY-CONTEXT:  Printing 4: four

     ACL2 !>

EVENP    test whether an integer is even

(evenp x) is true if and only if the integer x is even.  Actually, in
the ACL2 logic (evenp x) is defined to be true when x/2 is an integer.

The guard for evenp requires its argument to be an integer.

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

EXPLODE-NONNEGATIVE-INTEGER    the list of characters in the radix-r form of a number

     Examples:
     ACL2 !>(explode-nonnegative-integer 925 10 nil)
     (#9 #2 #5)
     ACL2 !>(explode-nonnegative-integer 325 16 nil)
     (#3 #9 #D)

For a non-negative integer n, (explode-nonnegative-integer n r nil) is
the list of characters in the radix-r (base-r) representation of n.

The guard for explode-nonnegative-integer requires the first argument
to be a nonnegative integer and second argument to be a valid radix for
ACL2 (2, 8, 10, or 16).

EXPT    exponential function

(Expt r i) is the result of raising the number r to the integer power i.

The guard for (expt r i) is that r is a number and i is an integer, and
furthermore, if r is 0 then i is nonnegative.  When the type
requirements of the guard aren't met, (expt r i) first coerces r to a
number and i to an integer.

Expt is a Common Lisp function.  See any Common Lisp documentation for
more information.  Note that r can be a complex number; this is
consistent with Common lisp.

FIFTH    fifth member of the list

See any Common Lisp documentation for details.

FIRST    first member of the list

See any Common Lisp documentation for details.

FIX    coerce to a number

Fix simply returns any numeric argument unchanged, returning 0 on a
non-numeric argument.  Also see NFIX, see IFIX, and see
RFIX for analogous functions that coerce to a natural number,
an integer, and a rational number, respectively.

Fix has a guard of t.

FIX-TRUE-LIST    coerce to a true list

Fix-true-list is the identity function on true-listp objects.  It
converts every list to a true list by dropping the final cdr, and it
converts every atom to nil.

FLET    local binding of function symbols

     Example Form:
     ; The following evaluates to (mv 7 10):
     (flet ((f (x)
               (+ x 3))
            (g (x)
               (declare (type integer x))
               (* x 2)))
       (mv (f 4) (g 5)))

     General Form:
     (flet (def1 ... defk) body)

where body is a term, and each defi is a definition as in defun but
with the leading defun symbol omitted.  See DEFUN.  The
innermost flet-binding of a function symbol, f, above a call of f, is
the one that provides the definition of f for that call.  Note that
flet does not provide recursion.  Consider the following example.

     (defun f (x) (+ x 3))
     (flet ((f (x) (cons x (f (1+ x)))))
       (f 4))

In the above term (cons x (f (1+ x))), f refers to the global
definition of f above the flet expression.  However, (f 4) refers to
the flet-binding of f, (f (x) (cons x (f x))).  The result of the flet
expression is thus obtained by evaluating (f 4) where (f 4) is (cons 4
(f (1+ 4))), where the latter call of f refers to the global
definition; thus we have (cons 4 (f 5)), which evaluates to (4 . 8).

Although flet behaves in ACL2 essentially as it does in Common Lisp,
ACL2 imposes the following restrictions and qualifications.

     o Every declare form for a local definition (def1 through defk,
     above) must be an ignore, ignorable, or type expression.

     o Each defi must bind a different function symbol.

     o Each defi must bind a symbol that is a legal name for an ACL2
     function symbol.  In particular, the symbol may not be in the
     keyword package or the main Lisp package.  Moreover, the symbol
     may not be a built-in ACL2 function or macro.

     o Every variable occurring in the body of a defi must be a formal
     parameter of that defi.  (This restriction is not enforced in
     Common Lisp.  If the restriction is inconvenient for you, the ACL2
     implementors may be able to remove it, with some effort, if you
     ask.)

     o If the flet-binding defi is in the body of a function f, then
     the stobj inputs for defi are implicitly those of its inputs that
     are declared stobj inputs of f.

Flet bindings are evaluated in parallel.  Consider the following
example.

     (defun f (x) x)
     (flet ((f (x) (cons x x))
            (g (x) (f x)))
       (g 3))

The binding of g refers to the global value of f, not the flet-binding
of f.  Thus, the flet expression evaluates to 3.  Compare the flet
expression above to the following one, which instead evaluates to (3 .
3).

     (defun f (x) x)
     (flet ((f (x) (cons x x)))
       (flet ((g (x) (f x)))
         (g 3)))

Under the hood, ACL2 translates flet bindings to lambda expressions
(see TERM).  The following example illustrates this point.

     ACL2 !>:trans (flet ((f (x) (cons x x))
                          (g (x y) (+ x y)))
                     (f (g 3 4)))

     ((LAMBDA (X) (CONS X X))
      ((LAMBDA (X Y) (BINARY-+ X Y)) '3 '4))

     => *

     ACL2 !>

Flet is part of Common Lisp.  See any Common Lisp documentation for
more information.  We conclude by pointing out an important aspect of
flet shared by ACL2 and Common Lisp: The binding is lexical, not
dynamic.  That is, the flet binding of a function symbol only applies to
calls of that function symbol in the body of the flet, not other calls
made in the course of evaluation.  Consider the following example.
Suppose we define:

     (defun f (x) x)
     (defun g (x) x)
     (defun h (x)
       (flet ((f (x) (cons x x)))
         (g x)))

Then evaluation of (h 3) results in 3, not in the cons pair (3 . 3),
because the flet binding of f only applies to calls of f that appear in
the body of that flet.  In this case, only g is called in the body of
that flet.

FLOOR    division returning an integer by truncating toward negative infinity

     Example Forms:
     ACL2 !>(floor 14 3)
     4
     ACL2 !>(floor -14 3)
     -5
     ACL2 !>(floor 14 -3)
     -5
     ACL2 !>(floor -14 -3)
     4
     ACL2 !>(floor -15 -3)
     5

(Floor i j) returns the result of taking the quotient of i and j and
returning the greatest integer not exceeding that quotient.  For
example, the quotient of -14 by 3 is -4 2/3, and the largest integer
not exceeding that rational number is -5.

The guard for (floor i j) requires that i and j are rational (real, in
ACL2(r)) numbers and j is non-zero.

Floor is a Common Lisp function.  See any Common Lisp documentation for
more information.  However, note that unlike Common Lisp, the ACL2
floor function returns only a single value,

FMS    :(str alist co-channel state evisc) => state

See FMT for further explanation, including documentation of the
tilde-directives.

FMS!    :(str alist co-channel state evisc) => state

This function is nearly identical to fms; see FMS.  The only
difference is that fms may insert backslash (\) characters when forced
to print past the right margin in order to make the output a bit
clearer in that case.  Use fms! instead if you want to be able to read
the forms back in.

FMS!-TO-STRING    See PRINTING-TO-STRINGS.

FMS-TO-STRING    See PRINTING-TO-STRINGS.

FMT    formatted printing

ACL2 provides the functions fmt, fmt1, and fms as substitutes for
Common Lisp's format function.  Also see FMT!, see
FMT1!, and see FMS! for versions of these functions that
write forms to files in a manner that allows them to be read, by
avoiding using backslash (\) to break long lines.  There are also
analogues of these functions that return a string without taking state
as an argument; see PRINTING-TO-STRINGS.

All three print a given string under an alist pairing character objects
with values, interpreting certain "tilde-directives" in the string.
Channel must be a character output channel (e.g., *standard-co*).

     General Forms:                                            result
     (fms string alist channel state evisc-tuple)         ; state
     (fmt string alist channel state evisc-tuple)         ; (mv col state)
     (fmt1 string alist column channel state evisc-tuple) ; (mv col state)

Fms and fmt print an initial newline to put channel in column 0; Fmt1
requires the current column as input.  Columns are numbered from 0.
The current column is the column into which the next character will be
printed.  (Thus, the current column number is also the number of
characters printed since the last newline.)  The col returned by fmt
and fmt1 is the current column at the conclusion of the formatting.
Evisc-tuple must be either nil (meaning no abbreviations are used when
objects are printed) or an "evisceration tuple"; see
EVISC-TUPLE.

We list the tilde-directives below.  The notation is explained after
the chart.

     ~xx  pretty print vx (maybe after printing a newline)
     ~yx  pretty print vx starting in current column; end with newline
     ~Xxy like ~xx but use vy as the evisceration tuple
     ~Yxy like ~yx but use vy as the evisceration tuple
     ~@x  if vx is a string, "str",  recursively format "str"
          if vx is ("str" . a), recursively format "str" under a+
     ~#x~[...~/...~/ ... ~/...~] cases on vx
          ^    ^     ...   ^  if 0<=vx<=k, choose vxth alternative
          0    1     ...   k  if vx is a list of length 1, case 0; else 1
     ~*x  iterator: vx must be of the form
          ("str0" "str1" "str2" "str3" lst . a);
          if lst is initially empty, format "str0" under a+; otherwise,
          bind #\* successively to the elements of lst and then
          recursively format "stri" under a+, where i=1 if there is one
          element left to process, i=2 if there are two left, and i=3
          otherwise.
     ~&x  print elements of vx with ~x, separated by commas and a
          final ``and''
     ~vx  print elements of vx with ~x, separated by commas and a
          final ``or''
     ~nx  if vx is a small positive integer, print it as a word, e.g.,
          seven;
          if vx is a singleton containing a small positive integer, print
            the corresponding ordinal as a word, e.g., seventh
     ~Nx  like ~nx but the word is capitalized, e.g., Seven or Seventh
     ~tx  tab out to column vx; newline first if at or past column vx
     ~cx  vx is (n . w), print integer n right justified in field of
          width w
     ~fx  print object vx flat over as many lines as necessary
     ~Fx  same as ~f, except that subsequent lines are indented to
          start one character to the right of the first character printed
     ~sx  if vx is a symbol, print vx, breaking on hyphens (unless the
          symbol would normally be printed with surrounding vertical bar
          characters (|), in which case print as with ~fx); if vx is a
          string, print the characters in it, breaking on hyphens; else
          vx is a number, to be printed using the current print-base
     ~    tilde space: print a space
     ~_x  print vx spaces
     ~
          tilde newline: skip following whitespace
     ~%   output a newline
     ~|   output a newline unless already on left margin
     ~~   print a tilde
     ~-   if close to rightmargin, output a hyphen and newline; else
          skip this char

If x is a character, then vx is the value of #\x under the current
alist.  When we say "format str under a+" we mean recursively process
the given string under an alist obtained by appending a to the current
alist.

Note:  ~p, ~q, ~P, and ~Q are also currently supported, but are
deprecated.  These are respectively the same as ~x, ~y, ~X, and ~Y,
except that their arguments are expected to be terms, preferably
untranslated (user-level) terms, that could be printed using infix
notation in certain environments.  Infix printing is not currently
supported but may be if there is sufficient need for it.

ACL2's formatting functions print to the indicated channel, keeping
track of which column they are in.  Fmt1 can be used if the caller
knows which column the channel is in (i.e., how many characters have
been printed since the last newline).  Otherwise, fmt or fms must be
used, both of which output a newline so as to establish the column
position at 0.  Unlike Common Lisp's format routine, fmt and its
relatives break the output into lines so that, by default, an attempt
is made to avoid printing past column 77.  See
SET-FMT-HARD-RIGHT-MARGIN for a discussion of how linebreaks are
inserted and how to change the relevant default settings.

The formatting functions scan the string from left to right, printing
each successive character unless it is a tilde (~).  Upon encountering
tildes the formatters take action determined by the character or
characters immediately following the tilde.  The typical
tilde-directive is a group of three successive characters from the
string being printed.  For example, ~x0 is a 3 character
tilde-directive.  The first character in a tilde-directive is always
the tilde character itself.  The next character is called the "command"
character.  The character after that is usually taken as the name of a
"format variable" that is bound in the alist under which the string is
being printed.  Format variables are, by necessity, characters.  The
objects actually printed by a tilde-directive are the objects obtained
by looking up the command's format variables in the alist.  Typical
format variable names are 0, 1, 2, ..., 9, a, b, c, etc., and if a
tilde-directive uses the format variable 0, as in ~x0, then the
character #\0 must be bound in the alist.  Some tilde commands take no
arguments and others take more than one, so some directives are of
length two and others are longer.

It should be noted that this use of characters in the string to denote
arguments is another break from Common Lisp's format routine.  In
Common Lisp, the directives refer implicitly to the "next item to be
printed."  But in ACL2 the directives name each item explicitly with
our format variables.

The following text contains examples that can be evaluated.  To make
this process easier, we use a macro which is defined as part of ACL2
just for this documentation.  The macro is named fmx and it takes up to
eleven arguments, the first of which is a format string, str, and the
others of which are taken as the values of format variables.  The
variables used are #\0 through #\9.  The macro constructs an
appropriate alist, a, and then evaluates (fmt str a *standard-co* state
nil).

Thus,

     (fmx "Here is v0, ~x0, and here is v1, ~x1."
          (cons 'value 0)
          (cons 'value 1))

is just an abbreviation for

     (fmt "Here is v0, ~x0, and here is v1, ~x1."
          (list (cons #\0 (cons 'value 0))
                (cons #\1 (cons 'value 1)))
          *standard-co*
          state
          nil)

which returns (mv 53 state) after printing the line

        Here is v0, (VALUE . 0), and here is v1, (VALUE . 1).

We now devote special attention to three of the tilde-directives whose
use is non-obvious.

_The Case Statement_

~#x is essentially a "case statement" in the language of fmt.  The
proper form of the statement is

     ~#x~[case-0~/case-1~/ ... ~/case-k~],

where each of the case-i is a format string.  In the most common use,
the variable x has an integer value, vx, between 0 and k, inclusive.
The effect of formatting the directive is to format case-vx.

For example

     (fmx "Go ~#0~[North~/East~/South~/West~].~%" 1)

will print "Go East." followed by a newline and will return

(mv 0 state), while if you change the 1 above to 3 (the maximum legal
value), it will print "Go West."

In order to make it easier to print such phrases as "there are seven
cases" requiring agreement between subject and verb based on the number
of elements of a list, the case statement allows its variable to take a
list as its value and selects case-0 if the list has length 1 and
case-1 otherwise.

     (let ((cases '(a b c)))
       (fmx "There ~#0~[is ~n1 case~/are ~n1 cases~]."
            cases
            (length cases)))

will print "There are three cases." but if you change the

'(a b c) above simply to '(a) it will print "There is one case." and if
you change it to nil it will print "There are zero cases."

_Indirection_

Roughly speaking, ~@ will act as though the value of its argument is a
format string and splice it into the current string at the current
position.  It is often used when the phrase to be printed must be
computed.  For example,

     (let ((ev 'DEFUN))
      (fmx "~x0 is an event~@1."
           'foo
           (if (member-eq ev '(defun defstub encapsulate))
               " that may introduce a function symbol"
               "")))

will print "foo is an event that may introduce a function symbol," but
if the value of ev is changed from 'defun to 'defthm, it prints "foo is
an event."  The ~@ directive "splices" in the computed phrase (which
might be empty).  Of course, this particular example could be done with
the case statement

     ~#1~[~/ that may introduce a function symbol~]

where the value of #\1 is appropriately computed to be 0 or 1.

If the argument to ~@ is a pair, it is taken to be a format string
consed onto an alist, i.e., ("str" . a), and the alist, a, is used to
extend the current one before "str" is recursively processed.  This
feature of fmt can be used to pass around "phrases" that contain
computed contextual information in a.  The most typical use is as
"error messages."  For example, suppose you are writing a function
which does not have access to state and so cannot print an error
message.  It may nevertheless be necessary for it to signal an error to
its caller, say by returning two results, the first of which is
interpreted as an error message if non-nil.  Our convention is to use a
~@ pair to represent such messages.  For example, the error value might
be produced by the code:

     (cons
       "Error:  The instruction ~x0 is illegal when the stack is ~x1.~%"
       (list (cons #\0 (current-instruction st))
             (cons #\1 (i-stack st))))

If the current-instruction and i-stack (whatever they are) are '(popi
3) and '(a b) when the cons above is evaluated, then it produces

     '("Error:  The instruction ~x0 is illegal when the stack is ~x1.~%"
       (#\0 POPI 3)
       (#\1 A B))

and if this pair is made the value of the fmt variable 0, then ~@0 will
print

        Error:  The instruction (POPI 3) is illegal when the stack is (A B).

For example, evaluate

     (let
      ((pair
       '("Error:  The instruction ~x0 is illegal when the stack is ~x1.~%"
         (#\0 POPI 3)
         (#\1 A B))))
      (fmx "~@0" pair)).

Thus, even though the function that produced the "error" could not
print it, it could specify exactly what error message and data are to
be printed.

This example raises another issue.  Sometimes it is desirable to break
lines in your format strings so as to make your source code more
attractive.  That is the purpose of the tilde-newline directive.  The
following code produces exactly the same output as described above.

     (let ((pair '("Error:  The instruction ~x0 ~
                   is illegal when the stack is ~
                   ~x1.~%"
                   (#\0 POPI 3)
                   (#\1 A B))))
      (fmx "~@0" pair)).

Finally, observe that when ~@0 extends the current alist, alist, with
the one, a, in its argument, the bindings from a are added to the front
of alist, overriding the current values of any shared variables.  This
ensures that the variable values seen by the recursively processed
string, "str", are those from a, but if "str" uses variables not bound
in a, their values are as specified in the original alist.
Intuitively, variables bound in a are local to the processing of ("str"
. a) but "str" may use "global variables."  The example above
illustrates this because when the ~@0 is processed, #\0 is bound to the
error message pair.  But when the ~x0 in the error string is processed,
#\0 is bound to the illegal instruction.

_Iteration_

The ~* directive is used to process each element of a list.  For
example,

     (let ((lst '(a b c d e f g h))) ; a true-list whose elements we exhibit
      (fmx "~*0"
           `("Whoa!"          ; what to print if there's nothing to print
             "~x*!"           ; how to print the last element
             "~x* and "       ; how to print the 2nd to last element
             "~x*, "          ; how to print all other elements
             ,lst)))          ; the list of elements to print

will print "A, B, C, D, E, F, G and H!".  Try this example with other
true list values of lst, such as '(a b), '(a), and nil.  The
tilde-directives ~&0 and ~v0, which take a true list argument and
display its elements separated by commas and a final "and" or "or," are
implemented in terms of the more general ~*.

The ~* directive allows the 5-tuple to specify in its final cdr an
alist with which to extend the current one before processing the
individual elements.

We often use ~* to print a series of phrases, separated by suitable
punctuation, whitespace and noise words.  In such use, the ~* handles
the separation of the phrases and each phrase is generally printed by
~@.

Here is a complex example.  In the let*, below, we bind phrases to a
list of ~@ pairs and then we create a ~* 5-tuple to print out the
conjunction of the phrases with a parenthetical "finally!" if the
series is longer than 3.

     (let* ((phrases
             (list (list "simplifying with the replacement rules ~&0"
                         (cons #\0 '(rewrite-rule1
                                     rewrite-rule2
                                     rewrite-rule3)))
                   (list "destructor elimination using ~x0"
                         (cons #\0 'elim-rule))
                   (list "generalizing the terms ~&0"
                         (cons #\0 '((rev x) (app u v))))
                   (list "inducting on ~x0"
                         (cons #\0 'I))))
            (5-tuple
             (list
              "magic"                            ; no phrases
              "~@*"                              ; last phrase
              "~@*, and~#f~[~/ (finally!)~] "    ; second to last phrase
              "~@*, "                            ; other phrases
              phrases                            ; the phrases themselves
              (cons #\f
                    (if (>(length phrases) 3) 1 0))))) ;print ``finally''?
       (fmx "We did it by ~*0." 5-tuple))

This let* prints

        We did it by simplifying with the replacement rules REWRITE-RULE1,
        REWRITE-RULE2 and REWRITE-RULE3, destructor elimination using ELIM-
        RULE, generalizing the terms (REV X) and (APP U V), and (finally!)
        inducting on I.

You might wish to try evaluating the let* after removing elements of
phrases.

Most of the output produced by ACL2 is produced via fmt statements.
Thus, inspection of the source code will yield many examples.  A
complicated example is the code that explains the simplifier's work.
See :pc simplify-clause-msg1.  An ad hoc example is provided by the
function fmt-doc-example, which takes two arguments: an arbitrary true
list and state.  To see how fmt-doc-example works, :pe fmt-doc-example.

     (fmt-doc-example '(a b c d e f g h i j k l m n o p) state)

will produce the output

        Here is a true list:  (A B C D E F G H I J K L M N O P).  It has 16
        elements, the third of which is C.

        We could print each element in square brackets:
        ([A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N],
        [almost there: O], [the end: P]).  And if we wished to itemize them
        into column 15 we could do it like this
        0123456789012345
            0 (zeroth) A
            1 (first)  B
            2 (second) C
            3 (third)  D
            4 (fourth) E
            5 (fifth)  F
            6 (sixth)  G
            7 (seventh)
                       H
            8 (eighth) I
            9 (ninth)  J
           10 (tenth)  K
           11 (eleventh)
                       L
           12 (twelfth)
                       M
           13 (thirteenth)
                       N
           14 (14th)   O
           15 (15th)   P
        End of example.

and return (mv 15 state).

Finally, we should remind the reader that fmt and its subfunctions,
most importantly fmt0, are written entirely in ACL2.  We make this
comment for two reasons.  First, it illustrates the fact that quite low
level code can be efficiently written in the language.  Second, it
means that as a last resort for documentation purposes you can read the
source code without changing languages.

FMT!    :(str alist co-channel state evisc) => state

This function is nearly identical to fmt; see FMT.  The only
difference is that fmt may insert backslash (\) characters when forced
to print past the right margin in order to make the output a bit
clearer in that case.  Use fmt! instead if you want to be able to read
the forms back in.

FMT!-TO-STRING    See PRINTING-TO-STRINGS.

FMT-TO-COMMENT-WINDOW    print to the comment window

See CW for an introduction to the comment window and the usual
way to print it.

Function fmt-to-comment-window is identical to fmt1 (see FMT),
except that the channel is in essence *standard-co* and the ACL2 state
is neither an input nor an output.  An analogous function,
fmt-to-comment-window!, prints with fmt! instead of fmt, in order to
avoid insertion of backslash (\) characters for margins; also see
CW!.

     General Form:
     (fmt-to-comment-window fmt-string alist col evisc-tuple)

where these arguments are as desribed for fmt1; see FMT.

FMT-TO-STRING    See PRINTING-TO-STRINGS.