• 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
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
        • Vl-to-sv
        • Vl-design->sv-design
          • Vl-simpconfig
          • Vl-hierarchy-sv-translation
          • Vl-expr-svex-translation
            • Sv::vl-expr.lisp
              • Vl-scopecontext-to-addr
              • Vl-binaryop-to-svex
              • Vl-expr-to-svex-maybe-typed
              • Vl-datatype-syscall-to-svex
              • Vl-operandinfo-to-svex-preproc
              • Vl-structmemberlist->types
              • Vl-seltrace-to-svex-select
              • Vl-portdecllist->types
              • Vl-operandinfo-to-svex-select
              • Vl-plusminus-partselect->svex
              • Vl-arrayrange->rel-lsb-and-width
              • Vl-unaryop-to-svex
              • Vl-funcall-args-to-ordered
              • Vl-expr-to-svex-lhs
              • Vl-operandinfo-to-svex
              • Vl-array-assignpat-keyval-resolve
              • Vl-err->vfatal
              • Vl-datatypelist-usertype-resolve
              • Vl-upscope-to-svex-upscope
              • Vl-err->fatal
              • Vl-streaming-concat-trunc/extend
              • Vl-operandinfo-base-svar
              • Vl-index-shift-amount
              • Vttree->constraints
              • Vl-slicesize-resolve
              • Vl-function-map-find-matching-aux
              • Vl-funname-lookup
              • Vl-datatype-size-warn
              • Svex-repeat-aux
              • Vl-$test$plusargs-to-svex
              • Svex-extend
              • Vl-structmemberlist-shift-bits
              • Vl-datatype-slot-width/range
              • Vl-datatype-index-shift-amount
              • Vl-datatype-field-shift-amount
              • 4vec-extend
              • Vl-function-pair-inputs-with-actuals
              • Vl-expr-to-svex-untyped
              • Vl-function-map-check-matching
              • Vl-datatype-syscall-remove-dims
              • Svex-concat-list-aux
              • Vttree-add-constraints
              • Vttree-add-warnings
              • Vl-check-struct-assignpat-keys
              • Vl-check-array-assignpat-keys
              • Sv::constraintlist-subst-memo
              • Vl-svex-keyval-index-lookup
              • Vl-function-map-find-matching
              • Vl-convert-dollarsign-to-expr
              • Vttree->constraints-acc
              • Vl-seltrace-type
              • Vl-seltrace-to-path
              • Vl-keyval-member-lookup
              • Svex-repeat
              • Vttree->warnings-acc
              • Vl-trunc/extend-type-err
              • Constraintlist-add-ctx
              • Vl-hidtrace-add-to-path
              • Svex-multiconcat
              • Vttree-join
              • Vl-value-to-string-aux
              • Vl-seltrace-add-to-path
              • Vl-value-to-4vec
              • Vl-expr-to-svex-selfdet
              • Vl-svex-keyval-default-lookup
              • Vl-$test$plusargs-p
              • Vl-value-to-svex
              • Vl-value-in-range
              • Vl-keyval-default-lookup
              • Sv::svexlist-args-extract-constants
              • Vl-string->bits
              • Vl-size-to-unsigned-logic
              • Vl-hidtrace-to-path
              • Svex-concat-list
              • Vttree->warnings
              • Vl-seltrace-unres-count
              • Vl-datatype-index-is-bitselect
              • Vl-bitlist->4vec
              • Vl-svex-keyvallist-vars
              • Vl-hidstep->svex-index
              • Vl-selstep->svex-name
              • Vl-datatypelist-resolved-p
              • Vl-datatype-$unpacked_dimensions
              • Vl-datatype-$dimensions
              • Vl-bitlist->offset
              • Vl-bitlist->onset
              • Vl-streamexprlist-has-with
              • Vl-hidstep-resolved-p
              • Vl-expr-needs-type-context
              • Vl-streamexprlist->exprs
              • Vl-integer-to-string
              • Vl-hidtrace-resolved-p
              • Vl-selstep-resolved-p
              • Vl-select-resolved-p
              • Vl-svex-keyvallist
              • Vl-datatypelist
              • Svex-x
            • Vttree
          • Vl-design->svex-modalist
          • Vl-svstmt
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Sv::vl-expr.lisp

