Note-2-7-new-functionality
ACL2 Version 2.7 Notes on New Functionality
ACL2 now has a more powerful technique for relieving a :rewrite or :linear rule's hypothesis that contains free
variables. A new documentation section has been written describing the
handling free variables in rules; see free-variables. In brief, the
primary change is that when a free-variable match for the current hypothesis
fails to allow subsequent hypotheses to be relieved, then additional matches
may be attempted until they have all been tried. Also see rule-classes (discussion of :match-free). Also see set-match-free-error, see set-match-free-default, and see add-match-free-override for interfaces provided to the user for controlling
the way ACL2 deals with free variables in hypotheses. We thank Rob Sumners
for several helpful discussions about the designs of those interfaces, as well
as Eric Smith and Robert Krug for helpful related discussions. Robert Krug
also found a performance bug in a preliminary version, for which we are
grateful.
WARNING: Book certification attempts may take much longer now that, by
default, ACL2 looks for more free variable matches (see paragraph just above).
You can get the old behavior by inserting the form
(set-match-free-default :once)
just after the initial in-package form. However, rules from
included books that have free variables can still slow down certification.
This can be fixed by inserting
(add-match-free-override :once t)
before the first event in the file that generates a proof.
Forward-chaining has been made more powerful in the presence of free
variables (see free-variables), thanks to a contribution by Erik
Reeber. Both before and now, when an attempt is made to relieve (prove) a
hypothesis of a :forward-chaining rule in the case that at least one
variable in that hypothesis is not yet bound, ACL2 looks in the current
context for an instance of that hypothesis. If it finds one, then it binds
the unbound variables and continues to the next hypothesis. What is new is
that ACL2 can now look for multiple instances of that hypothesis. Consider
the following example; an explanation is below.
(encapsulate (((op * *) => *))
(local (defun op (x y) (< x y)))
(defthm transitivity-of-op
(implies (and (op x y) (op y z)) (op x z))
:rule-classes :forward-chaining))
; fails in Version_2.6; succeeds in in Version_2.7
(thm (implies (and (op a b) (op b c) (op b e)) (op a c)))
Before Version_2.7, the proof of the thm above fails. When the
:forward-chaining rule transitivity-of-op binds x to a and
y to b, it then looks for an instance of (op y z) in the
current context, with y bound to b but z unbound. It happens
to find (op b e) before (op b c), and it then adds (op a e) to
the context. But starting with Version_2.7, it continues to look for
additional instances and finds (op b c) in the context as well, chaining
forward to (op a c) and thus proving the theorem.
A new macro, bind-free, provides a simple way to get much or most
of the power of metafunctions. Thanks to Eric Smith for coming up with
the idea and to Robert Krug for providing an implementation (which we modified
only very slightly) and documentation. See bind-free and see bind-free-examples.
With the addition of bind-free (mentioned above), syntaxp
has become a macro, although that change should be transparent to the user.
More importantly, the argument of syntaxp may now refer to variables
mfc and state, giving syntaxp some of the power of extended
metafunctions; see syntaxp and see extended-metafunctions.
Thanks to Robert Krug for implementing that extension. Also, the argument of
syntaxp may now include calls of :program mode functions.
See syntaxp and see syntaxp-examples (thanks to Robert Krug for
updating the former and creating the latter documentation).
The linear-arithmetic decision procedure (see linear-arithmetic) has
now been extended so that ACL2 can reason about non-linear arithmetic as well
(see non-linear-arithmetic for how to turn on this feature). We thank
Robert Krug for the initial implementation of this, and Eric Smith for finding
a couple of bugs in it.
Some trace utilities have been made available in the ACL2 loop.
- Function trace$ (and also untrace$) calls the
corresponding underlying Lisp routine trace (and untrace), which
however continues (as it has for some time) to be enhanced for GCL and Allegro
CL.
- Macro open-trace-file causes trace output to go to a specified
file. Macro close-trace-file causes trace output to go to the screen
(which is the default).
- Macro with-error-trace (or, wet for short) causes a backtrace
to be written out for many failures, including guard violations. See trace, see trace$, and see :DOC wet [** NOTE: eliminated after
Version 3.3].
A new theory, minimal-theory has been provided (see theories). It can be particularly useful for speeding up proofs involving
:use hints.
New events defund and defthmd behave exactly like
defun and defthm, respectively, except that these new events
disable the new name.
The new macro with-output can be used to suppress output that would
normally result from evaluation of a form.
The form (pstack) can give the user an idea of what the
prover has been up to during a proof, or after a user-aborted proof.
Moreover, by evaluating (verbose-pstack t) (see verbose-pstack)
one can get trace-like information about prover functions, including
time summaries, printed to the screen during a proof. Thanks to Bill Legato
and Robert Krug for initiating this work and to Robert for providing some
initial implementation.
The new command :comp-gcl is identical in functionality,
except that it always leaves .c and .h files when compiling in GCL.
Thanks to Rob Sumners and Vernon Austel for suggesting such a capability.
The macro e/d provides a convenient way to enable some
rules and disable others. It was formerly in a book supplied with the
distribution, books/ihs/ihs-init.lisp, written by Bishop Brock (who we
thank for providing this useful macro).
New distributed books include those in books/ordinals/,
books/rtl/rel3/, and books/misc/simplify-defuns.lisp (which is
documented in books/misc/simplify-defuns.txt).
The :expand hint now accepts a special value, :LAMBDAS, that
tells the ACL2 rewriter to expand all lambda applications (let
expressions). See hints.
A new function zpf has been added as a fast test against 0 for
nonnegative fixnums.
A new macro gc$ allows the user to call the garbage collector of
the underlying Common Lisp. Thanks to Rob Sumners for suggesting this
feature.
It is now possible to monitor simple (abbreviation) rules.
However, as a warning explains, they are still not considered monitored during
preprocessing; see monitor. Thanks to Robert Krug for providing this
improvement.
The second argument of certify-book, if supplied, formerly had to
be either t or a non-negative integer. Now it can be the symbol ?,
in the ACL2 package, indicating that the usual check should be suppressed
on the number of commands that have been executed to create the world in which
certify-book was called.
