Fast-alist-pop
fast-alist-pop removes the first key-value pair from a fast
alist, provided that the key is not bound in the remainder of the alist.
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 is just CDR. 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 removes the key/value pair corresponding to the CAR
of the alist from its backing hash table.
To maintain both the consistency of the alist with the backing hash table
and constant-time performance, fast-alist-pop has a guard requiring that the
key of that first pair not be bound in the cdr of the alist. Otherwise, simply
removing that pair from the hash table would not be correct, since the key
would remain in the alist bound to some value, which could only be discovered
by linearly traversing the alist.
Note this is just a special case of fast-alist-pop*.
