(vl-wildeq-rewrite-main x ctx warnings) → (mv new-warnings new-x)
Function:
(defun vl-wildeq-rewrite-main (x ctx warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-context-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (not (vl-atom-p x)) (or (eq (vl-nonatom->op x) :vl-binary-wildeq) (eq (vl-nonatom->op x) :vl-binary-wildneq))))) (let ((__function__ 'vl-wildeq-rewrite-main)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) (ctx (vl-context-fix ctx)) ((unless (vl-expr-welltyped-p x)) (mv (warn :type :vl-wildeq-fail :msg "~a0: failing to simplify wildcard equality operator ~ because it is not well-typed: ~a1." :args (list ctx x)) x)) ((vl-nonatom x) x) ((list lhs rhs) x.args) ((mv okp care-mask zap-expr) (vl-wildeq-decompose-rhs rhs)) ((unless okp) (mv (warn :type :vl-wildeq-fail :msg "~a0: right-hand side of wildcard equality operator ~ is too complex; we only support constants. ~ Expression: ~a1." :args (list ctx x)) x)) (new-x (if (eq x.op :vl-binary-wildeq) (vl-wildeq-replacement-expr lhs care-mask zap-expr x.atts) (vl-wildneq-replacement-expr lhs care-mask zap-expr x.atts)))) (mv (ok) new-x))))
Theorem:
(defthm vl-warninglist-p-of-vl-wildeq-rewrite-main.new-warnings (b* (((mv ?new-warnings ?new-x) (vl-wildeq-rewrite-main x ctx warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-p-of-vl-wildeq-rewrite-main.new-x (b* (((mv ?new-warnings ?new-x) (vl-wildeq-rewrite-main x ctx warnings))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-welltyped-p-after-vl-wildeq-rewrite-main (implies (and (vl-expr-welltyped-p x) (not (vl-atom-p x)) (or (eq (vl-nonatom->op x) :vl-binary-wildeq) (eq (vl-nonatom->op x) :vl-binary-wildneq))) (b* (((mv ?warnings new-x) (vl-wildeq-rewrite-main x ctx warnings))) (and (vl-expr-welltyped-p new-x) (equal (vl-expr->finalwidth new-x) (vl-expr->finalwidth x)) (equal (vl-expr->finaltype new-x) (vl-expr->finaltype x))))))
Theorem:
(defthm vl-wildeq-rewrite-main-of-vl-expr-fix-x (equal (vl-wildeq-rewrite-main (vl-expr-fix x) ctx warnings) (vl-wildeq-rewrite-main x ctx warnings)))
Theorem:
(defthm vl-wildeq-rewrite-main-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-wildeq-rewrite-main x ctx warnings) (vl-wildeq-rewrite-main x-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-wildeq-rewrite-main-of-vl-context-fix-ctx (equal (vl-wildeq-rewrite-main x (vl-context-fix ctx) warnings) (vl-wildeq-rewrite-main x ctx warnings)))
Theorem:
(defthm vl-wildeq-rewrite-main-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-wildeq-rewrite-main x ctx warnings) (vl-wildeq-rewrite-main x ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-wildeq-rewrite-main-of-vl-warninglist-fix-warnings (equal (vl-wildeq-rewrite-main x ctx (vl-warninglist-fix warnings)) (vl-wildeq-rewrite-main x ctx warnings)))
Theorem:
(defthm vl-wildeq-rewrite-main-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-wildeq-rewrite-main x ctx warnings) (vl-wildeq-rewrite-main x ctx warnings-equiv))) :rule-classes :congruence)