Iterates over the indices of an array, creating svex module components for each index using vl-datatype-elem->mod-components
(vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases) → (mv wires insts aliases)
Function:
(defun vl-datatype-dimension->mod-components-tr (count msi incr subwire submod wires insts aliases) (declare (xargs :guard (and (natp count) (integerp msi) (integerp incr) (sv::wire-p subwire) (or (sv::modname-p submod) (not submod)) (sv::wirelist-p wires) (sv::modinstlist-p insts) (sv::lhspairs-p aliases)))) (let ((__function__ 'vl-datatype-dimension->mod-components-tr)) (declare (ignorable __function__)) (b* (((when (zp count)) (mv (rev (sv::wirelist-fix wires)) (rev (sv::modinstlist-fix insts)) (rev (sv::lhspairs-fix aliases)))) (next-count (1- count)) ((mv wire1 insts1 aliases1) (vl-datatype-elem->mod-components (lifix msi) subwire (* (sv::wire->width subwire) next-count) submod))) (vl-datatype-dimension->mod-components-tr next-count (+ (lifix incr) (lifix msi)) incr subwire submod (cons wire1 wires) (revappend-without-guard insts1 insts) (revappend-without-guard aliases1 aliases)))))
Theorem:
(defthm wirelist-p-of-vl-datatype-dimension->mod-components-tr.wires (b* (((mv ?wires ?insts ?aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-datatype-dimension->mod-components-tr.insts (b* (((mv ?wires ?insts ?aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases))) (sv::modinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-datatype-dimension->mod-components-tr.aliases (b* (((mv ?wires ?insts ?aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-of-nfix-count (equal (vl-datatype-dimension->mod-components-tr (nfix count) msi incr subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases)))
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-nat-equiv-congruence-on-count (implies (acl2::nat-equiv count count-equiv) (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count-equiv msi incr subwire submod wires insts aliases))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-of-ifix-msi (equal (vl-datatype-dimension->mod-components-tr count (ifix msi) incr subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases)))
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-int-equiv-congruence-on-msi (implies (acl2::int-equiv msi msi-equiv) (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi-equiv incr subwire submod wires insts aliases))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-of-ifix-incr (equal (vl-datatype-dimension->mod-components-tr count msi (ifix incr) subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases)))
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-int-equiv-congruence-on-incr (implies (acl2::int-equiv incr incr-equiv) (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr-equiv subwire submod wires insts aliases))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-of-wire-fix-subwire (equal (vl-datatype-dimension->mod-components-tr count msi incr (sv::wire-fix subwire) submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases)))
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-wire-equiv-congruence-on-subwire (implies (sv::wire-equiv subwire subwire-equiv) (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire-equiv submod wires insts aliases))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-of-wirelist-fix-wires (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod (sv::wirelist-fix wires) insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases)))
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-wirelist-equiv-congruence-on-wires (implies (sv::wirelist-equiv wires wires-equiv) (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires-equiv insts aliases))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-of-modinstlist-fix-insts (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires (sv::modinstlist-fix insts) aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases)))
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-modinstlist-equiv-congruence-on-insts (implies (sv::modinstlist-equiv insts insts-equiv) (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts-equiv aliases))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-of-lhspairs-fix-aliases (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts (sv::lhspairs-fix aliases)) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases)))
Theorem:
(defthm vl-datatype-dimension->mod-components-tr-lhspairs-equiv-congruence-on-aliases (implies (sv::lhspairs-equiv aliases aliases-equiv) (equal (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases) (vl-datatype-dimension->mod-components-tr count msi incr subwire submod wires insts aliases-equiv))) :rule-classes :congruence)