• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • Stobj
        • State
        • Memoize
        • Mbe
        • Io
        • Apply$
        • System-utilities
        • Defpkg
        • Mutual-recursion
        • Arrays
        • Programming-with-state
        • Characters
        • Loop$
        • Time$
        • Defmacro
        • Defconst
        • Guard
        • Evaluation
        • Equality-variants
        • 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-make-list
          • Compilation
          • Hons
          • ACL2-built-ins
          • Advanced-features
          • Set-check-invariant-risk
          • Developers-guide
          • Numbers
          • Irrelevant-formals
          • Efficiency
          • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
          • Redefining-programs
          • Lists
          • Invariant-risk
          • Errors
          • Defabbrev
          • Conses
          • Alists
          • Set-register-invariant-risk
          • Program-wrapper
          • Strings
          • Get-internal-time
          • Basics
          • Packages
          • System-attachments
          • Defmacro-untouchable
          • Primitive
          • <<
          • Revert-world
          • Set-duplicate-keys-action
          • Unmemoize
          • Symbols
          • Def-list-constructor
          • Easy-simplify-term
          • Defiteration
          • Defopen
          • Sleep
        • Real
        • ACL2-tutorial
        • Debugging
        • Miscellaneous
        • Prover-output
        • Built-in-theorems
        • Macros
        • Interfacing-tools
        • About-ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Fast-alists
    • ACL2-built-ins

    Fast-alist-clean

    (fast-alist-clean alist) can be used to eliminate "shadowed pairs" from a fast alist.

    This documentation topic assumes familiarity with fast alists; see fast-alists. See fast-alist-clean!, fast-alist-fork, and fast-alist-fork! for related utilities.

    Logically, (fast-alist-clean alist) is defined as follows:

    Function: fast-alist-clean

    (defun fast-alist-clean (alist)
           (declare (xargs :guard t))
           (fast-alist-fork alist
                            (if (consp alist)
                                (cdr (last alist))
                                alist)))

    The result is thus a corresponding fast alist, with the order reversed and with atoms and shadowed pairs removed, as per the definition above; see fast-alist-fork for details. Moreover, if alist is not a fast alist, then (fast-alist-clean alist) is executed in raw Lisp by calling fast-alist-fork as indicated above.

    However, if alist is a fast alist, then a special definition under the hood provides a different handling of associated hash tables. After running (fast-alist-clean alist) to obtain a result, cleaned-alist, the hash table that had been associated with alist will now be associated with cleaned-alist instead. This saves the expense of creating a new hash table, but there is still the expense of copying the alist, as for fast-alist-fork. However, unlike fast-alist-fork, there is no need to free the input alist.

    Note that the final cdr is preserved, so that the name is preserved for use by fast-alist-summary (also see hons-acons).