Fgl-fast-alist-support
Support for hash-based fast alists in FGL
FGL supports the use of fast alist primitives (see ACL2::fast-alists) in its rewriter. However, for accesses and updates to be
fast, the user must ensure the following conditions are met:
- The keys of the alist are always concrete values. (The values need not be
concrete.)
- The alist must only be used in a single-threaded, imperative-style manner,
just as with ACL2 fast alists. For example, the following usage will cause a
slow lookup to occur:
(let* ((al1 (hons-acons 'a 'aa nil))
(al2 (hons-acons 'b 'bb al1)))
(hons-get 'a al1))
The alist must not be modified within an if branch and then accessed
outside that branch, unless care is taken to arrange the branch merging such
that the keys of the alist remain concrete.
For another approach to fast lookups in alists, see fgl-array-support.
