		Search-engine friendly clone of the ACL2 documentation.

Fast-alist-fork

(fast-alist-fork alist ans) can be used to eliminate "shadowed pairs" from an alist or to copy fast-alists.

This documentation topic assumes familiarity with fast alists; see fast-alists. See fast-alist-fork!, fast-alist-clean, and fast-alist-clean! for related utilities.

Logically, (fast-alist-fork alist ans) is defined as follows:

Function: fast-alist-fork

(defun fast-alist-fork (alist ans)
       (declare (xargs :guard t))
       (cond ((atom alist) ans)
             ((atom (car alist))
              (fast-alist-fork (cdr alist) ans))
             ((hons-assoc-equal (car (car alist)) ans)
              (fast-alist-fork (cdr alist) ans))
             (t (fast-alist-fork (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 fast-alist-fork is potentially expensive, for the following two reasons.

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.
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, fast-alist-fork 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
                                      (fast-alist-fork alist nil))))
  ...)

See fast-alist-free-on-exit and see fast-alist-free.

Subtopics

Hons-shrink-alist: Deprecated feature