• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
        • Pat->al
        • Pat-flatten1
        • Similar-patternsp
        • Member-of-pat-flatten
        • Pat-flatten
        • Al->pat
        • Assoc-pat->al
        • Subsetp-of-pat-flatten
        • Pat->fal
        • Data-for-patternp
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Patterns

Al->pat

(al->pat pat al default) builds a new data object that is compatible with pat, using the data from al and providing the default value for missing keys.

For instance,

(al->pat '((a (b c)) d)
         '((a . 1) (b . 2) (d . 4))
         'oops)
  -->
((1 (2 oops)) 4)

Note that al should be a fast alist.

Definitions and Theorems

Function: al->pat

(defun al->pat (pat al default)
  (declare (xargs :guard t))
  (if pat (if (atom pat)
              (let ((look (hons-get pat al)))
                (if look (cdr look) default))
            (cons (al->pat (car pat) al default)
                  (al->pat (cdr pat) al default)))
    nil))

Theorem: true-listp-al->pat

(defthm true-listp-al->pat
  (implies (true-listp pat)
           (true-listp (al->pat pat al default)))
  :rule-classes ((:rewrite) (:type-prescription)))

Theorem: len-al->pat

(defthm len-al->pat
  (implies (true-listp pat)
           (equal (len (al->pat pat al default))
                  (len pat))))