• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Mutual-recursion
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Loop$-primer
        • Fast-alists
        • Defmacro
        • Defconst
        • Evaluation
        • Guard
        • Equality-variants
        • Compilation
        • Hons
        • ACL2-built-ins
        • Developers-guide
        • System-attachments
        • Advanced-features
        • Set-check-invariant-risk
        • Numbers
        • Irrelevant-formals
        • Efficiency
        • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
        • Redefining-programs
        • Lists
        • Invariant-risk
        • Errors
        • Defabbrev
        • Conses
        • Alists
          • Std/alists
          • Omaps
          • Fast-alists
          • Alistp
          • Misc/records
          • Remove-assocs
          • Assoc
          • Symbol-alistp
          • Rassoc
          • Remove-assoc
          • Remove1-assoc
          • Alist-map-vals
          • Depgraph
          • Alist-map-keys
          • Put-assoc
          • Strip-cars
          • Pairlis$
          • Strip-cdrs
          • Sublis
            • Hons-sublis
          • Acons
          • Eqlable-alistp
          • Assoc-string-equal
          • Standard-string-alistp
          • Alist-to-doublets
          • Character-alistp
          • Alist-keys-subsetp
          • R-symbol-alistp
          • R-eqlable-alistp
          • Pairlis
          • Pairlis-x2
          • Pairlis-x1
          • Delete-assoc
        • Set-register-invariant-risk
        • Strings
        • Program-wrapper
        • Get-internal-time
        • Basics
        • Packages
        • Defmacro-untouchable
        • Primitive
        • <<
        • Revert-world
        • Set-duplicate-keys-action
        • Unmemoize
        • Symbols
        • Def-list-constructor
        • Easy-simplify-term
        • Defiteration
        • Defopen
        • Sleep
      • Start-here
      • Real
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Alists
  • ACL2-built-ins

Sublis

Substitute an alist into a tree

(Sublis alist tree) is obtained by replacing every leaf of tree with the result of looking that leaf up in the association list alist. However, a leaf is left unchanged if it is not found as a key in alist.

Leaves are looked up using the function assoc. The guard for (sublis alist tree) requires (eqlable-alistp alist). This guard ensures that the guard for assoc will be met for each lookup generated by sublis.

Sublis is defined in Common Lisp. See any Common Lisp documentation for more information.

Function: sublis

(defun sublis (alist tree)
       (declare (xargs :guard (eqlable-alistp alist)))
       (cond ((atom tree)
              (let ((pair (assoc tree alist)))
                   (cond (pair (cdr pair)) (t tree))))
             (t (cons (sublis alist (car tree))
                      (sublis alist (cdr tree))))))

Subtopics

Hons-sublis
memoized version of SUBLIS which uses fast-alists.