		Search-engine friendly clone of the ACL2 documentation.

Note-2-6

Note-2-6-new-functionality

ACL2 Version 2.6 Notes on New Functionality

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.

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

make fasl ACL2=my-allegro-acl2

which will create compiled (.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 responsible 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 suffixing 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.