Major Section: NOTE-2-6
A fundamental change is the provision of the ``nu-rewriter'' for
simplifying expressions composed of NTH, UPDATE-NTH, and
UPDATE-NTH-ARRAY applications and LET expressions and other
calls of non-recursive functions or LAMBDA expressions involving
those symbols. The nu-rewriter applies the obvious rewrite rule for
(NTH i (UPDATE-NTH j v s)) and the analogous rule for
UPDATE-NTH-ARRAY. See nu-rewriter The nu-rewriter can be
enabled with set-nu-rewriter-mode.
A new flag has been added to the xargs of defun permitting
the declaration that the function is non-executable. The
usage is (declare (xargs :non-executable t)) and the effect is that
the function has no executable counterpart. On the positive side: the
function is permitted to use single-threaded object names and functions
arbitrarily, as in theorems rather than as in executable definitions.
Such functions are not permitted to declare any names :stobjs but
accessors, etc., may be used, just as in theorems.
A new flag has been added to permit the system to abbreviate output
by introducing LET* notation identifying common subterms. The
formula being proved is not affected; this flag changes its
displayed form only. See set-let*-abstractionp.
A ``raw mode'' has been added, primarily for faster loading of applications. see set-raw-mode.
Functions alphorder and lexorder have been put in :logic mode.
Lexorder is now a total order ordering of the ACL2 universe, and
theorems are included to that effect. Thanks to Pete Manolios for
suggesting the idea and providing events to use, and to Rob Sumners
for assistance with some modifications. See also the new book
books/misc/total-order for an irreflexive total order.
The ACL2 user can now make system calls to the host operating system. See sys-call and see sys-call-status. Thanks to Rob Sumners for working out this idea with Pete Manolios and Robert Krug, who we also thank, and for working out the implementation with us.
It is no longer required to use absolute pathnames in include-book
forms that have been executed before a certify-book. Any relative
pathname strings in such contexts will be expanded into absolute
pathnames before they are saved in the portcullis of the certificate
of the book being certified.
ACL2 can now be built on top of Allegro Common Lisp 6.0, and also on Windows platforms on top of Allegro Common Lisp and GCL. Thanks to Pete Manolios and Vinay K. Siddhavanahalli for their help with Windows.
Rob Sumners has designed and provided an initial implementation for two
improvements to defstobj (also see stobj). First, array fields can
now be resized. Resize and length functions are provided for array fields,
which can be used to resize stobj array fields dynamically. The recognizers
for array fields have been simplified to accommodate this change, so that
they only check that each element of the array field has the specified type.
Second, performance has been improved for stobjs with a large number of
fields, by changing their Common Lisp implementation to store the fields in a
simple vector instead of a list.
Now stobjs may be bound locally; see with-local-stobj. Thanks to Rob Sumners, who encouraged us to implement this capability, was an early user of it, and participated usefully in discussions on its design.
New functions fms!, fmt!, and fmt1! are the same as their respective
functions without the ``!,'' except that the ``!'' functions are
guaranteed to print forms that can be read back in (at a slight
readability cost).
We added extended-metafunctions, metafunctions which
allow state and context sensitive rewriting to some
extent. We thank Robert Krug for pushing for and on this idea.
The documentation has been improved. In particular, a new
documentation topic provides a gentle introduction to ACL2
arrays -- see arrays-example -- and additional
documentation has been provided for getting started with proof trees
in emacs -- see proof-tree-emacs.
New Makefile targets fasl and o have been added to the books/
directory of the distribution. For example, you might first certify
books using an ACL2 built on top of GCL (which creates compiled
files with suffix o). Then, when standing in the books/
directory, you might execute the command
which will create compiled (make fasl ACL2=my-allegro-acl2
.fasl) files for Allegro Common
Lisp, assuming that my-allegro-acl2 starts up an ACL2 built on
that Common Lisp.
The macro let* now allows variables to be declared ignored.
See let* and see let.
The user may now control backchaining. This feature was designed and primarily implemented by Robert Krug (though the authors of ACL2 are resposible for any errors); thanks, Robert! See backchain-limit.
It is now possible to ``slow down'' the rate at which case splits are generated by the simplifier. See set-case-split-limitations.
Accesses to stobjs using nth or update-nth are now
displayed using symbolic constants instead of numeric indices. For
example, given the event
(defstobj foo a b :renaming ((b c)))then the term
(nth 0 foo) will be displayed (for example, during
proofs) as (nth *a* foo) while (nth 1 foo) will be displayed
as (nth *c* foo). The defstobj event now correspondingly
introduces a defconst event for each field accessor function,
introducing a constant whose name is obtained from the accessor's
name by prefixing and suffixin a ``*,'' as in the example above:
accessor a generates (defconst *a* 0) and accessor c
generates (defconst *c* 1). See nth-aliases-table for how to
extend this feature for alternate names of stobjs.Computed hints have been improved. It is now possible to detect within a computed hint whether the goal clause is stable under simplification; it is also possible for a computed hint to change the list of available hints. See computed-hints.
It is now possible to provide ``default hints'' that are appended to the hints explicitly provided. See set-default-hints.
Using computed hints (see computed-hints) and default hints
(see set-default-hints) it is possible to implement a book that
supports ``priority phased simplification.'' Using this book
you can assign priorities to your rules and cause the theorem
prover to simplify each goal maximally under all the rules of
one priority before enabling rules of the next priority.
See books/misc/priorities.lisp.
The macro defabbrev has been improved to allow declare forms and
documentation strings and to do more error-checking. Thanks to Rob Sumners
for designing this enhancement and providing the first implementation.
See defabbrev.
Further changes were made to support CMU Lisp. Wolfhard Buss helped with these changes.
A new table was added that is used when printing proof output, so
that nests of right-associated calls of a binary function are
replaced by corresponding macro calls, as has been the case for
binary-+ and +, binary-append and append, and so on.
See add-binop.
Operators logand, logior, logxor, and logeqv are now
macros (formerly, they were functions) that call corresponding
binary functions (e.g., binary-logand) defined in source file
"axioms.lisp". Thanks to Rob Sumners for this enhancement. Proof
output will however continue to show calls of logand, logior,
logxor, and logeqv.
Function (allocate-fixnum-range fixnum-lo fixnum-hi) sets aside more
"permanent" fixnums in GCL.
ACL2 now runs under CLISP. Thanks to Wolfhard Buss and Sam
Steingold for their assistance with the port.
Michael ``Bogo'' Bogomolny has created a search engine, accessible from the ACL2 home page. For that purpose he modified the HTML translator to create one file per topic (a good idea in any case). Thanks, Bogo!
An emacs file of potential (but optional) use for ACL2 users may be
found in emacs/emacs-acl2.el. In particular, this file supports
the use of proof trees (see proof-tree).
Some books have been added or modified. In particular, Robert Krug has
contributed books/arithmetic-2/, which provides an alternative to the
existing collection of books about arithmetic, books/arithmetic/. For a
discussion of the distributed books see the link to README.html in the
installation instructions.