Rewrite an
(vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) → (mv warnings new-stmt)
Function:
(defun vl-casezx-stmt-elim (type check test cases default atts ctx warnings ss) (declare (xargs :guard (and (vl-casetype-p type) (vl-casecheck-p check) (vl-expr-p test) (vl-caselist-p cases) (vl-stmt-p default) (vl-atts-p atts) (vl-modelement-p ctx) (vl-warninglist-p warnings) (vl-scopestack-p ss)))) (declare (xargs :guard (member type '(:vl-casez :vl-casex)))) (let ((__function__ 'vl-casezx-stmt-elim)) (declare (ignorable __function__)) (b* ((type (vl-casetype-fix type)) (check (vl-casecheck-fix check)) (test (vl-expr-fix test)) (ctx (vl-modelement-fix ctx)) (?ss (vl-scopestack-fix ss)) (warnings (vl-warninglist-fix warnings)) (new-warnings (vl-casestmt-size-warnings test cases ctx)) (new-warnings (if (and (vl-expr-welltyped-p test) (posp (vl-expr->finalwidth test)) (eq (vl-expr->finaltype test) :vl-unsigned)) new-warnings (warn :type :vl-casezx-fail :msg "~a0: can't handle ~s1 statement because ~ the test expression ~a2 is either signed, ~ unsized, or of size 0." :args (list ctx (if (eq type :vl-casex) "casex" "casez") test) :acc new-warnings))) ((when new-warnings) (mv (append-without-guard new-warnings warnings) (make-vl-casestmt :casetype type :check check :test test :caselist cases :default default :atts atts))) (warnings (if check (warn :type :vl-casezx-check :msg "~a0: we don't yet implement priority, unique, or ~ unique0 checking for casez/x statements. We will ~ treat this as an ordinary casez/x statement." :args (list (vl-modelement-fix ctx))) warnings)) ((mv warnings new-stmt) (vl-casezx-elim-aux type test cases default ctx warnings)) ((unless new-stmt) (b* ((warnings (warn :type :vl-casezx-unsafe-conversion :msg "~a0: ~s1 statement is not supported, so we ~ are processing it as a regular case ~ statement, which may be unsound." :args (list ctx (if (eq type :vl-casex) "casex" "casez"))))) (vl-casestmt-elim check test cases default atts ctx warnings)))) (mv warnings new-stmt))))
Theorem:
(defthm vl-warninglist-p-of-vl-casezx-stmt-elim.warnings (b* (((mv ?warnings ?new-stmt) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-stmt-p-of-vl-casezx-stmt-elim.new-stmt (b* (((mv ?warnings ?new-stmt) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss))) (vl-stmt-p new-stmt)) :rule-classes :rewrite)
Theorem:
(defthm vl-casezx-stmt-elim-of-vl-casetype-fix-type (equal (vl-casezx-stmt-elim (vl-casetype-fix type) check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss)))
Theorem:
(defthm vl-casezx-stmt-elim-vl-casetype-equiv-congruence-on-type (implies (vl-casetype-equiv type type-equiv) (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type-equiv check test cases default atts ctx warnings ss))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-stmt-elim-of-vl-casecheck-fix-check (equal (vl-casezx-stmt-elim type (vl-casecheck-fix check) test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss)))
Theorem:
(defthm vl-casezx-stmt-elim-vl-casecheck-equiv-congruence-on-check (implies (vl-casecheck-equiv check check-equiv) (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check-equiv test cases default atts ctx warnings ss))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-stmt-elim-of-vl-expr-fix-test (equal (vl-casezx-stmt-elim type check (vl-expr-fix test) cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss)))
Theorem:
(defthm vl-casezx-stmt-elim-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test-equiv cases default atts ctx warnings ss))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-stmt-elim-of-vl-caselist-fix-cases (equal (vl-casezx-stmt-elim type check test (vl-caselist-fix cases) default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss)))
Theorem:
(defthm vl-casezx-stmt-elim-vl-caselist-equiv-congruence-on-cases (implies (vl-caselist-equiv cases cases-equiv) (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases-equiv default atts ctx warnings ss))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-stmt-elim-of-vl-stmt-fix-default (equal (vl-casezx-stmt-elim type check test cases (vl-stmt-fix default) atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss)))
Theorem:
(defthm vl-casezx-stmt-elim-vl-stmt-equiv-congruence-on-default (implies (vl-stmt-equiv default default-equiv) (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default-equiv atts ctx warnings ss))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-stmt-elim-of-vl-atts-fix-atts (equal (vl-casezx-stmt-elim type check test cases default (vl-atts-fix atts) ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss)))
Theorem:
(defthm vl-casezx-stmt-elim-vl-atts-equiv-congruence-on-atts (implies (vl-atts-equiv atts atts-equiv) (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts-equiv ctx warnings ss))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-stmt-elim-of-vl-modelement-fix-ctx (equal (vl-casezx-stmt-elim type check test cases default atts (vl-modelement-fix ctx) warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss)))
Theorem:
(defthm vl-casezx-stmt-elim-vl-modelement-equiv-congruence-on-ctx (implies (vl-modelement-equiv ctx ctx-equiv) (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx-equiv warnings ss))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-stmt-elim-of-vl-warninglist-fix-warnings (equal (vl-casezx-stmt-elim type check test cases default atts ctx (vl-warninglist-fix warnings) ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss)))
Theorem:
(defthm vl-casezx-stmt-elim-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-stmt-elim-of-vl-scopestack-fix-ss (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings (vl-scopestack-fix ss)) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss)))
Theorem:
(defthm vl-casezx-stmt-elim-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss) (vl-casezx-stmt-elim type check test cases default atts ctx warnings ss-equiv))) :rule-classes :congruence)