HONS-SHRINK-ALIST

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. It assumes familiarity with fast alists; see fast-alists.

Logically, (hons-shrink-alist alist ans) is defined as follows:

 (cond ((atom alist)
        ans)
       ((atom (car alist))
        (hons-shrink-alist (cdr alist) ans))
       ((hons-assoc-equal (car (car alist)) ans)
        (hons-shrink-alist (cdr alist) ans))
       (t
        (hons-shrink-alist (cdr alist) (cons (car alist) ans))))

The alist argument need not be a fast alist.

Typically ans is set to nil or some other atom. In this case, shrinking produces a new, fast alist which is like alist except that (1) any "malformed," atomic entries have been removed, (2) all "shadowed pairs" have been removed, and (3) incidentally, the surviving elements have been reversed. This can be useful as a way to clean up any unnecessary bindings in alist, or as a way to obtain a "deep copy" of a fast alist that can extended independently from the original while maintaining discipline.

Note that hons-shrink-alist is potentially expensive, for the following two reasons.

o The alist is copied, dropping any shadowed pairs. This process will require a hash table lookup for each entry in the alist; and it will require creating a new alist, which uses additional memory.

o Unless ans is a fast alist that is stolen (see below), a new hash table is created, which uses additional memory. This hash table is populated in time that is linear in the number of unique keys in the alist.

When ans is not an atom, good discipline requires that it is a fast alist. In this case, hons-shrink-alist steals the hash table for ans and extends it with all of the bindings in alist that are not in ans. From the perspective of hons-assoc-equal, you can think of the resulting alist as being basically similar to (append ans alist), but in a different order.

Note that when ans is not a fast alist (e.g., ans is an atom) then such stealing does not take place.

A common idiom is to replace an alist by the result of shrinking it, in which case it is best to free the input alist, for example as follows.

  (let ((alist (fast-alist-free-on-exit alist
                                        (hons-shrink-alist alist nil))))
    ...)