HONS-ACONS!

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.

Logically, hons-acons! is like acons except that its guard does not require 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 you're doing.

Drawback 1. 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 using 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 constructed with 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 discussion in 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 adequate to 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.