• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
        • Memoize
        • Fast-alists
          • Slow-alist-warning
          • Hons-acons
          • Fast-alist-fork
          • Hons-acons!
          • With-fast-alist
          • Fast-alist-clean
          • Fast-alist-pop
          • Fast-alist-free
          • Fast-alist-pop*
          • Hons-get
          • Hons-assoc-equal
          • Make-fast-alist
          • Make-fal
          • Fast-alist-free-on-exit
          • With-stolen-alist
          • Fast-alist-fork!
          • Fast-alist-summary
          • Fast-alist-clean!
          • Fast-alist-len
          • With-stolen-alists
          • Fast-alists-free-on-exit
          • Cons-subtrees
          • With-fast-alists
          • Hons-dups-p1
          • Ansfl
          • Hons-revappend
          • Hons-member-equal
          • Hons-make-list
          • Hons-reverse
          • Hons-list*
          • Hons-list
          • Hons-append
        • Hons
        • Set-max-mem
        • Hons-enabled
        • Unmemoize
        • Number-subtrees
      • Events
      • History
      • Parallelism
      • Programming
      • Start-here
      • Real
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Alists
  • Programming
  • Hons-and-memoization

Fast-alists

Alists with hidden hash tables for faster execution

The implementation of fast alists is, in many ways, similar to that of ACL2 arrays. Logically, hons-acons is just like acons, and hons-get is similar to assoc-equal. But under the hood, hash tables are associated with these alists, and, when a certain discipline is followed, these functions execute with hash table speeds.

What is this discipline? Each hons-acons operation "steals" the hash table associated with the alist that is being extended. Because of this, one must be very conscious of which object is the most recent extension of an alist and use that extension exclusively.

The only penalty for a failure to keep track of the most recent extension is a loss of execution speed, not of correctness, and perhaps the annoyance of some slow-alist-warnings.

Maintaining discipline may require careful passing of a fast alist up and down through function calls, as with any single threaded object in an applicative setting, but there is no syntactic enforcement that insists you only use the most recent extension of an alist as there is for single threaded objects (stobjs). Also, even with perfectly proper code, discipline can sometimes be lost due to user interrupts and aborts.

Performance Notes

See hons-acons for how the final cdr of a fast alist can be used as a size hint or as a name for reports printed by calling fast-alist-summary.

The keys of fast alists are always normed. Why? In Common Lisp, equal-based hashing is relatively slow, so to allow the use of eql-based hash tables, hons-acons and hons-get always hons-copy the keys involved.

Since alist keys are frequently atoms, this norming activity may often be so fast that you do not need to think about it. But if you are going to use large structures as the keys for your fast alist, this overhead can be significant, and you may want to ensure that your keys are normed ahead of time.

There is no automatic mechanism for reclaiming the hash tables that are associated with alists. Because of this, to avoid memory leaks, you should call fast-alist-free to remove the hash table associated with alists that will no longer be used.

Subtopics

Slow-alist-warning
Warnings/errors issued when fast-alists are used inefficiently
Hons-acons
(hons-acons key val alist) is the main way to create or extend fast-alists.
Fast-alist-fork
(fast-alist-fork alist ans) can be used to eliminate "shadowed pairs" from an alist or to copy fast-alists.
Hons-acons!
(hons-acons! key val alist) is an alternative to hons-acons that produces normed, fast alists.
With-fast-alist
(with-fast-alist name form) causes name to be a fast alist for the execution of form.
Fast-alist-clean
(fast-alist-clean alist) can be used to eliminate "shadowed pairs" from a fast alist.
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.
Fast-alist-free
(fast-alist-free alist) throws away the hash table associated with a fast alist.
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.
Hons-get
(hons-get key alist) is the efficient lookup operation for fast-alists.
Hons-assoc-equal
(hons-assoc-equal key alist) is not fast; it serves as the logical definition for hons-get.
Make-fast-alist
(make-fast-alist alist) creates a fast-alist from the input alist, returning alist itself or, in some cases, a new object equal to it.
Make-fal
Make a fast alist out of an alist.
Fast-alist-free-on-exit
Free a fast alist after the completion of some form.
With-stolen-alist
(with-stolen-alist name form) ensures that name is a fast alist at the start of the execution of form. At the end of execution, it ensures that name is a fast alist if and only if it was originally. That is, if name was not a fast alist originally, its hash table link is freed, and if it was a fast alist originally but its table was modified during the execution of form, that table is restored. Note that any extended table created from the original fast alist during form must be manually freed.
Fast-alist-fork!
(fast-alist-fork! alist ans) is an alternative to fast-alist-fork that produces a normed result.
Fast-alist-summary
(fast-alist-summary) prints some basic statistics about any current fast alists.
Fast-alist-clean!
(fast-alist-clean! alist) is an alternative to fast-alist-clean that produces a normed result.
Fast-alist-len
(fast-alist-len alist) counts the number of unique keys in a fast alist.
With-stolen-alists
Concisely call with-stolen-alist on multiple alists.
Fast-alists-free-on-exit
Concisely call fast-alist-free-on-exit for several alists.
Cons-subtrees
Build a fast alist whose keys are the subtrees of X
With-fast-alists
Concisely call with-fast-alist on multiple alists.
Hons-dups-p1
Basic duplicates check; table is a fast alist that associates already-seen elements with t.
Ansfl
(ANSFL X Y) returns the single value X after first flushing the fast hash table backing for Y, if Y is a fast alist.
Hons-revappend
REVAPPEND using HONS instead of CONS
Hons-member-equal
MEMBER-EQUAL using HONS-EQUAL for each equality check
Hons-make-list
Like make-list, but produces honses.
Hons-reverse
REVERSE using HONS instead of CONS
Hons-list*
(LIST* ...) using HONS instead of CONS
Hons-list
(LIST ...) using HONS instead of CONS
Hons-append
APPEND using HONS instead of CONS