Handles situations like
(vl-casezx-match-any-expr type test match-exprs ctx warnings) → (mv warnings expr?)
Function:
(defun vl-casezx-match-any-expr (type test match-exprs ctx warnings) (declare (xargs :guard (and (vl-casetype-p type) (vl-expr-p test) (vl-exprlist-p match-exprs) (vl-modelement-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (member type '(:vl-casez :vl-casex)) (vl-expr-welltyped-p test) (posp (vl-expr->finalwidth test)) (equal (vl-expr->finaltype test) :vl-unsigned)))) (let ((__function__ 'vl-casezx-match-any-expr)) (declare (ignorable __function__)) (b* (((when (atom match-exprs)) (mv (fatal :type :vl-casezx-fail :msg "~a0: case list has no match expressions?" :args (list (vl-modelement-fix ctx))) nil)) ((mv warnings compare1) (vl-casezx-matchexpr type test (car match-exprs) ctx warnings)) ((unless compare1) (mv warnings nil)) ((when (atom (cdr match-exprs))) (mv warnings compare1)) ((mv warnings compare-rest) (vl-casezx-match-any-expr type test (cdr match-exprs) ctx warnings)) ((unless compare-rest) (mv warnings nil))) (mv warnings (make-vl-nonatom :op :vl-binary-bitor :args (list compare1 compare-rest) :finaltype :vl-unsigned :finalwidth 1)))))
Theorem:
(defthm vl-warninglist-p-of-vl-casezx-match-any-expr.warnings (b* (((mv ?warnings ?expr?) (vl-casezx-match-any-expr type test match-exprs ctx warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-casezx-match-any-expr.expr? (b* (((mv ?warnings ?expr?) (vl-casezx-match-any-expr type test match-exprs ctx warnings))) (equal (vl-expr-p expr?) (if expr? t nil))) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finalwidth-of-vl-casezx-match-any-expr (b* (((mv ?warnings ?expr?) (vl-casezx-match-any-expr type test match-exprs ctx warnings))) (implies expr? (equal (vl-expr->finalwidth expr?) 1))) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finaltype-of-vl-casezx-match-any-expr (b* (((mv ?warnings ?expr?) (vl-casezx-match-any-expr type test match-exprs ctx warnings))) (implies expr? (equal (vl-expr->finaltype expr?) :vl-unsigned))) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-welltyped-p-of-vl-casezx-match-any-expr (implies (and (vl-expr-welltyped-p test) (posp (vl-expr->finalwidth test)) (equal (vl-expr->finaltype test) :vl-unsigned)) (b* (((mv & result) (vl-casezx-match-any-expr type test match-exprs ctx warnings))) (implies result (vl-expr-welltyped-p result)))))
Theorem:
(defthm vl-casezx-match-any-expr-of-vl-casetype-fix-type (equal (vl-casezx-match-any-expr (vl-casetype-fix type) test match-exprs ctx warnings) (vl-casezx-match-any-expr type test match-exprs ctx warnings)))
Theorem:
(defthm vl-casezx-match-any-expr-vl-casetype-equiv-congruence-on-type (implies (vl-casetype-equiv type type-equiv) (equal (vl-casezx-match-any-expr type test match-exprs ctx warnings) (vl-casezx-match-any-expr type-equiv test match-exprs ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-match-any-expr-of-vl-expr-fix-test (equal (vl-casezx-match-any-expr type (vl-expr-fix test) match-exprs ctx warnings) (vl-casezx-match-any-expr type test match-exprs ctx warnings)))
Theorem:
(defthm vl-casezx-match-any-expr-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casezx-match-any-expr type test match-exprs ctx warnings) (vl-casezx-match-any-expr type test-equiv match-exprs ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-match-any-expr-of-vl-exprlist-fix-match-exprs (equal (vl-casezx-match-any-expr type test (vl-exprlist-fix match-exprs) ctx warnings) (vl-casezx-match-any-expr type test match-exprs ctx warnings)))
Theorem:
(defthm vl-casezx-match-any-expr-vl-exprlist-equiv-congruence-on-match-exprs (implies (vl-exprlist-equiv match-exprs match-exprs-equiv) (equal (vl-casezx-match-any-expr type test match-exprs ctx warnings) (vl-casezx-match-any-expr type test match-exprs-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-match-any-expr-of-vl-modelement-fix-ctx (equal (vl-casezx-match-any-expr type test match-exprs (vl-modelement-fix ctx) warnings) (vl-casezx-match-any-expr type test match-exprs ctx warnings)))
Theorem:
(defthm vl-casezx-match-any-expr-vl-modelement-equiv-congruence-on-ctx (implies (vl-modelement-equiv ctx ctx-equiv) (equal (vl-casezx-match-any-expr type test match-exprs ctx warnings) (vl-casezx-match-any-expr type test match-exprs ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-match-any-expr-of-vl-warninglist-fix-warnings (equal (vl-casezx-match-any-expr type test match-exprs ctx (vl-warninglist-fix warnings)) (vl-casezx-match-any-expr type test match-exprs ctx warnings)))
Theorem:
(defthm vl-casezx-match-any-expr-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-casezx-match-any-expr type test match-exprs ctx warnings) (vl-casezx-match-any-expr type test match-exprs ctx warnings-equiv))) :rule-classes :congruence)