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

FULL-BOOK-NAME    book naming conventions assumed by ACL2

For this discussion we assume that the resident operating system is Unix
(trademark of AT&T), but analogous remarks apply to other operating
systems supported by ACL2, in particular, the Macintosh operating system
where `:' plays roughly the role of `/' in Unix; see PATHNAME.

ACL2 defines a "full book name" to be an "absolute filename string,"
that may be divided into contiguous sections: a "directory string", a
"familiar name" and an "extension".  See PATHNAME for the
definitions of "absolute," "filename string," and other notions
pertaining to naming files.  Below we exhibit the three sections of one
such string:

     "/usr/home/smith/project/arith.lisp"

     "/usr/home/smith/project/"           ; directory string
                             "arith"      ; familiar name
                                  ".lisp" ; extension

The sections are marked by the rightmost slash and rightmost dot, as
shown below.

     "/usr/home/smith/project/arith.lisp"
                             |     |
                             slash dot
                             |     |
     "/usr/home/smith/project/"           ; directory string
                             "arith"      ; familiar name
                                  ".lisp" ; extension

The directory string includes (and terminates with) the rightmost slash.
The extension includes (and starts with) the rightmost dot.  The dot
must be strictly to the right of the slash so that the familiar name is
well-defined and nonempty.

If you are using ACL2 on a system in which file names do not have this
form, please contact the authors and we'll see what we can do about
generalizing ACL2's conventions.

KEEP    how we know if include-book read the correct files

The certificate (see CERTIFICATE for general information) of a
certified file is divided into two parts, a portcullis and a keep.
These names come from castle lore.  The keep is the strongest and
usually tallest tower of a castle from which the entire courtyard can be
surveyed by the defenders.  The keep of a book is a list of file names
and check sums used after the book has been included, to determine if
the files read were (up to check sum) those certified.

Once the portcullis is open, include-book can enter the book and read
the event forms therein.  The non-local event forms are in fact
executed, extending the host theory.  That may read in other books.
When that has been finished, the keep of the certificate is inspected.
The keep is a list of the book names which are included (hereditarily
through all subbooks) in the certified book (including the certified
book itself) together with the check sums of the objects in those books
at the time of certification.  We compare the check sums of the books
just included to the check sums of the books stored in the keep.  If
differences are found then we know that the book or one of its subbooks
has been changed since certification.

See INCLUDE-BOOK to continue the guided tour through books.

MAKEFILES    See BOOK-MAKEFILES.

PATHNAME    introduction to filename conventions in ACL2

The notion of pathname objects from Common Lisp is not supported in
ACL2, nor is the function pathname.  However, ACL2 supports file
operations, using conventions for naming files based on those of the
Unix (trademark of AT&T) operating system, so that the character / is
used to terminate directory names.  Some file names are "absolute"
(complete) descriptions of a file or directory; others are "relative" to
the current working directory or to the connected book directory (see
CBD).  We emphasize that even for users of Windows-based systems
or Macintosh computers, ACL2 file names are in the Unix style.  We will
call these *ACL2 pathnames*, often omitting the "ACL2."

Pathnames starting with the directory separator (/) are absolute
pathnames.  All other pathnames are relative pathnames.  An exception is
in the Microsoft Windows operating system, where the drive may be
included, e.g., "c:/home/smith/acl2/book-1.lisp".  In fact, the drive
*must* be included in the portcullis of a book; see PORTCULLIS.

Consider the following examples.  The filename string

     "/home/smith/acl2/book-1.lisp"

is an absolute pathname, with top-level directory "home", under that the
directory "smith" and then the directory "acl2", and finally, within
that directory the file "book-1.lisp".  If the connected book directory
is "/home/smith/" (see CBD), then the filename string above also
corresponds to the relative filename string "acl2/book1.lisp".

PORTCULLIS    the gate guarding the entrance to a certified book

The certificate (see CERTIFICATE for general information) of a
certified file is divided into two parts, a portcullis and a keep.
These names come from castle lore.  The portcullis of a castle is an
iron grate that slides up through the ceiling of the tunnel-like
entrance.  The portcullis of a book ensures that include-book does not
start to read the book until the appropriate context has been created.

Technically, the portcullis consists of the version number of the
certifying ACL2, a list of commands used to create the "certification
world" and an alist specifying the check sums of all the books included
in that world.  The portcullis is constructed automatically by
certify-book from the world in which certify-book is called, but that
world must have certain properties described below.  After listing the
properties we discuss the issues in a more leisurely manner.

Each command in the portcullis must be either a defpkg form or an
embedded event form (see EMBEDDED-EVENT-FORM).

Consider a book to be certified.  The book is a file containing event
forms.  Suppose the file contains references to such symbols as
my-pkg::fn and acl2-arith::cancel, but that the book itself does not
create the packages.  Then a hard Lisp error would be caused merely by
the attempt to read the expressions in the book.  The corresponding
defpkgs cannot be written into the book itself because the book must be
compilable and Common Lisp compilers differ on the rules concerning the
inline definition of new packages.  The only safe course is to make all
defpkgs occur outside of compiled files.

