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.