[acl2/acl2] b28cf2: Made some efficiency improvements (motivated by ob...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: b28cf2c037881fe6e567dc80184a6299bf81656b
https://github.com/acl2/acl2/commit/b28cf2c037881fe6e567dc80184a6299bf81656b
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-11-19 (Sat, 19 Nov 2016)

Changed paths:
M acl2-fns.lisp
M axioms.lisp
M books/misc/check-acl2-exports.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M memoize-raw.lisp
M memoize.lisp

Log Message:
-----------
Made some efficiency improvements (motivated by observed poor performance of read-object).

Quoting :doc note-7-3:

Several low-level efficiency improvements, which can speed up
[read-object], may also speed up some other operations.

* Finding a package from a string can be faster (low-level raw Lisp
function find-package-fast).
* The implementation of low-level raw Lisp function bad-lisp-objectp
was tweaked to use type recognizers, which are faster in some
Lisps than corresponding recognizer predicates; for example,
the test (consp x) has been replaced by the test (typep x
'cons).
* New raw Lisp function bad-lisp-consp processes conses on behalf of
bad-lisp-objectp, and now bad-lisp-consp is memoized at startup
instead of bad-lisp-objectp. Note that we continue to use
memoization option :forget t, which throws away memoization
information when exiting the top-level call of the function.
With this change, we avoid the overhead of memoization when
checking non-cons values, which was perhaps of limited value
anyhow. There could be slowdown when large EQ strings occur
repeatedly inside a cons pair, but we expect such slowdown to
be at most negligible in practice.
* New utility set-bad-lisp-consp-memoize can turn off memoization of
the new raw Lisp function bad-lisp-consp.

Not mentioned above (maybe will add it later): a dynamic-extent
declaration in read-object can save substantial consing.

Note: I observed about another 1% (after turning off memoization for
bad-lisp-objectp) by eliminating some infix-printing code from
read-object. J and I talked about perhaps eliminating such code a
couple of years ago, but it seemed that it was working, so we decided
to leave it in. We could change our minds about that some day.

[GitHub]

Branch: refs/heads/testing