NOTE-2-7-OTHER

ACL2 Version 2.7 Notes on Miscellaneous Changes
Major Section:  NOTE-2-7

Made several minor documentation improvements. We are grateful to Eric Smith for suggesting (most of) these.

Improved (show-bdd) (see bdd) to give more useful feedback when there are ``leaf'' terms not known to be Boolean.

Sped up processing of large mutual-recursion nests. In one large example the speedup was roughly two orders of magnitude.

Modified event printing so that if both 'prove and 'event are inhibited, then events are no longer printed on behalf of certify-book, encapsulate, or defstobj. Thanks to Eric Smith for prompting consideration of such a change.

The following technical change was made to support with-error-trace and wet (see note-2-7-new-functionality), but may be of interest to those who do low-level programming using the ACL2 logical world. The 'unnormalized-body property is now stored not only for functions defined in :logic mode, but also for functions defined by the user in :program mode. (:Program mode Functions built into ACL2 still have their 'unnormalized-body property omitted, in order to save space.)

The handling of ``invisible'' functions for purposes of controlling rewriting (see loop-stopper) has been moved to a new table; see invisible-fns-table. Macros that access and modify this table are called ``...-invisible-fns-table'' in place of their former names, ``...-invisible-fns-alist.'' This feature was formerly implemented in the acl2-defaults-table, which prevented a book from exporting lists of invisible functions intended to work with the rewrite rules developed in the book. Thanks to Eric Smith and Rob Sumners for suggesting this change. See set-invisible-fns-table (formerly set-invisible-fns-alist), and also see add-invisible-fns and see remove-invisible-fns, which provides ways to incrementally add to and remove from this table, respectively. The handling of printing binary function call nests using macros (See add-binop) has also been moved out of the acl2-defaults-table as suggested by Eric and Rob, but this feature didn't work anyhow (see note-2-7-bug-fixes). Incidentally, the symbols binop-table, add-binop, and remove-binop have all been added to the list *acl2-exports* (see acl2-user), add-invisible-fns and remove-invisible-fns have been added to that list, and set-invisible-fns-alist has been replaced in that list by set-invisible-fns-table. Function invisible-fns-alistp is no longer defined and has been removed from *acl2-exports*.

We now enforce the stated restriction on the pairings in macro-aliases-table (see macro-aliases-table), namely, that it associates names of macros with names of funcions (with respect to the current ACL2 logical world). We make a similar requirement on invisible-fns-table.

The theory-invariant event has been modified so that the default action is an error rather than a warning. Thanks to Eric Smith for suggesting this change. Also, the value returned upon successful execution of a theory-invariant event is now the key.

Proof output that reports destructor elimination no longer uses the word ``generalizing''. This small change may help in browsing proof output, since now ``generaliz'' takes you to true uses of generalization. Thanks to Matyas Sustik for suggesting such a change.

The command :pl now prints an abbreviated controller-alist for ;definition rules. Formerly the output from :pl could be overwhelming when the supplied function was part of a large mutual-recursion nest.

The defaults for keyword parameters of certify-book have changed. See note-2-7-bug-fixes, in particular, the discussion there of two modifications to certify-book.

Technical changes have been made to compress1 and compress2 that should usually be invisible to users. The next paragraph describes them in detail, only for competeness (i.e., that description can be ignored by most users). But first, here is an example showing an effect on users. The slow array warning was not there previously. Notice that the warning only arises if the event form is changed. The solution is to be sure that redundant defconst forms are syntactically identical.

ACL2 !>(defconst *a* (compress1 'demo 
                                '((:header :dimensions (5)
                                           :maximum-length 15
                                           :default uninitialized
                                           :name demo)
                                  (1 . one)
                                  (0 . zero))))

Summary
Form:  ( DEFCONST *A* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 *A*
ACL2 !>(aref1 'demo *a* 0)
ZERO
ACL2 !>(defconst *a* (compress1 'demo 
                                '((:header :dimensions (5)
                                           :maximum-length 15
                                           :default uninitialized
                                           :name demo)
                                  (1 . one)
                                  (0 . zero))))

This event is redundant.  See :DOC redundant-events.

Summary
Form:  ( DEFCONST *A* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 :REDUNDANT
ACL2 !>(aref1 'demo *a* 0)
ZERO
ACL2 !>(defconst *a* (compress1 'demo 
                                '((:header :dimensions (5)
                                           :maximum-length 15
                                           :default uninitialized
                                           :name demo)
                                  (0 . zero)
                                  (1 . one))))

This event is redundant.  See :DOC redundant-events.

Summary
Form:  ( DEFCONST *A* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 :REDUNDANT
ACL2 !>(aref1 'demo *a* 0)


**********************************************************
Slow Array Access!  A call of AREF1 on an array named
DEMO is being executed slowly.  See :DOC slow-array-warning
**********************************************************

ZERO
ACL2 !>

As before, the von Neumann structure stored in the 'acl2-array property of the array name contains the array list object in its car. However, previously it was the case that compress1 and compress2 did not update that car when its new value would be equal to its old value. This was done largely in support of some type-set tables defined using defconst in type-set-b.lisp. The new versions of compress1 and compress2 are simpler in that no such exception is made in the case of equal lists, although instead the entire compression process is short-circuited when the input array list object is eq to the car of the 'acl2-array property. This change was made because the equality test was causing a ``slow array access'' warning to be printed in rare cases during proofs, as described elswhere (see note-2-7-bug-fixes).

We no longer distribute documentation specific to Lucid Emacs. The Info documentation in directory doc/EMACS/ works well both for Gnu Emacs and XEmacs.

A little-advertised macro, value, has long been allowed for top-level forms in books; see embedded-event-form. This has been replaced by a new macro, value-triple. The two have the same semantics at the top-level of books, where state is ``live''. However, value-triple should be used at the top-level of a book, while value should be used in function definitions (as before). This change eliminates a warning put out by the Allegro Common Lisp compiler for top-level value forms in books.