(vl-module-weirdint-elim x) → (mv new-x addmods)
Function:
(defun vl-module-weirdint-elim (x) (declare (xargs :guard (vl-module-p x))) (let ((__function__ 'vl-module-weirdint-elim)) (declare (ignorable __function__)) (b* ((x (vl-module-fix x)) ((when (vl-module->hands-offp x)) (mv x nil)) ((vl-module x) x) (warnings x.warnings) ((mv warnings assigns-changedp assigns) (vl-assignlist-weirdint-elim x.assigns warnings)) ((mv warnings modinsts-changedp modinsts) (vl-modinstlist-weirdint-elim x.modinsts warnings)) ((mv warnings gateinsts-changedp gateinsts) (vl-gateinstlist-weirdint-elim x.gateinsts warnings)) ((mv warnings alwayses-changedp alwayses) (vl-alwayslist-weirdint-elim x.alwayses warnings)) ((mv warnings initials-changedp initials) (vl-initiallist-weirdint-elim x.initials warnings)) (changedp (or assigns-changedp modinsts-changedp gateinsts-changedp alwayses-changedp initials-changedp)) ((unless changedp) (mv (change-vl-module x :warnings warnings) nil)) (orig-names (vl-exprlist-names (vl-module-allexprs x))) ((when (or (member-equal "vl-x-wire" orig-names) (member-equal "vl-z-wire" orig-names))) (let ((warnings (fatal :type :vl-bad-names :msg "~m0 already has a wire named \"vl-x-wire\" or \"vl-z-wire\"." :args (list (vl-module->name x))))) (mv (change-vl-module x :warnings warnings) nil))) (temp-module (change-vl-module x :assigns assigns :modinsts modinsts :gateinsts gateinsts :alwayses alwayses :initials initials :warnings warnings)) (new-names (vl-exprlist-names (vl-module-allexprs temp-module))) (need-x-wire (member-equal "vl-x-wire" new-names)) (need-z-wire (member-equal "vl-z-wire" new-names)) ((unless (or need-x-wire need-z-wire)) (let ((warnings (fatal :type :vl-weirdint-not-weird :msg "Expected to at least need X or Z after eliminating weird ints."))) (mv (change-vl-module x :warnings warnings) nil))) (addmods nil) (addmods (if need-x-wire (cons *vl-1-bit-x* addmods) addmods)) (addmods (if need-z-wire (cons *vl-1-bit-z* addmods) addmods)) (nf (vl-starting-namefactory temp-module)) ((mv nf temp-module) (if need-x-wire (vl-module-add-x/z-wire nf temp-module :x) (mv nf temp-module))) ((mv nf temp-module) (if need-z-wire (vl-module-add-x/z-wire nf temp-module :z) (mv nf temp-module))) (- (vl-free-namefactory nf))) (mv temp-module addmods))))
Theorem:
(defthm vl-module-p-of-vl-module-weirdint-elim.new-x (b* (((mv ?new-x ?addmods) (vl-module-weirdint-elim x))) (vl-module-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-p-of-vl-module-weirdint-elim.addmods (b* (((mv ?new-x ?addmods) (vl-module-weirdint-elim x))) (vl-modulelist-p addmods)) :rule-classes :rewrite)
Theorem:
(defthm vl-module-weirdint-elim-mvtypes-1 (true-listp (mv-nth 1 (vl-module-weirdint-elim x))) :rule-classes :type-prescription)
Theorem:
(defthm vl-module-weirdint-elim-of-vl-module-fix-x (equal (vl-module-weirdint-elim (vl-module-fix x)) (vl-module-weirdint-elim x)))
Theorem:
(defthm vl-module-weirdint-elim-vl-module-equiv-congruence-on-x (implies (vl-module-equiv x x-equiv) (equal (vl-module-weirdint-elim x) (vl-module-weirdint-elim x-equiv))) :rule-classes :congruence)