Creates, e.g., the expression
(vl-casestmt-compare-expr test match-exprs) → compare-expr
Function:
(defun vl-casestmt-compare-expr (test match-exprs) (declare (xargs :guard (and (vl-expr-p test) (vl-exprlist-p match-exprs)))) (declare (xargs :guard (and (vl-expr->finaltype test) (posp (vl-expr->finalwidth test)) (vl-casestmt-matchexpr-sizes-agreep test match-exprs)))) (let ((__function__ 'vl-casestmt-compare-expr)) (declare (ignorable __function__)) (b* (((when (atom match-exprs)) (raise "Case statement with zero match expressions?") |*sized-1'bx*|) (compare1 (vl-casestmt-compare-expr1 test (car match-exprs))) ((when (atom (cdr match-exprs))) compare1) (compare-rest (vl-casestmt-compare-expr test (cdr match-exprs)))) (make-vl-nonatom :op :vl-binary-bitor :args (list compare1 compare-rest) :finaltype :vl-unsigned :finalwidth 1))))
Theorem:
(defthm vl-expr-p-of-vl-casestmt-compare-expr (b* ((compare-expr (vl-casestmt-compare-expr test match-exprs))) (vl-expr-p compare-expr)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finalwidth-of-vl-casestmt-compare-expr (b* ((compare-expr (vl-casestmt-compare-expr test match-exprs))) (equal (vl-expr->finalwidth compare-expr) 1)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finaltype-of-vl-casestmt-compare-expr (b* ((compare-expr (vl-casestmt-compare-expr test match-exprs))) (equal (vl-expr->finaltype compare-expr) :vl-unsigned)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-welltyped-p-of-vl-casestmt-compare-expr (implies (and (force (posp (vl-expr->finalwidth test))) (force (vl-expr->finaltype test)) (force (vl-casestmt-matchexpr-sizes-agreep test match-exprs)) (force (vl-expr-welltyped-p test)) (force (vl-exprlist-welltyped-p match-exprs))) (vl-expr-welltyped-p (vl-casestmt-compare-expr test match-exprs))))
Theorem:
(defthm vl-casestmt-compare-expr-of-vl-expr-fix-test (equal (vl-casestmt-compare-expr (vl-expr-fix test) match-exprs) (vl-casestmt-compare-expr test match-exprs)))
Theorem:
(defthm vl-casestmt-compare-expr-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casestmt-compare-expr test match-exprs) (vl-casestmt-compare-expr test-equiv match-exprs))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-compare-expr-of-vl-exprlist-fix-match-exprs (equal (vl-casestmt-compare-expr test (vl-exprlist-fix match-exprs)) (vl-casestmt-compare-expr test match-exprs)))
Theorem:
(defthm vl-casestmt-compare-expr-vl-exprlist-equiv-congruence-on-match-exprs (implies (vl-exprlist-equiv match-exprs match-exprs-equiv) (equal (vl-casestmt-compare-expr test match-exprs) (vl-casestmt-compare-expr test match-exprs-equiv))) :rule-classes :congruence)