(hons-acons! key val alist)is an alternative to
produces normed, fast alists.
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.
Ordinarily, fast-alists are constructed with
hons-acons instead of
hons-acons!. In such alists, the keys are honsed, but the conses that make
up the "spine" of the alist itself are ordinary conses. In other words, it
is basically correct to say:
(hons-acons key val alist) == (cons (cons (hons-copy key) val) alist)
In contrast, when
hons-acons! is used, the conses making up the alist
itself are also normed. That is,
(hons-acons! key val alist) == (hons (hons key val) alist)
Generally, you should not use
hons-acons! unless you really know what
hons-acons! requires you to
hons-copy all of the values
that are being stored in the fast alist. If you are storing large values, this
may be expensive.
Drawback 2. It can be more difficult to maintain the proper discipline when
hons-acons!. For instance, consider the following:
(let ((al1 (hons-acons 1 'one (hons-acons 2 'two nil))) (al2 (hons-acons 1 'one (hons-acons 2 'two nil)))) ...)
Here, both al1 and al2 are valid fast alists and they can be extended
independently without any trouble. But if these alists had instead been
hons-acons!, then since both al1 and al2 are equal, normed
conses, they will literally be
eq and hence will refer to precisely the
same hash table. In other words,
hons-acons! makes it relatively easy to
inadvertently steal the hash table associated with some other fast alist.
This problem can be alleviated somewhat by uniquely naming alists; see the
hons-acons for details.
Despite these drawbacks,
hons-acons! is the only way besides
hons-shrink-alist! to generate a fast alist that is normed. It is not
hons-copy a fast alist that was generated by ordinary
hons-acons calls, because this would produce an EQUAL-but-not-EQ object,
and this new object would not be associated with the fast alist's hash table.