Explain-giant-lambda-object
print data related to a large lambda object
Translate will signal an error if it encounters an
“excessively large” lambda object. These objects are so
large they are difficult to comprehend when printed. So the error message
directs you to this documentation topic. To see the lambda object that
caused the error, execute
(explain-giant-lambda-object)
The rest of this documentation topic explains why we detect these objects
and what you can do about them.
When a lambda object is translated we hons-copy it
so that it is uniquely represented. This speeds up the performance of the
compiled lambda cache (see print-cl-cache).
However, if the number of conses in the lambda object is greater than
or equal to (lambda-object-count-max-val), we cause an error. If this
error has been signaled in your session we recommend that you evaluate
(explain-giant-lambda-object), which will tell you more about the
excessively large lambda object. The current value of
(lambda-object-count-max-val) is 200,000. For reference, the largest
function definition in the ACL2 sources (as of Version 8.6) is the mutual-recursion event defining rewrite and its 51 mutually recursive
subfunctions. The total number of conses in that clique is 14,656.
There are generally two ways excessively large lambda objects come
into existence: (1) they are generated automatically, as by macros,
functions, or make-event, or (2) you wrote a small lambda object
but used a big quoted constant in it.
(1) If the offending lambda object was built mechanically, we
recommend that you redefine the generation process so that it introduces a
named function. For example, suppose the lambda object sketched below
is excessively large.
(lambda (x y)
(if (eq x 'FOO1)
(my-foo1 y)
(if (eq x 'FOO2)
(my-foo2 y)
...)))
Then perhaps instead of generating that object you could generate
the definition
(defun my-big-switch (x y)
(if (eq x 'FOO1)
(my-foo1 y)
(if (eq x 'FOO2)
(my-foo2 y)
...)))
And then use the quite small (lambda$ (x y) (my-big-switch x y)) in
place of the offending lambda object. Of course, this is not always
easy to carry out, since it would also require calling defwarrant on
my-big-switch and providing that warrant as a hypothesis to any theorem
involving the new lambda object.
(2) If the offending lambda object just contains large quoted
constants perhaps you can bind a variable to the large value outside of the
lambda object and pass that variable into the lambda object in a
new formal.
For example, suppose the term (regression-suite) returns is a list of
pairs of sample inputs and correct output for testing some software system
whose binary machine code is in the constant declared below.
(defconst *system*
'(#x488b55f0
#x31ff
#xff142570081050
#xf84995b0000
#xf645f801
#xf8573100000
#x807df019
...))
Then we might wish to execute something like the following.
ACL2 !>(loop$ for pair in (regression-suite)
always (equal (sim *system* (car pair)) (cdr pair)))
which simulates the *system* on every input in the regression suite
and compares the result to the known correct answer.
The formal translation of this term is
(always$ '(lambda (loop$-ivar)
(equal (sim '(#x488b55f0
#x31ff
#xff142570081050
#xf84995b0000
#xf645f801
#xf8573100000
#x807df019
...)
(car loop$-ivar))
(cdr loop$-ivar)))
(regression-suite))
Note that the constant *system* has been rendered as its quoted value
and that it is inside of the lambda object. If *system* is a very
large constant, that lambda object may be excessively large.
But we can avoid that by writing this instead.
ACL2 !>(let ((sys *system*))
(loop$ for pair in (regression-suite)
always (equal (sim sys (car pair)) (cdr pair))))
which essentially translates to
(let ((sys '(#x488b55f0
#x31ff
#xff142570081050
#xf84995b0000
#xf645f801
#xf8573100000
#x807df019
dots)))
(always$+ '(lambda (loop$-gvars loop$-ivars)
(equal (sim (car loop$-gvars)
(car (car loop$-ivars)))
(cdr (car loop$-ivars))))
(list sys)
(loop$-as (list (regression-suite)))))
Note that the lambda object no longer contains the large constant.
It now refers to a “global” variable whose value is that of
*system*. The lambda object is quite small.
For what it is worth, the largest single object in the ACL2 image (as of
Version 8.6) is the value of (w state), the logical world. Upon
starting the system (w state) contains 128,784 elements, but contains
multiple pointers to shared substructures (e.g., to tails of itself). The
total number of conses is on the order of (expt 10 655) when counted
naively, but the total number of distinct conses is 1,875,653. So if you
build a lambda object containing the value of (w state) it will be
“excessively large.”
