• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
        • Address
        • Wire
          • Wire-fix
          • Wire-p
          • Make-wire
          • Wire-equiv
          • Change-wire
          • Wire->name
          • Wire->low-idx
          • Wire->delay
          • Wire->width
          • Wire->type
          • Wire->atts
          • Wirelist
            • Wirelist-fix
            • Wirelist->names
            • Wirelist-p
            • Wirelist-find
            • Wirelist-equiv
          • Wire->revp
          • Wiretype
        • Module
        • Lhs
        • Path
        • Svar-add-namespace
        • Design
        • Modinst
        • Lhs-add-namespace
        • Modalist
        • Path-add-namespace
        • Modname->submodnames
        • Name
        • Constraintlist-addr-p
        • Svex-alist-addr-p
        • Svar-map-addr-p
        • Lhspairs-addr-p
        • Modname
        • Assigns-addr-p
        • Lhs-addr-p
        • Lhatom-addr-p
        • Modhier-list-measure
        • Attributes
        • Modhier-measure
        • Modhier-list-measure-aux
        • Modhier-loopfreelist-p
        • Modhier-loopfree-p
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Wirelist

Wirelist->names

(wirelist->names x) maps wire->name across a list.

Signature

(wirelist->names x) → names

Arguments

x — Guard (wirelist-p x).

Returns

names — Type (namelist-p names).

This is an ordinary defprojection.

Definitions and Theorems

Function: wirelist->names-exec

(defun wirelist->names-exec (x acc)
  (declare (xargs :guard (wirelist-p x)))
  (declare (xargs :guard t))
  (let ((__function__ 'wirelist->names-exec))
    (declare (ignorable __function__))
    (if (consp x)
        (wirelist->names-exec (cdr x)
                              (cons (wire->name (car x)) acc))
      acc)))

Function: wirelist->names-nrev

(defun wirelist->names-nrev (x acl2::nrev)
  (declare (xargs :stobjs (acl2::nrev)))
  (declare (xargs :guard (wirelist-p x)))
  (declare (xargs :guard t))
  (let ((__function__ 'wirelist->names-nrev))
    (declare (ignorable __function__))
    (if (atom x)
        (acl2::nrev-fix acl2::nrev)
      (let ((acl2::nrev (acl2::nrev-push (wire->name (car x))
                                         acl2::nrev)))
        (wirelist->names-nrev (cdr x)
                              acl2::nrev)))))

Function: wirelist->names

(defun wirelist->names (x)
 (declare (xargs :guard (wirelist-p x)))
 (declare (xargs :guard t))
 (let ((__function__ 'wirelist->names))
  (declare (ignorable __function__))
  (mbe
   :logic
   (if (consp x)
       (cons (wire->name (car x))
             (wirelist->names (cdr x)))
     nil)
   :exec
   (if (atom x)
       nil
     (acl2::with-local-nrev (wirelist->names-nrev x acl2::nrev))))))

Theorem: namelist-p-of-wirelist->names

(defthm namelist-p-of-wirelist->names
  (b* ((names (wirelist->names x)))
    (namelist-p names))
  :rule-classes :rewrite)

Theorem: wirelist->names-of-wirelist-fix-x

(defthm wirelist->names-of-wirelist-fix-x
  (equal (wirelist->names (wirelist-fix x))
         (wirelist->names x)))

Theorem: wirelist->names-wirelist-equiv-congruence-on-x

(defthm wirelist->names-wirelist-equiv-congruence-on-x
  (implies (wirelist-equiv x x-equiv)
           (equal (wirelist->names x)
                  (wirelist->names x-equiv)))
  :rule-classes :congruence)

Theorem: wirelist->names-of-take

(defthm wirelist->names-of-take
  (implies (<= (nfix acl2::n) (len x))
           (equal (wirelist->names (take acl2::n x))
                  (take acl2::n (wirelist->names x))))
  :rule-classes ((:rewrite)))

Theorem: wirelist->names-nrev-removal

(defthm wirelist->names-nrev-removal
  (equal (wirelist->names-nrev x acl2::nrev)
         (append acl2::nrev (wirelist->names x)))
  :rule-classes ((:rewrite)))

Theorem: wirelist->names-exec-removal

(defthm wirelist->names-exec-removal
  (equal (wirelist->names-exec x acl2::acc)
         (revappend (wirelist->names x)
                    acl2::acc))
  :rule-classes ((:rewrite)))

Theorem: wirelist->names-of-rev

(defthm wirelist->names-of-rev
  (equal (wirelist->names (rev x))
         (rev (wirelist->names x)))
  :rule-classes ((:rewrite)))

Theorem: wirelist->names-of-list-fix

(defthm wirelist->names-of-list-fix
  (equal (wirelist->names (list-fix x))
         (wirelist->names x))
  :rule-classes ((:rewrite)))

Theorem: wirelist->names-of-append

(defthm wirelist->names-of-append
  (equal (wirelist->names (append acl2::a acl2::b))
         (append (wirelist->names acl2::a)
                 (wirelist->names acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: cdr-of-wirelist->names

(defthm cdr-of-wirelist->names
  (equal (cdr (wirelist->names x))
         (wirelist->names (cdr x)))
  :rule-classes ((:rewrite)))

Theorem: car-of-wirelist->names

(defthm car-of-wirelist->names
  (equal (car (wirelist->names x))
         (and (consp x) (wire->name (car x))))
  :rule-classes ((:rewrite)))

Theorem: wirelist->names-under-iff

(defthm wirelist->names-under-iff
  (iff (wirelist->names x) (consp x))
  :rule-classes ((:rewrite)))

Theorem: consp-of-wirelist->names

(defthm consp-of-wirelist->names
  (equal (consp (wirelist->names x))
         (consp x))
  :rule-classes ((:rewrite)))

Theorem: len-of-wirelist->names

(defthm len-of-wirelist->names
  (equal (len (wirelist->names x))
         (len x))
  :rule-classes ((:rewrite)))

Theorem: true-listp-of-wirelist->names

(defthm true-listp-of-wirelist->names
  (true-listp (wirelist->names x))
  :rule-classes :type-prescription)

Theorem: wirelist->names-when-not-consp

(defthm wirelist->names-when-not-consp
  (implies (not (consp x))
           (equal (wirelist->names x) nil))
  :rule-classes ((:rewrite)))

Theorem: wirelist->names-of-cons

(defthm wirelist->names-of-cons
  (equal (wirelist->names (cons acl2::a acl2::b))
         (cons (wire->name acl2::a)
               (wirelist->names acl2::b)))
  :rule-classes ((:rewrite)))