• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
          • Unparameterization
          • Elaborate
          • Addnames
          • Annotate
            • Increment-elim
            • Make-implicit-wires
            • Basic-bind-elim
            • Argresolve
            • Basicsanity
            • Portdecl-sign
            • Enum-names
            • Port-resolve
            • Udp-elim
              • Vl-udp-vardecls-from-portdecls
              • Vl-udps-to-modules
                • Vl-udpline-match-expr
                • Vl-combinational-udptable-synth
                • Vl-udptable-assignrhs
                • Vl-udp-to-module
                • Vl-udp-vardecl-from-portdecl
                • Vl-design-udp-elim
              • Vl-annotate-design
              • Vl-annotate-module
            • Clean-warnings
            • Eliminitial
            • Custom-transform-hooks
            • Problem-modules
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Udp-elim

    Vl-udps-to-modules

    (vl-udps-to-modules x) maps vl-udp-to-module across a list.

    Signature
    (vl-udps-to-modules x) → mods
    Arguments
    x — Guard (vl-udplist-p x).
    Returns
    mods — Type (vl-modulelist-p mods).

    This is an ordinary defprojection.

    Definitions and Theorems

    Function: vl-udps-to-modules-exec

    (defun vl-udps-to-modules-exec (x acc)
     (declare (xargs :guard (vl-udplist-p x)))
     (declare (xargs :guard t))
     (let ((__function__ 'vl-udps-to-modules-exec))
       (declare (ignorable __function__))
       (if
         (consp x)
         (vl-udps-to-modules-exec (cdr x)
                                  (cons (vl-udp-to-module (car x)) acc))
         acc)))

    Function: vl-udps-to-modules-nrev

    (defun vl-udps-to-modules-nrev (x nrev)
      (declare (xargs :stobjs (nrev)))
      (declare (xargs :guard (vl-udplist-p x)))
      (declare (xargs :guard t))
      (let ((__function__ 'vl-udps-to-modules-nrev))
        (declare (ignorable __function__))
        (if (atom x)
            (nrev-fix nrev)
          (let ((nrev (nrev-push (vl-udp-to-module (car x))
                                 nrev)))
            (vl-udps-to-modules-nrev (cdr x)
                                     nrev)))))

    Function: vl-udps-to-modules

    (defun vl-udps-to-modules (x)
      (declare (xargs :guard (vl-udplist-p x)))
      (declare (xargs :guard t))
      (let ((__function__ 'vl-udps-to-modules))
        (declare (ignorable __function__))
        (mbe :logic
             (if (consp x)
                 (cons (vl-udp-to-module (car x))
                       (vl-udps-to-modules (cdr x)))
               nil)
             :exec
             (if (atom x)
                 nil
               (with-local-nrev (vl-udps-to-modules-nrev x nrev))))))

    Theorem: vl-modulelist-p-of-vl-udps-to-modules

    (defthm vl-modulelist-p-of-vl-udps-to-modules
      (b* ((mods (vl-udps-to-modules x)))
        (vl-modulelist-p mods))
      :rule-classes :rewrite)

    Theorem: vl-udps-to-modules-of-update-nth

    (defthm vl-udps-to-modules-of-update-nth
     (implies
        (<= (nfix acl2::n) (len acl2::x))
        (equal (vl-udps-to-modules (update-nth acl2::n acl2::v acl2::x))
               (update-nth acl2::n (vl-udp-to-module acl2::v)
                           (vl-udps-to-modules acl2::x))))
     :rule-classes ((:rewrite)))

    Theorem: vl-udps-to-modules-of-revappend

    (defthm vl-udps-to-modules-of-revappend
      (equal (vl-udps-to-modules (revappend acl2::x acl2::y))
             (revappend (vl-udps-to-modules acl2::x)
                        (vl-udps-to-modules acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: nthcdr-of-vl-udps-to-modules

    (defthm nthcdr-of-vl-udps-to-modules
      (equal (nthcdr acl2::n (vl-udps-to-modules acl2::x))
             (vl-udps-to-modules (nthcdr acl2::n acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: nth-of-vl-udps-to-modules

    (defthm nth-of-vl-udps-to-modules
      (equal (nth acl2::n (vl-udps-to-modules acl2::x))
             (and (< (nfix acl2::n) (len acl2::x))
                  (vl-udp-to-module (nth acl2::n acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: vl-udps-to-modules-of-take

    (defthm vl-udps-to-modules-of-take
      (implies (<= (nfix acl2::n) (len acl2::x))
               (equal (vl-udps-to-modules (take acl2::n acl2::x))
                      (take acl2::n (vl-udps-to-modules acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: set-equiv-congruence-over-vl-udps-to-modules

    (defthm set-equiv-congruence-over-vl-udps-to-modules
      (implies (set-equiv acl2::x acl2::y)
               (set-equiv (vl-udps-to-modules acl2::x)
                          (vl-udps-to-modules acl2::y)))
      :rule-classes ((:congruence)))

    Theorem: subsetp-of-vl-udps-to-modules-when-subsetp

    (defthm subsetp-of-vl-udps-to-modules-when-subsetp
      (implies (subsetp acl2::x acl2::y)
               (subsetp (vl-udps-to-modules acl2::x)
                        (vl-udps-to-modules acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: member-of-vl-udp-to-module-in-vl-udps-to-modules

    (defthm member-of-vl-udp-to-module-in-vl-udps-to-modules
      (implies (member acl2::k acl2::x)
               (member (vl-udp-to-module acl2::k)
                       (vl-udps-to-modules acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-udps-to-modules-nrev-removal

    (defthm vl-udps-to-modules-nrev-removal
      (equal (vl-udps-to-modules-nrev acl2::x nrev)
             (append nrev (vl-udps-to-modules acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-udps-to-modules-exec-removal

    (defthm vl-udps-to-modules-exec-removal
      (equal (vl-udps-to-modules-exec acl2::x acl2::acc)
             (revappend (vl-udps-to-modules acl2::x)
                        acl2::acc))
      :rule-classes ((:rewrite)))

    Theorem: vl-udps-to-modules-of-rev

    (defthm vl-udps-to-modules-of-rev
      (equal (vl-udps-to-modules (rev acl2::x))
             (rev (vl-udps-to-modules acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-udps-to-modules-of-list-fix

    (defthm vl-udps-to-modules-of-list-fix
      (equal (vl-udps-to-modules (list-fix acl2::x))
             (vl-udps-to-modules acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: vl-udps-to-modules-of-append

    (defthm vl-udps-to-modules-of-append
      (equal (vl-udps-to-modules (append acl2::a acl2::b))
             (append (vl-udps-to-modules acl2::a)
                     (vl-udps-to-modules acl2::b)))
      :rule-classes ((:rewrite)))

    Theorem: cdr-of-vl-udps-to-modules

    (defthm cdr-of-vl-udps-to-modules
      (equal (cdr (vl-udps-to-modules acl2::x))
             (vl-udps-to-modules (cdr acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: car-of-vl-udps-to-modules

    (defthm car-of-vl-udps-to-modules
      (equal (car (vl-udps-to-modules acl2::x))
             (and (consp acl2::x)
                  (vl-udp-to-module (car acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: vl-udps-to-modules-under-iff

    (defthm vl-udps-to-modules-under-iff
      (iff (vl-udps-to-modules acl2::x)
           (consp acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: consp-of-vl-udps-to-modules

    (defthm consp-of-vl-udps-to-modules
      (equal (consp (vl-udps-to-modules acl2::x))
             (consp acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: len-of-vl-udps-to-modules

    (defthm len-of-vl-udps-to-modules
      (equal (len (vl-udps-to-modules acl2::x))
             (len acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: true-listp-of-vl-udps-to-modules

    (defthm true-listp-of-vl-udps-to-modules
      (true-listp (vl-udps-to-modules acl2::x))
      :rule-classes :type-prescription)

    Theorem: vl-udps-to-modules-when-not-consp

    (defthm vl-udps-to-modules-when-not-consp
      (implies (not (consp acl2::x))
               (equal (vl-udps-to-modules acl2::x)
                      nil))
      :rule-classes ((:rewrite)))

    Theorem: vl-udps-to-modules-of-cons

    (defthm vl-udps-to-modules-of-cons
      (equal (vl-udps-to-modules (cons acl2::a acl2::b))
             (cons (vl-udp-to-module acl2::a)
                   (vl-udps-to-modules acl2::b)))
      :rule-classes ((:rewrite)))