		Search-engine friendly clone of the ACL2 documentation.

Caseelim

Vl-casezx-match-any-expr

Handles situations like casez(foo) ... 3'bxx1, 3'bx10: ... endcase, i.e., where we have multiple match expressions associated with the same body.

Signature
(vl-casezx-match-any-expr type test match-exprs ctx warnings) → (mv warnings expr?)
Arguments: type — Kind of case statement.
Guard (vl-casetype-p type).; test — E.g., for casex(data) ..., data.
Guard (vl-expr-p test).; match-exprs — The match expressions, usually weird integers with wildcard bits.
Guard (vl-exprlist-p match-exprs).; ctx — Context for warnings.
Guard (vl-modelement-p ctx).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; expr? — On failure nil, otherwise an expression that checks whether we have any match.
Type (equal (vl-expr-p expr?) (if expr? t nil)).

Definitions and Theorems

Function: vl-casezx-match-any-expr

(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: vl-warninglist-p-of-vl-casezx-match-any-expr.warnings

(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: return-type-of-vl-casezx-match-any-expr.expr?

(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: vl-expr->finalwidth-of-vl-casezx-match-any-expr

(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: vl-expr->finaltype-of-vl-casezx-match-any-expr

(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: vl-expr-welltyped-p-of-vl-casezx-match-any-expr

(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: vl-casezx-match-any-expr-of-vl-casetype-fix-type

(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: vl-casezx-match-any-expr-vl-casetype-equiv-congruence-on-type

(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: vl-casezx-match-any-expr-of-vl-expr-fix-test

(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: vl-casezx-match-any-expr-vl-expr-equiv-congruence-on-test

(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: vl-casezx-match-any-expr-of-vl-exprlist-fix-match-exprs

(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: vl-casezx-match-any-expr-vl-exprlist-equiv-congruence-on-match-exprs

(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: vl-casezx-match-any-expr-of-vl-modelement-fix-ctx

(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: vl-casezx-match-any-expr-vl-modelement-equiv-congruence-on-ctx

(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: vl-casezx-match-any-expr-of-vl-warninglist-fix-warnings

(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: vl-casezx-match-any-expr-vl-warninglist-equiv-congruence-on-warnings

(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)