• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • 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
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Patterns

    Member-of-pat-flatten

    (member-of-pat-flatten a pat) is an optimized way to ask if a is a member of (pat-flatten1 pat).

    This just avoids actually flattening the pattern, and picks a function with optimized EQ/EQL/EQUAL testing.

    Definitions and Theorems

    Function: member-eq-of-pat-flatten

    (defun member-eq-of-pat-flatten (a pat)
      (declare (xargs :guard (symbolp a)))
      (mbe :logic
           (if (member-equal a (pat-flatten1 pat))
               t
             nil)
           :exec
           (if pat (if (atom pat)
                       (eq a pat)
                     (or (member-eq-of-pat-flatten a (car pat))
                         (member-eq-of-pat-flatten a (cdr pat))))
             nil)))

    Function: member-eql-of-pat-flatten

    (defun member-eql-of-pat-flatten (a pat)
      (declare (xargs :guard (eqlablep a)))
      (mbe :logic
           (if (member-equal a (pat-flatten1 pat))
               t
             nil)
           :exec
           (if pat (if (atom pat)
                       (eql a pat)
                     (or (member-eql-of-pat-flatten a (car pat))
                         (member-eql-of-pat-flatten a (cdr pat))))
             nil)))

    Function: member-equal-of-pat-flatten-aux

    (defun member-equal-of-pat-flatten-aux (a pat)
      (declare (xargs :guard t))
      (mbe :logic
           (if (member-equal a (pat-flatten1 pat))
               t
             nil)
           :exec
           (if pat (if (atom pat)
                       (equal a pat)
                     (or (member-equal-of-pat-flatten-aux a (car pat))
                         (member-equal-of-pat-flatten-aux a (cdr pat))))
             nil)))

    Function: member-of-pat-flatten

    (defun member-of-pat-flatten (a pat)
      (declare (xargs :guard t))
      (mbe :logic
           (if (member-equal a (pat-flatten1 pat))
               t
             nil)
           :exec (cond ((symbolp a)
                        (member-eq-of-pat-flatten a pat))
                       ((or (acl2-numberp a) (characterp a))
                        (member-eql-of-pat-flatten a pat))
                       (t (member-equal-of-pat-flatten-aux a pat)))))