Major Section: HONS-AND-MEMOIZATION
This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.
The implementation of fast alists is, in many ways, similar to that of ACL2
arrays. Logically, hons-acons is just like acons, and
hons-get is similar to assoc-equal. But under the hood, hash
tables are associated with these alists, and, when a certain discipline is
followed, these functions execute with hash table speeds.
What is this discipline? Each hons-acons operation "steals" the hash
table associated with the alist that is being extended. Because of this, one
must be very conscious of which object is the most recent extension of an alist
and use that extension exclusively.
The only penalty for a failure to keep track of the most recent extension is
a loss of execution speed, not of correctness, and perhaps the annoyance of
some slow-alist-warnings.
Maintaining discipline may require careful passing of a fast alist up and down
through function calls, as with any single threaded object in an applicative
setting, but there is no syntactic enforcement that insists you only use
the most recent extension of an alist as there is for single threaded
objects (stobjs). Also, even with perfectly proper code, discipline can
sometimes be lost due to user interrupts and aborts.
Performance Notes
The keys of fast alists are always normed. Why? In Common Lisp,
equal-based hashing is relatively slow, so to allow the use of eql-based hash
tables, hons-acons and hons-get always hons-copy the keys
involved.
Since alist keys are frequently atoms, this norming activity may often be so fast that you do not need to think about it. But if you are going to use large structures as the keys for your fast alist, this overhead can be significant, and you may want to ensure that your keys are normed ahead of time.
There is no automatic mechanism for reclaiming the hash tables that are
associated with alists. Because of this, to avoid memory leaks, you should
call fast-alist-free to remove the hash table associated with alists
that will no longer be used.
