(vl-casestmt-elim-aux test cases default) → new-stmt
Function:
(defun vl-casestmt-elim-aux (test cases default) (declare (xargs :guard (and (vl-expr-p test) (vl-caselist-p cases) (vl-stmt-p default)))) (declare (xargs :guard (and (vl-expr->finaltype test) (posp (vl-expr->finalwidth test)) (vl-casestmt-sizes-agreep test cases)))) (let ((__function__ 'vl-casestmt-elim-aux)) (declare (ignorable __function__)) (b* ((cases (vl-caselist-fix cases)) ((when (atom cases)) (vl-stmt-fix default)) ((cons match-exprs1 body1) (car cases))) (make-vl-ifstmt :condition (vl-casestmt-compare-expr test match-exprs1) :truebranch body1 :falsebranch (vl-casestmt-elim-aux test (cdr cases) default)))))
Theorem:
(defthm vl-stmt-p-of-vl-casestmt-elim-aux (b* ((new-stmt (vl-casestmt-elim-aux test cases default))) (vl-stmt-p new-stmt)) :rule-classes :rewrite)
Theorem:
(defthm vl-casestmt-elim-aux-of-vl-expr-fix-test (equal (vl-casestmt-elim-aux (vl-expr-fix test) cases default) (vl-casestmt-elim-aux test cases default)))
Theorem:
(defthm vl-casestmt-elim-aux-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casestmt-elim-aux test cases default) (vl-casestmt-elim-aux test-equiv cases default))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-elim-aux-of-vl-caselist-fix-cases (equal (vl-casestmt-elim-aux test (vl-caselist-fix cases) default) (vl-casestmt-elim-aux test cases default)))
Theorem:
(defthm vl-casestmt-elim-aux-vl-caselist-equiv-congruence-on-cases (implies (vl-caselist-equiv cases cases-equiv) (equal (vl-casestmt-elim-aux test cases default) (vl-casestmt-elim-aux test cases-equiv default))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-elim-aux-of-vl-stmt-fix-default (equal (vl-casestmt-elim-aux test cases (vl-stmt-fix default)) (vl-casestmt-elim-aux test cases default)))
Theorem:
(defthm vl-casestmt-elim-aux-vl-stmt-equiv-congruence-on-default (implies (vl-stmt-equiv default default-equiv) (equal (vl-casestmt-elim-aux test cases default) (vl-casestmt-elim-aux test cases default-equiv))) :rule-classes :congruence)