More generally, when a book is certified it is certified within some
logical world.  That "certification world" contains not only the
necessary defpkgs but also, perhaps, function and constant definitions
and maybe even references to other books.  When certify-book creates the
certificate for a file it recovers from the certification world the
commands used to create that world from the initial ACL2 world.  Those
commands become part of the portcullis for the certified book.  In
addition, certify-book records in the portcullis the check sums (see
CHECK-SUM) of all the books included in the certification world.

Include-book presumes that it is impossible even to read the contents of
a certified book unless the portcullis can be "raised." To raise the
portcullis we must be able to execute (possibly redundantly, but
certainly without error), all of the commands in the portcullis and then
verify that the books thus included were identical to those used to
build the certification world (up to check sum).  This raising of the
portcullis must be done delicately since defpkgs are present: we cannot
even read a command in the portcullis until we have successfully
executed the previous ones, since packages are being defined.

Clearly, a book is most useful if it is certified in the most elementary
extension possible of the initial logic.  If, for example, your
certification world happens to contain a defpkg for "MY-PKG" and the
function foo, then those definitions become part of the portcullis for
the book.  Every time the book is included, those names will be defined
and will have to be either new or redundant (see
REDUNDANT-EVENTS).  But if those names were not necessary to the
certification of the book, their presence would unnecessarily restrict
the utility of the book.

See KEEP to continue the guided tour of books.

SET-CBD    to set the connected book directory

     Example Forms:
     ACL2 !>:set-cbd "/usr/home/smith/"
     ACL2 !>:set-cbd "my-acl2/books"

See CBD for a description of the connected book directory.

     General Form:
     (set-cbd str)

where str is a nonempty string that represents the desired directory
(see PATHNAME).  This command sets the connected book directory
(see CBD) to the string representing the indicated directory.
Thus, this command may determine which files are processed by
include-book and certify-book commands typed at the top-level.  However,
the cbd is also temporarily set by those two book processing commands.

IMPORTANT: Pathnames in ACL2 are in the Unix (trademark of AT&T) style.
That is, the character "/" separates directory components of a pathname,
and pathnames are absolute when they start with this character, and
relative otherwise.  See PATHNAME.

UNCERTIFIED-BOOKS    invalid certificates and uncertified books

Include-book has a special provision for dealing with uncertified books:
If the file has no certificate or an invalid certificate (i.e., one
whose check sums describe files other than the ones actually read), a
warning is printed and the book is otherwise processed as though it were
certified and had an open portcullis.  (For details see BOOKS,
see CERTIFICATE, and see PORTCULLIS.)

This can be handy, but it can have disastrous consequences.

The provision allowing uncertified books to be included can have
disastrous consequences, ranging from hard lisp errors, to damaged
memory, to quiet logical inconsistency.

It is possible for the inclusion of an uncertified book to render the
logic inconsistent.  For example, one of its non-local events might be
(defthm t-is-nil (equal t nil)).  It is also possible for the inclusion
of an uncertified book to cause hard errors or breaks into raw Common
Lisp.  For example, if the file has been edited since it was certified,
it may contain too many open parentheses, causing Lisp to read past "end
of file." Similarly, it might contain non-ACL2 objects such as 3.1415 or
ill-formed event forms that cause ACL2 code to break.