Vl-structmemberlist->types

(vl-structmemberlist->types x) maps vl-structmember->type across a list.

Signature

(vl-structmemberlist->types x) → types

Arguments

x — Guard (vl-structmemberlist-p x).

Returns

types — Type (vl-datatypelist-p types).

This is an ordinary defprojection.

Definitions and Theorems

Function: vl-structmemberlist->types-exec

(defun vl-structmemberlist->types-exec (x acc)
  (declare (xargs :guard (vl-structmemberlist-p x)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-structmemberlist->types-exec))
    (declare (ignorable __function__))
    (if (consp x)
        (vl-structmemberlist->types-exec
             (cdr x)
             (cons (vl-structmember->type (car x))
                   acc))
      acc)))

Function: vl-structmemberlist->types-nrev

(defun vl-structmemberlist->types-nrev (x nrev)
  (declare (xargs :stobjs (nrev)))
  (declare (xargs :guard (vl-structmemberlist-p x)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-structmemberlist->types-nrev))
    (declare (ignorable __function__))
    (if (atom x)
        (nrev-fix nrev)
      (let ((nrev (nrev-push (vl-structmember->type (car x))
                             nrev)))
        (vl-structmemberlist->types-nrev (cdr x)
                                         nrev)))))

Function: vl-structmemberlist->types

(defun vl-structmemberlist->types (x)
 (declare (xargs :guard (vl-structmemberlist-p x)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-structmemberlist->types))
  (declare (ignorable __function__))
  (mbe
    :logic
    (if (consp x)
        (cons (vl-structmember->type (car x))
              (vl-structmemberlist->types (cdr x)))
      nil)
    :exec
    (if (atom x)
        nil
      (with-local-nrev (vl-structmemberlist->types-nrev x nrev))))))

Theorem: vl-datatypelist-p-of-vl-structmemberlist->types

(defthm vl-datatypelist-p-of-vl-structmemberlist->types
  (b* ((types (vl-structmemberlist->types x)))
    (vl-datatypelist-p types))
  :rule-classes :rewrite)

Theorem: vl-structmemberlist->types-of-vl-structmemberlist-fix-x

(defthm vl-structmemberlist->types-of-vl-structmemberlist-fix-x
  (equal (vl-structmemberlist->types (vl-structmemberlist-fix x))
         (vl-structmemberlist->types x)))

Theorem: vl-structmemberlist->types-vl-structmemberlist-equiv-congruence-on-x

(defthm
 vl-structmemberlist->types-vl-structmemberlist-equiv-congruence-on-x
 (implies (vl-structmemberlist-equiv x x-equiv)
          (equal (vl-structmemberlist->types x)
                 (vl-structmemberlist->types x-equiv)))
 :rule-classes :congruence)

Theorem: nthcdr-of-vl-structmemberlist->types

