(hons-acons key val alist)is the main way to create or extend
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.
hons-acons is like
acons except that its guard does not
alistp; we leave it enabled and would think it odd to ever prove
a theorem about it.
Under the hood, two things are done differently. First, the key is copied with
hons-copy; this lets us use EQL-based hash tables instead of
EQUAL-based hash tables for better performance. Second, assuming there is a
valid hash table associated with this alist, we destructively update the hash
table by binding key to val. The hash table will no longer be associated with
alist, but will instead be associated with the new alist returned by
Hash Table Creation
A new hash table is created by
hons-acons whenever alist is an atom.
acons, we do not require that alist be nil, and in fact you
may wish to use a non-nil value for one of two reasons.
1. As a size hint
By default, the new hash table will be given a quite modest default capacity of 60 elements. As more elements are added, the table may need to be resized to accommodate them, and this resizing has some runtime cost.
When a natural number is used as a fast alist's name, we interpret it as a size
hint. For example,
(hons-acons 'foo 'bar 1000) instructs us to use 1000 as
the initial size for this hash table and binds 'foo to 'bar. The resulting
table should not need to be resized until more than 1000 elements are added.
We ignore size hints that request fewer than 60 elements.
Because of hash collisions, hash tables typically need to have a larger size than the actual number of elements they contain. The hash tables for fast alists are told to grow when they reach 70% full. So, an easy rule of thumb might be: multiply the expected number of elements you need by 1.5 to keep your hash tables about 2/3 full.
2. As an alist name
We also frequently use a symbol for alist, and think of this symbol as the name of the new alist. We have found that naming alists can be valuable for two reasons:
First, the name can be helpful in identifying fast alists that should have been
Second, names can sometimes be used to avoid a subtle and insidious
table-stealing phenomenon that occurs when using fast-alists that are
themselves normed; see
At the moment, there is no way to simultaneously name a fast alist and also give it a size hint. We may eventually allow strings to include embedded name and size components, but for now we have not implemented this capability.