Even if a book is perfectly well formed and could be certified (in a
suitable extension of ACL2's initial world), its uncertified inclusion
might cause Lisp errors or inconsistencies!  For example, it might
mention packages that do not exist in the host world.  The portcullis of
a certified book ensures that the correct defpkgs have been admitted,
but if a book is read without actually raising its portcullis, symbols
in the file, e.g., acl2-arithmetic::fn, could cause "unknown package"
errors in Common Lisp.  Perhaps the most subtle disaster occurs if the
host world does have a defpkg for each package used in the book but the
host defpkg imports different symbols than those required by the
portcullis.  In this case, it is possible that formulas which were
theorems in the certified book are non-theorems in the host world, but
those formulas can be read without error and will then be quietly
assumed.

In short, if you include an uncertified book, *all bets are off*
regarding the validity of the future behavior of ACL2.

That said, it should be noted that ACL2 is pretty tough and if errors
don't occur, the chances are that deductions after the inclusion of an
uncertified book are probably justified in the (possibly inconsistent)
logical extension obtained by assuming the admissibility and validity of
the definitions and conjectures in the book.

BREAK-REWRITE    the read-eval-print loop entered to monitor rewrite rules

ACL2 allows the user to monitor the application of rewrite rules.  When
monitored rules are about to be tried by the rewriter, an interactive
break occurs and the user is allowed to watch and, in a limited sense,
control the attempt to apply the rule.  This interactive loop, which is
technically just a call of the standard top-level ACL2 read-eval-print
loop, ld, on a "wormhole state" (see WORMHOLE), is called
"break-rewrite."  While in break-rewrite, certain keyword commands are
available for accessing information about the context in which the lemma
is being tried.  These keywords are called break-rewrite "commands."

To abort from inside break-rewrite at any time, execute sharpsign-period
(#.).

For further information, see the related :doc topics listed below.

As explained in the documentation for monitor, it is possible to cause
the ACL2 rewriter to monitor the attempted application of selected
rules.  When such a rule is about to be tried, the rewriter evaluates
its break condition and if the result is non-nil, break-rewrite is
entered.

Break-rewrite permits the user to inspect the current state by
evaluating break-rewrite commands.  Type :help in break-rewrite to see
what the break-rewrite commands are.  However, break-rewrite is actually
just a call of the general ACL2 read-eval-print loop, ld, on a certain
state and the break-rewrite commands are simply aliases provided by the
ld-special ld-keyword-aliases.  See LD for details about this
read-eval-print loop.  Thus, with a few exceptions, anything you can do
at the ACL2 top-level can be done within break-rewrite.  For example,
you can evaluate arbitrary expressions, use the keyword command hack,
access documentation, print events, and even define functions and prove
theorems.  However, the "certain state" upon which ld was called is a
"wormhole state" (see WORMHOLE) because break-rewrite is not
allowed to have any effect upon the behavior of rewrite.  What this
means, very roughly but understandably, is that break-rewrite operates
on a copy of the state being used by rewrite and when break-rewrite
exits the wormhole closes and the state "produced" by break-rewrite
disappears.  Thus, break-rewrite lets you query the state of the
rewriter and even do experiments involving proofs, etc., but these
experiments have no effect on the ongoing proof attempt.

When you first enter break-rewrite a simple herald is printed such as:

     (3 Breaking (:rewrite lemma12) on (delta a (+ 1 j)):

The integer after the open parenthesis indicates the depth of nested
break-rewrite calls.  In this discussion we use 3 consistently for this
integer.  Unless you abort or somehow enter unbalanced parentheses into
the script, the entire session at a given depth will be enclosed in
balanced parentheses, making it easy to skip over them in Emacs.

You then will see the break-rewrite prompt:

     3 ACL2 !>

The leading integer is, again, the depth.  Because breaks often occur
recursively it is convenient always to know the level with which you are
interacting.

You may type arbitrary commands as in the top-level ACL2 loop.  For
example, you might type:

     3 ACL2 !>:help

or

     3 ACL2 !>:pe lemma12

More likely, upon entering break-rewrite you will determine the context
of the attempted application.  Here are some useful commands:

     3 ACL2 >:target           ; the term being rewritten
     3 ACL2 >:unify-subst      ; the unifying substitution
     3 ACL2 >:path             ; the stack of goals pursued by the rewriter
                               ; starting at the top-level clause being simplified
                               ; and ending with the current application

At this point in the interaction the system has not yet tried to apply
the monitored rule.  That is, it has not tried to establish the
hypotheses, considered the heuristic cost of backchaining, rewritten the
right-hand side of the conclusion, etc.  When you are ready for it to
try the rule you can type one of several different "proceed" commands.
The basic proceed commands are :ok, :go, and :eval.

     :ok

exits break-rewrite without further interaction.  When break-rewrite
exits it prints "3)", closing the parenthesis that opened the level 3
interaction.

     :go

exits break-rewrite without further interaction, but prints out the
result of the application attempt, i.e., whether the application
succeeded, if so, what the :target term was rewritten to, and if not why
the rule was not applicable.

     :eval

causes break-rewrite to attempt to apply the rule but interaction at
this level of break-rewrite resumes when the attempt is complete.  When
control returns to this level of break-rewrite a message indicating the
result of the application attempt (just as in :go) is printed, followed
by the prompt for additional user input.

Generally speaking, :ok and :go are used when the break in question is
routine or uninteresting and :eval is used when the break is one that
the user anticipates is causing trouble.  For example, if you are trying
to determine why a lemma isn't being applied to a given term and the
:target of the current break-rewrite is the term in question, you would
usually :eval the rule and if break-rewrite reports that the rule failed
then you are in a position to determine why, for example by carefully
inspecting the :type-alist of governing assumptions or why some
hypothesis of the rule could not be established.

It is often the case that when you are in break-rewrite you wish to
change the set of monitored runes.  This can be done by using :monitor
and :unmonitor as noted above.  For example, you might want to monitor a
certain rule, say hyp-reliever, just when it is being used while
attempting to apply another rule, say main-lemma.  Typically then you
would monitor main-lemma at the ACL2 top-level, start the proof-attempt,
and then in the break-rewrite in which main-lemma is about to be tried,
you would install a monitor on hyp-reliever.  If during the ensuing
:eval hyp-reliever is broken you will know it is being used under the
attempt to apply main-lemma.

However, once hyp-reliever is being monitored it will be monitored even
after main-lemma has been tried.  That is, if you let the proof attempt
proceed then you may see many other breaks on hyp-reliever, breaks that
are not "under" the attempt to apply main-lemma.  One way to prevent
this is to :eval the application of main-lemma and then :unmonitor
hyp-reliever before exiting.  But this case arises so often that ACL2
supports several additional "flavors" of proceed commands.

:Ok!, :go!, and :eval! are just like their counterparts (:ok, :go, and
:eval, respectively), except that while processing the rule that is
currently broken no runes are monitored.  When consideration of the
current rule is complete, the set of monitored runes is restored to its
original setting.

:Ok$, :go$, and :eval$ are similar but take an additional argument which
must be a list of runes.  An example usage of :eval$ is

     3 ACL2 !>:eval$ ((:rewrite hyp-reliever))

These three commands temporarily install unconditional breaks on the
runes listed, proceed with the consideration of the currently broken
rule, and then restore the set of monitored rules to its original
setting.

Thus, there are nine ways to proceed from the initial entry into
break-rewrite although we often speak as though there are two, :ok and
:eval, and leave the others implicit.  We group :go with :ok because in
all their flavors they exit break-rewrite without further interaction
(at the current level).  All the flavors of :eval require further
interaction after the rule has been tried.

To abort a proof attempt and return to the top-level of ACL2 you may at
any time type #. (that is, number-sign followed by a period) followed by
a carriage return.

We now address ourselves to the post-:eval interaction with
break-rewrite.  As noted, that interaction begins with break-rewrite's
report on the results of applying the rule: whether it worked and either
what it produced or why it failed.  This information is also printed by
certain keyword commands available after :eval, namely :wonp,
:rewritten-rhs, and :failure-reason.  In addition, by using brr@ (see
BRR@.) you can obtain this information in the form of
ACL2 data objects.  This allows the development of more sophisticated
"break conditions"; see MONITOR for examples.  In this
connection we point out the macro form (ok-if term).  See OK-IF.
This command exits break-rewrite if term evaluates to non-nil and
otherwise does not exit.  Thus it is possible to define macros that
provide other kinds of exits from break-rewrite.  The only way to exit
break-rewrite after :eval is :ok (or, equivalently, the use of ok-if).

ACL2 users who wish to know more about break-rewrite so that they can
develop more convenient ways to monitor rules are encouraged to speak to
J Moore.

The rest of this documentation discusses a few implementation details of
break-rewrite and may not be interesting to the typical user.

There is no ACL2 function named break-rewrite.  It is an illusion
created by appropriate calls to two functions named brkpt1 and brkpt2.
As previously noted, break-rewrite is ld operating on a wormhole state.
One might therefore wonder how break-rewrite can apply a rule and then
communicate the results back to the rewriter running in the external
state.  The answer is that it cannot.  Nothing can be communicated
through a wormhole.  In fact, brkpt1 and brkpt2 are each calls of ld
running on wormhole states.  Brkpt1 implements the pre-:eval
break-rewrite and brkpt2 implements the post-:eval break-rewrite.  The
rewriter actually calls brkpt1 before attempting to apply a rule and
calls brkpt2 afterwards.  In both cases, the rewriter passes into the
wormhole the relevant information about the current context.  Logically
brkpt1 and brkpt2 are no-ops and rewrite ignores the nil they return.
But while control is in them the execution of rewrite is suspended and
cannot proceed until the break-rewrite interactions complete.

This design causes a certain anomoly that might be troubling.  Suppose
that inside break-rewrite before :evaling a rule (i.e., in the brkpt1
wormhole state) you define some function, foo.  Suppose then you :eval
the rule and eventually control returns to break-rewrite (i.e., to
brkpt2 on a wormhole state with the results of the application in it).
You will discover that foo is no longer defined!  That is because the
wormhole state created during your pre-:eval interaction is lost when we
exit the wormhole to resume the proof attempt.  The post-:eval wormhole
state is in fact identical to the initial pre-:eval state (except for
the results of the application) because rewrite did not change the
external state and both wormhole states are copies of it.

There is a lot more to know about break-rewrite, most of which is fairly
easy to learn from looking at the code, since it is all expressed in
ACL2.  Feel free to ask questions of J Moore.

BREAK-LEMMA    a quick introduction to breaking rewrite rules in ACL2

     Example:
     :brr t                          ; if you haven't done that yet
     :monitor (:rewrite lemma12) t   ; to install a break point on the
                                     ; rule named (:rewrite lemma12)

ACL2 does not support Nqthm's break-lemma but supports a very similar
and more powerful break facility.  Suppose some proof is failing;
apparently some particular rule is not being used and you wish to learn
why.  Then you need the ACL2 break-rewrite facility.  See
BREAK-REWRITE and all of its associated :doc topics for details.  The
following basic steps are required.

(1) To enable the "break rewrite" feature, you must first execute

     ACL2 !>:brr t

at the top-level of ACL2.  Equivalently, evaluate (brr t).
Break-rewrite stays enabled until you disable it with (brr nil).  When
break-rewrite is enabled the ACL2 rewriter will run slower than normal
but you will be able to monitor the attempts to apply specified rules.

(2) Decide what runes (see RUNE) you wish to monitor.  For
example, you might want to know why (:rewrite lemma12 . 2) is not being
used in the attempted proof.  That, by the way, is the name of the
second rewrite rule generated from the event named lemma12.

The command

     ACL2 !>:monitor (:rewrite lemma12 . 2) t

will install an "unconditional" break point on that rule.  The "t" at
the end of the command means it is unconditional, i.e., a break will
occur every time the rule is tried.  ACL2 supports conditional breaks
also, in which case the t is replaced by an expression that evaluates to
non-nil when you wish for a break to occur.  See MONITOR.  The
above keyword command is, of course, equivalent to

     ACL2 !>(monitor '(:rewrite lemma12 . 2) t)

which you may also type.  You may install breaks on as many rules as you
wish.  You must use monitor on each rule.  You may also change the break
condition on a rule with monitor.  Use unmonitor (see UNMONITOR)
to remove a rule from the list of monitored rules.

(3) Then try the proof again.  When a monitored rule is tried by the
rewriter you will enter an interactive break, called break-rewrite.  See
BREAK-REWRITE for a detailed description.  Very simply,
break-rewrite lets you inspect the context of the attempted application
both before and after the attempt.  When break-rewrite is entered it
will print out the "target" term being rewritten.  If you type :go
break-rewrite will try the rule and then exit, telling you (a) whether
the rule was applied, (b) if so, how the target was rewritten, and (c)
if not, why the rule failed.  There are many other commands.  See
BRR-COMMANDS.

(4) When you have finished using the break-rewrite feature you should
disable it to speed up the rewriter.  You can disable it with

     ACL2 !>:brr nil

The list of monitored rules and their break conditions persists but is
ignored.  If you enable break-rewrite later, the list of monitored rules
will be displayed and will be used again by rewrite.

You should disable the break-rewrite feature whenever you are not
intending to use it, even if the list of monitored rules is empty,
because the rewriter is slowed down as long as break-rewrite is enabled.

If you get a stack overflow, see CW-GSTACK.

BRR    to enable or disable the breaking of rewrite rules

     Example:
     :brr t       ; enable
     :brr nil     ; disable

     General Form:
     (brr flg)

where flg evaluates to t or nil.  This function modifies state so that
the attempted application of certain rewrite rules are "broken." "Brr"
stands for "break-rewrite" and can be thought of as a mode with two
settings.  The normal mode is "disabled."

When brr mode is "enabled" the ACL2 rewriter monitors the attempts to
apply certain rules and advises the user of those attempts by entering
an interactive wormhole break.  From within this break the user can
watch selected application attempts.  See BREAK-REWRITE.  The
user can also interact with the system during brr breaks via
brr-commands.

The rules monitored are selected by using the monitor and unmonitor
commands.  It is possible to break a rune "conditionally" in the sense
that an interactive break will occur only if a specified predicate is
true of the environment at the time of the attempted application.  See
MONITOR and see UNMONITOR.

Even if a non-empty set of rules has been selected, no breaks will occur
unless brr mode is enabled.  Thus, the first time in a session that you
wish to monitor a rewrite rule, use :brr t to enable brr mode.
Thereafter you may select runes to be monitored with monitor and
unmonitor with the effect that whenever monitored rules are tried (and
their break conditions are met) an interactive break will occur.  Be
advised that when brr mode is enabled the rewriter is somewhat slower
than normal.  Furthermore, that sluggishness persists even if no runes
are monitored.  You may regain normal performance -- regardless of what
runes are monitored -- by disabling brr mode with :brr nil.

Why isn't brr mode disabled automatically when no runes are monitored?
More generally, why does ACL2 have brr mode at all?  Why not just test
whether there are monitored runes?  If you care about the answers, see
WHY-BRR.

BRR Mode and Console Interrupts: If the system is operating in brr mode
and you break into raw Lisp (as by causing a console interrupt or
happening upon a signalled Lisp error; see BREAKS), the normal
way to quit from such a break (:q in GCL, :reset in Allegro CL, and q in
CMU CL) will return to the innermost ACL2 read-eval-print loop.  This
may or may not be the top-level of your ACL2 session!  In particular, if
the break happens to occur while ACL2 is within the brr environment (in
which it is preparing to read brr-commands), the abort will merely
return to that brr environment.  Upon exiting that environment, normal
theorem proving is continued (and the brr environment may be entered
again in response to subsequent monitored rule applications).  Before
returning to the brr environment, ACL2 "cleans up" from the interrupted
brr processing.  However, it is not possible (given the current
implementation) to clean up perfectly.  This may have two side-effects.
First, the system may occasionally print the self-explanatory "Cryptic
BRR Message 1" (or 2), informing you that the system has attempted to
recover from an aborted brr environment.  Second, it is possible that
subsequent brr behavior in that proof will be erroneous because the
cleanup was done incorrectly.  The moral is that you should not trust
what you learn from brr if you have interrupted and aborted brr
processing during the proof.  These issues do not affect the behavior or
soundness of the theorem prover.

BRR-COMMANDS    Break-Rewrite Commands

     #.              abort to ACL2 top-level
     :target         term being rewritten
     :unify-subst    substitution making :lhs equal :target
     :hyps           hypotheses of the rule
     :hyp i          ith hypothesis of the rule
     :lhs            left-hand side of rule's conclusion
     :rhs            right-hand side of rule's conclusion
     :type-alist     type assumptions governing :target
     :initial-ttree  ttree before :eval (see TTREE)
     :ancestors      negations of backchaining hypotheses being pursued
     :wonp           indicates if application succeed (after :eval)
     :rewritten-rhs  rewritten :rhs (after :eval)
     :final-ttree    ttree after :eval (see TTREE)
     :failure-reason reason rule failed (after :eval)
     :path           rewrite's path from top clause to :target
     :frame i        ith frame in :path
     :top            top-most frame in :path
     :ok             exit break
     :go             exit break, printing result
     :eval           try rule and re-enter break afterwards
     :ok!            :ok but no recursive breaks
     :go!            :go but no recursive breaks
     :eval!          :eval but no recursive breaks
     :ok$ runes      :ok with runes monitored during recursion
     :go$ runes      :go with runes monitored during recursion
     :eval$ runes    :eval with runes monitored during recursion
     :help           this message
     :standard-help  :help message from ACL2 top-level

Break-rewrite is just a call of the standard ACL2 read-eval-print loop,
ld, on a "wormhole" state.  Thus, you may execute most commands you
might normally execute at the top-level of ACL2.  However, all state
changes you cause from within break-rewrite are lost when you exit or
:eval the rule.  You cannot modify stobjs from within the break.  See
BREAK-REWRITE for more details and see LD for general
information about the standard ACL2 read-eval-print loop.

BRR@    to access context sensitive information within break-rewrite

     Example:
     (brr@ :target)      ; the term being rewritten
     (brr@ :unify-subst) ; the unifying substitution

     General Form:
     (brr@ :symbol)

where :symbol is one of the following keywords.  Those marked with *
probably require an implementor's knowledge of the system to use
effectively.  They are supported but not well documented.  More is said
on this topic following the table.

     :symbol             (brr@ :symbol)
     -------             ---------------------

     :target             the term to be rewritten.  This term is an
                         instantiation of the left-hand side of the
                         conclusion of the rewrite-rule being broken.
                         This term is in translated form!  Thus, if
                         you are expecting (equal x nil) -- and your
                         expectation is almost right -- you will see
                         (equal x 'nil); similarly, instead of (cadr a)
                         you will see (car (cdr a)).  In translated
                         forms, all constants are quoted (even nil, t,
                         strings and numbers) and all macros are
                         expanded.

     :unify-subst        the substitution that, when applied to :target,
                         produces the left-hand side of the rule being
                         broken.  This substitution is an alist pairing
                         variable symbols to translated (!) terms.

     :wonp               t or nil indicating whether the rune was
                         successfully applied.  (brr@ :wonp) returns
                         nil if evaluated before :EVALing the rule.

     :rewritten-rhs      the result of successfully applying the rule
                         or else nil if (brr@ :wonp) is nil.  The result
                         of successfully applying the rule is always a
                         translated (!) term and is never nil.

     :failure-reason     some non-nil lisp object indicating why the rule
                         was not applied or else nil.  Before the rule is
                         :EVALed, (brr@ :failure-reason) is nil.  After
                         :EVALing the rule, (brr@ :failure-reason) is nil
                         if (brr@ :wonp) is t.  Rather than document the
                         various non-nil objects returned as the failure
                         reason, we encourage you simply to evaluate
                         (brr@ :failure-reason) in the contexts of interest.
                         Alternatively, study the ACL2 function tilde-@-
                         failure-reason-phrase.

     :lemma           *  the rewrite rule being broken.  For example,
                         (access rewrite-rule (brr@ :lemma) :lhs) will
                         return the left-hand side of the conclusion
                         of the rule.

     :type-alist      *  a display of the type-alist governing :target.
                         Elements on the displayed list are of the form
                         (term type), where term is a term and type
                         describes information about term assumed to hold
                         in the current context.  The type-alist may be
                         used to determine the current assumptions, e.g.,
                         whether A is a CONSP.

     :ancestors       *  a stack of frames indicating the backchain history
                         of the current context.  The theorem prover is in
                         the process of trying to establish each hypothesis
                         in this stack.  Thus, the negation of each hypothesis
                         can be assumed false.  Each frame also records the
                         rules on behalf of which this backchaining is being
                         done and the weight (function symbol count) of the
                         hypothesis.  All three items are involved in the
                         heuristic for preventing infinite backchaining.
                         Exception:  Some frames are "binding hypotheses"
                         (equal var term) or (equiv var (double-rewrite term))
                         that bind variable var to the result of rewriting
                         term.

     :gstack          *  the current goal stack.  The gstack is maintained
                         by rewrite and is the data structure printed as the
                         current "path."  Thus, any information derivable
                         from the :path brr command is derivable from gstack.
                         For example, from gstack one might determine that
                         the current term is the second hypothesis of a
                         certain rewrite rule.

In general brr@-expressions are used in break conditions, the
expressions that determine whether interactive breaks occur when
monitored runes are applied.  See MONITOR.  For example, you
might want to break only those attempts in which one particular term is
being rewritten or only those attempts in which the binding for the
variable a is known to be a consp.  Such conditions can be expressed
using ACL2 system functions and the information provided by brr@.
Unfortunately, digging some of this information out of the internal data
structures may be awkward or may, at least, require intimate knowledge
of the system functions.  But since conditional expressions may employ
arbitrary functions and macros, we anticipate that a set of convenient
primitives will gradually evolve within the ACL2 community.  It is to
encourage this evolution that brr@ provides access to the *'d data.

MONITOR    to monitor the attempted application of a rule name

     Example:
     (monitor '(:rewrite assoc-of-app) 't)
     :monitor (:rewrite assoc-of-app) t
     :monitor (:definition app) (equal (brr@ :target) '(app c d))

     General Form:
     (monitor rune term)

where rune is a rune and term is a term, called the "break condition."
Rune must be either a :rewrite rune or a :definition rune.

When a rune is monitored any attempt to apply it may result in an
interactive break in an ACL2 "wormhole state." There you will get a
chance to see how the application proceeds.  See BREAK-REWRITE
for a description of the interactive loop entered.  Whether an
interactive break occurs depends on the value of the break condition
expression associated with the monitored rune.

NOTE: Some :rewrite rules are considered "simple abbreviations"; see
SIMPLE.  These can be be monitored, but only at certain times
during the proof.  Monitoring is carried out by code inside the rewriter
but abbreviation rules may be applied by a special purpose simplifier
inside the so-called *preprocess* phase of a proof.  If you desire to
monitor an abbreviation rule, a warning will be printing suggesting that
you may want to supply the hint :DO-NOT '(PREPROCESS); see
HINTS.  Without such a hint, an abbreviation rule can be applied
during the preprocess phase of a proof, and no such application will
cause an interactive break.

To remove a rune from the list of monitored runes, use unmonitor.  To
see which runes are monitored and what their break conditions are,
evaluate (monitored-runes).

Monitor, unmonitor and monitored-runes are macros that expand into
expressions involving state.  While these macros appear to return the
list of monitored runes this is an illusion.  They all print monitored
rune information to the comment window and then return error triples
instructing ld to print nothing.  It is impossible to return the list of
monitored runes because it exists only in the wormhole state with which
you interact when a break occurs.  This allows you to change the
monitored runes and their conditions during the course of a proof
attempt without changing the state in which the the proof is being
constructed.

Unconditional break points are obtained by using the break condition t.
We now discuss conditional break points.  The break condition, expr,
must be a term that contains no free variables other than state and that
returns a single non-state result.  In fact, the result should be nil,
t, or a true list of commands to be fed to the resulting interactive
break.  Whenever the system attempts to use the associated rule, expr is
evaluated in the wormhole interaction state.  A break occurs only if the
result of evaluating expr is non-nil.  If the result is a true list,
that list is appended to the front of standard-oi and hence is taken as
the initial user commands issued to the interactive break.

In order to develop effective break conditions it must be possible to
access context sensitive information, i.e., information about the
context in which the monitored rune is being tried.  The brr@ macro may
be used in break conditions to access such information as the term being
rewritten and the current governing assumptions.  This information is
not stored in the proof state but is transferred into the wormhole state
when breaks occur.  The macro form is (brr@ :sym) where :sym is one of
several keyword symbols, including :target (the term being rewritten),
:unify-subst (the substitution that instantiates the left-hand side of
the conclusion of the rule so that it is the target term), and
:type-alist (the governing assumptions).  See BRR@.

For example,

     ACL2 !>:monitor (:rewrite assoc-of-app)
                     (equal (brr@ :target) '(app a (app b c)))

will monitor (:rewrite assoc-of-app) but will cause an interactive break
only when the target term, the term being rewritten, is (app a (app b
c)).

Because break conditions are evaluated in the interaction environment,
the user developing a break condition for a given rune can test
candidate break conditions before installing them.  For example, suppose
an unconditional break has been installed on a rune, that an interactive
break has occurred and that the user has determined both that this
particular application is uninteresting and that many more such
applications will likely occur.  An appropriate response would be to
develop an expression that recognizes such applications and returns nil.
Of course, the hard task is figuring out what makes the current
application uninteresting.  But once a candidate expression is
developed, the user can evaluate it in the current context simply to
confirm that it returns nil.

Recall that when a break condition returns a non-nil true list that list
is appended to the front of standard-oi.  For example,

     ACL2 !>:monitor (:rewrite assoc-of-app) '(:go)

will cause (:rewrite assoc-of-app) to be monitored and will make the
break condition be '(:go).  This break condition always evaluates the
non-nil true list (:go).  Thus, an interactive break will occur every
time (:rewrite assoc-of-app) is tried.  The break is fed the command
:go.  Now the command :go causes break-rewrite to (a) evaluate the
attempt to apply the lemma, (b) print the result of that attempt, and
(c) exit from the interactive break and let the proof attempt continue.
Thus, in effect, the above :monitor merely "traces" the attempted
applications of the rune but never causes an interactive break requiring
input from the user.

It is possible to use this feature to cause a conditional break where
the effective break condition is tested *after* the lemma has been
tried.  For example:

     ACL2 !>:monitor (:rewrite lemma12)
                     '(:unify-subst
                       :eval$ nil
                       :ok-if (or (not (brr@ :wonp))
                                  (not (equal (brr@ :rewritten-rhs) '(foo a))))
                       :rewritten-rhs)

causes the following behavior when (:rewrite lemma12) is tried.  A break
always occurs, but it is fed the commands above.  The first,
:unify-subst, causes break-rewrite to print out the unifying
substitution.  Then in response to :eval$ nil the lemma is tried but
with all runes temporarily unmonitored.  Thus no breaks will occur
during the rewriting of the hypotheses of the lemma.  When the attempt
has been made, control returns to break-rewrite (which will print the
results of the attempt, i.e., whether the lemma was applied, if so what
the result is, if not why it failed).  The next command, the :ok-if with
its following expression, is a conditional exit command.  It means exit
break-rewrite if either the attempt was unsuccessful, (not (brr@
:wonp)), or if the result of the rewrite is any term other than (foo a).
If this condition is met, the break is exited and the remaining break
commands are irrelevant.  If this condition is not met then the next
command, :rewritten-rhs, prints the result of the application (which in
this contrived example is known to be (foo a)).  Finally, the list of
supplied commands is exhausted but break-rewrite expects more input.
Therefore, it begins prompting the user for input.  The end result,
then, of the above :monitor command is that the rune in question is
elaborately traced and interactive breaks occur whenever it rewrites its
target to (foo a).

We recognize that the above break condition is fairly arcane.  We
suspect that with experience we will develop some useful idioms.  For
example, it is straightforward now to define macros that monitor runes
in the ways suggested by the following names: trace-rune,
break-if-target-is, and break-if-result-is.  For example, the last could
be defined as

     (defmacro break-if-result-is (rune term)
       `(monitor ',rune
                 '(quote (:eval :ok-if
                                (not (equal (brr@ :rewritten-rhs) ',term))))))

(Note however that the submitted term must be in translated form.)

Since we don't have any experience with this kind of control on lemmas
we thought it best to provide a general (if arcane) mechanism and hope
that the ACL2 community will develop the special cases that we find most
convenient.

MONITORED-RUNES    print the monitored runes and their break conditions

     Example and General Form:
     :monitored-runes

This macro prints a list, each element of which is of the form (rune
expr), showing each monitored rune and its current break condition.

OK-IF    conditional exit from break-rewrite

     Example Form:
     :ok-if (null (brr@ :wonp))

     General Form:
     :ok-if expr

where expr is a term involving no free variables other than state and
returning one non-state result which is treated as Boolean.  This form
is intended to be executed from within break-rewrite (see
BREAK-REWRITE).

Consider first the simple situation that the (ok-if term) is a command
read by break-rewrite.  Then, if the term is non-nil, break-rewrite
exits and otherwise it does not.

More generally, ok-if returns an ACL2 error triple (mv erp val state).
(See LD for more on error triples.)  If any form being evaluated
as a command by break-rewrite returns the triple returned by (ok-if
term) then the effect of that form is to exit break-rewrite if term is
non-nil.  Thus, one might define a function or macro that returns the
value of ok-if expressions on all outputs and thus create a convenient
new way to exit break-rewrite.

The exit test, term, generally uses brr@ to access context sensitive
information about the attempted rule application.  See BRR@.
Ok-if is useful inside of command sequences produced by
break conditions.  See MONITOR.  :ok-if is most useful after an
:eval command has caused break-rewrite to try to apply the rule because
in the resulting break environment expr can access such things as
whether the rule succeeded, if so, what term it produced, and if not,
why.  There is no need to use :ok-if before :evaling the rule since the
same effects could be achieved with the break condition on the rule
itself.  Perhaps we should replace this concept with :eval-and-break-if?
Time will tell.

SET-BRR-TERM-EVISC-TUPLE    controls printing of terms inside the break-rewrite loop

This macro controls printing of terms inside the break-rewrite loop (see
BREAK-REWRITE).

     Examples:
     (set-brr-term-evisc-tuple nil) ; default (inside brr)
     (set-brr-term-evisc-tuple '(nil 3 4 nil))

The first of the examples above restores the break-rewrite state to one
in which terms are printed in full.  The second sets the print-level to
3 and the print-length to 4, to replace substructures deeper than 3 by
"#" and those longer than 4 by "..."; see see LD-EVISC-TUPLE for
information about the shape of the argument of this macro, which is
evaluated.

This macro can be executed either inside a break from break-rewrite, or
at the top level.  Its effect will persist, except potentially when you
execute "#." to exit break-rewrite.

Here is an example showing the effect of this macro.

     1 ACL2 >:unify-subst
          X : (CONS A
                    (CONS B
                          (CONS C
                                (CONS D (CONS E (CONS F (CONS G 'NIL)))))))
     1 ACL2 >(set-brr-term-evisc-tuple (evisc-tuple 3 4 nil nil))
     <state>
     1 ACL2 >:unify-subst
          X : (CONS A (CONS B (CONS C #)))
     1 ACL2 >