Iterates over the fields of a union, creating svex module components for each field using vl-datatype-elem->mod-components
(vl-union-fields->mod-components members subwires submodnames) → (mv wires insts aliases width)
Function:
(defun vl-union-fields->mod-components (members subwires submodnames) (declare (xargs :guard (and (vl-structmemberlist-p members) (sv::wirelist-p subwires) (sv::maybe-modnamelist-p submodnames)))) (declare (xargs :guard (and (equal (len subwires) (len members)) (equal (len submodnames) (len members))))) (let ((__function__ 'vl-union-fields->mod-components)) (declare (ignorable __function__)) (b* (((when (atom members)) (mv nil nil nil 0)) ((vl-structmember x) (car members)) ((mv wires insts aliases width) (vl-union-fields->mod-components (cdr members) (cdr subwires) (cdr submodnames))) ((mv wire1 insts1 aliases1) (vl-datatype-elem->mod-components x.name (car subwires) 0 (car submodnames)))) (mv (cons wire1 wires) (append-without-guard insts1 insts) (append-without-guard aliases1 aliases) (max (sv::wire->width wire1) width)))))
Theorem:
(defthm wirelist-p-of-vl-union-fields->mod-components.wires (b* (((mv ?wires ?insts ?aliases ?width) (vl-union-fields->mod-components members subwires submodnames))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-union-fields->mod-components.insts (b* (((mv ?wires ?insts ?aliases ?width) (vl-union-fields->mod-components members subwires submodnames))) (sv::modinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-union-fields->mod-components.aliases (b* (((mv ?wires ?insts ?aliases ?width) (vl-union-fields->mod-components members subwires submodnames))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-vl-union-fields->mod-components.width (b* (((mv ?wires ?insts ?aliases ?width) (vl-union-fields->mod-components members subwires submodnames))) (natp width)) :rule-classes :type-prescription)
Theorem:
(defthm posp-width-of-vl-union-fields->mod-components (b* (((mv ?wires ?insts ?aliases ?width) (vl-union-fields->mod-components members subwires submodnames))) (implies (consp members) (posp width))) :rule-classes :type-prescription)
Theorem:
(defthm vars-of-vl-union-fields->mod-components (b* (((mv ?wires ?insts ?aliases ?width) (vl-union-fields->mod-components members subwires submodnames))) (sv::svarlist-addr-p (sv::lhspairs-vars aliases))) :rule-classes :rewrite)
Theorem:
(defthm vl-union-fields->mod-components-of-vl-structmemberlist-fix-members (equal (vl-union-fields->mod-components (vl-structmemberlist-fix members) subwires submodnames) (vl-union-fields->mod-components members subwires submodnames)))
Theorem:
(defthm vl-union-fields->mod-components-vl-structmemberlist-equiv-congruence-on-members (implies (vl-structmemberlist-equiv members members-equiv) (equal (vl-union-fields->mod-components members subwires submodnames) (vl-union-fields->mod-components members-equiv subwires submodnames))) :rule-classes :congruence)
Theorem:
(defthm vl-union-fields->mod-components-of-wirelist-fix-subwires (equal (vl-union-fields->mod-components members (sv::wirelist-fix subwires) submodnames) (vl-union-fields->mod-components members subwires submodnames)))
Theorem:
(defthm vl-union-fields->mod-components-wirelist-equiv-congruence-on-subwires (implies (sv::wirelist-equiv subwires subwires-equiv) (equal (vl-union-fields->mod-components members subwires submodnames) (vl-union-fields->mod-components members subwires-equiv submodnames))) :rule-classes :congruence)