Make-fal
Make a fast alist out of an alist.
Note: it is usually better to use make-fast-alist.
(make-fal al name) copies the alist AL with hons-acons to make a
fast alist that ends with NAME.
Typically name is an atom, and it becomes the final cdr of the
new fast alist. Some atoms have special meanings, e.g., they act as size
hints; see hons-acons for details.
However, name can also be an existing fast alist. In this case, this
fast alist is extended with the new pairs from al, using hons-acons. Note that name will no longer be fast after the call of
make-fal.
There's nothing under-the-hood about make-fal; it just repeatedly calls
hons-acons. The built-in function make-fast-alist is generally
more efficient and can be nicer to reason about because logically it is just
the identity. On the other hand, make-fast-alist can't be used to extend
an existing fast alist like make-fal.
Definitions and Theorems
Function: make-fal
(defun make-fal (al name)
(declare (xargs :guard t))
(cond ((atom al) name)
((atom (car al))
(make-fal (cdr al) name))
(t (hons-acons (caar al)
(cdar al)
(make-fal (cdr al) name)))))
