(hons-shrink-alist alist ans) can be used to eliminate "shadowed pairs"
from an alist or to copy 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.
Logically, hons-shrink-alist 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.
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.
