Fast-alist-pop*
fast-alist-pop* removes the first key-value pair from a fast
alist, rebinding that key to its previous value in the backing hash table.
That value must be provided as the prev-binding argument.
This is a user extension to the ACL2 (in particular, ACL2H) system.
It may eventually be added to acl2h proper, but until then it requires a trust
tag since it hasn't been thoroughly vetted for soundness.
Logically, (fast-alist-pop* pair x) is just (cdr x). However, it
has a special side-effect when called on a fast alist (see hons-acons).
A fast alist has a backing hash table mapping its keys to their
corresponding (unshadowed) pairs, which supports constant-time alist lookup.
Hons-acons adds key/value pairs to the alist and its backing hash table,
and hons-get performs constant-time lookup by finding the backing hash
table and looking up the key in the table. However, logically, hons-get is
just hons-assoc-equal, a more traditional alist lookup function that
traverses the alist until it finds the matching key. Correspondingly,
fast-alist-pop* is logically just CDR, but it undoes the binding in the backing
hash table represented by the CAR of the alist. The guard requires that the
prev-binding argument is the shadowed binding of (caar x) in the
remainder of the alist, so to undo that binding in the backing hash table, we
associate that key to the cdr of the prev-binding.