(defthm nthcdr-of-vl-structmemberlist->types
  (equal (nthcdr acl2::n
                 (vl-structmemberlist->types acl2::x))
         (vl-structmemberlist->types (nthcdr acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-structmemberlist->types-of-take

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

Theorem: set-equiv-congruence-over-vl-structmemberlist->types

(defthm set-equiv-congruence-over-vl-structmemberlist->types
  (implies (set-equiv acl2::x acl2::y)
           (set-equiv (vl-structmemberlist->types acl2::x)
                      (vl-structmemberlist->types acl2::y)))
  :rule-classes ((:congruence)))

Theorem: subsetp-of-vl-structmemberlist->types-when-subsetp

(defthm subsetp-of-vl-structmemberlist->types-when-subsetp
  (implies (subsetp acl2::x acl2::y)
           (subsetp (vl-structmemberlist->types acl2::x)
                    (vl-structmemberlist->types acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: member-of-vl-structmember->type-in-vl-structmemberlist->types

(defthm
      member-of-vl-structmember->type-in-vl-structmemberlist->types
  (implies (member acl2::k acl2::x)
           (member (vl-structmember->type acl2::k)
                   (vl-structmemberlist->types acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-structmemberlist->types-nrev-removal

(defthm vl-structmemberlist->types-nrev-removal
  (equal (vl-structmemberlist->types-nrev acl2::x nrev)
         (append nrev
                 (vl-structmemberlist->types acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-structmemberlist->types-exec-removal

(defthm vl-structmemberlist->types-exec-removal
  (equal (vl-structmemberlist->types-exec acl2::x acl2::acc)
         (revappend (vl-structmemberlist->types acl2::x)
                    acl2::acc))
  :rule-classes ((:rewrite)))

Theorem: vl-structmemberlist->types-of-rev

(defthm vl-structmemberlist->types-of-rev
  (equal (vl-structmemberlist->types (rev acl2::x))
         (rev (vl-structmemberlist->types acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-structmemberlist->types-of-list-fix

(defthm vl-structmemberlist->types-of-list-fix
  (equal (vl-structmemberlist->types (list-fix acl2::x))
         (vl-structmemberlist->types acl2::x))
  :rule-classes ((:rewrite)))

Theorem: vl-structmemberlist->types-of-append

(defthm vl-structmemberlist->types-of-append
  (equal (vl-structmemberlist->types (append acl2::a acl2::b))
         (append (vl-structmemberlist->types acl2::a)
                 (vl-structmemberlist->types acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: cdr-of-vl-structmemberlist->types

(defthm cdr-of-vl-structmemberlist->types
  (equal (cdr (vl-structmemberlist->types acl2::x))
         (vl-structmemberlist->types (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: car-of-vl-structmemberlist->types

(defthm car-of-vl-structmemberlist->types
  (equal (car (vl-structmemberlist->types acl2::x))
         (and (consp acl2::x)
              (vl-structmember->type (car acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: vl-structmemberlist->types-under-iff

(defthm vl-structmemberlist->types-under-iff
  (iff (vl-structmemberlist->types acl2::x)
       (consp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: consp-of-vl-structmemberlist->types

(defthm consp-of-vl-structmemberlist->types
  (equal (consp (vl-structmemberlist->types acl2::x))
         (consp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: len-of-vl-structmemberlist->types

(defthm len-of-vl-structmemberlist->types
  (equal (len (vl-structmemberlist->types acl2::x))
         (len acl2::x))
  :rule-classes ((:rewrite)))

Theorem: true-listp-of-vl-structmemberlist->types

(defthm true-listp-of-vl-structmemberlist->types
  (true-listp (vl-structmemberlist->types acl2::x))
  :rule-classes :type-prescription)

Theorem: vl-structmemberlist->types-when-not-consp

(defthm vl-structmemberlist->types-when-not-consp
  (implies (not (consp acl2::x))
           (equal (vl-structmemberlist->types acl2::x)
                  nil))
  :rule-classes ((:rewrite)))

Theorem: vl-structmemberlist->types-of-cons

(defthm vl-structmemberlist->types-of-cons
  (equal (vl-structmemberlist->types (cons acl2::a acl2::b))
         (cons (vl-structmember->type acl2::a)
               (vl-structmemberlist->types acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: vl-datatypelist-resolved-p-of-vl-structmemberlist->types

(defthm vl-datatypelist-resolved-p-of-vl-structmemberlist->types
  (b* ((?types (vl-structmemberlist->types x)))
    (implies (vl-structmemberlist-resolved-p x)
             (vl-datatypelist-resolved-p types))))