• 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

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)))))