		Search-engine friendly clone of the ACL2 documentation.

Expression-sizing

Vl-assignpattern-replacement

Signature
(vl-assignpattern-replacement lhs-type x ctx warnings) → (mv successp pairs new-warnings)
Arguments: lhs-type — Guard (vl-datatype-p lhs-type).; x — Guard (vl-expr-p x).; ctx — Guard (vl-context-p ctx).; warnings — Guard (vl-warninglist-p warnings).
Returns: successp — Type (booleanp successp).; pairs — Type (vl-type-expr-pairs-p pairs).; new-warnings — Type (vl-warninglist-p new-warnings).

Definitions and Theorems

Function: vl-assignpattern-replacement

(defun vl-assignpattern-replacement (lhs-type x ctx warnings)
 (declare (xargs :guard (and (vl-datatype-p lhs-type)
                             (vl-expr-p x)
                             (vl-context-p ctx)
                             (vl-warninglist-p warnings))))
 (declare
  (xargs
      :guard
      (and (not (vl-atom-p x))
           (member (vl-nonatom->op x)
                   '(:vl-pattern-positional
                         :vl-pattern-multi :vl-pattern-keyvalue)))))
 (let ((__function__ 'vl-assignpattern-replacement))
  (declare (ignorable __function__))
  (b* (((vl-nonatom x)))
   (case
       x.op
       (:vl-pattern-positional (vl-assignpattern-positional-replacement
                                    lhs-type x.args x ctx warnings))
       (:vl-pattern-multi (vl-assignpattern-multi-replacement
                               lhs-type x.args x ctx warnings))
       (:vl-pattern-keyvalue (vl-assignpattern-keyvalue-replacement
                                  lhs-type x.args x ctx warnings))
       (otherwise (mv (mbe :logic nil :exec 'impossible)
                      nil nil))))))

Theorem: booleanp-of-vl-assignpattern-replacement.successp

(defthm booleanp-of-vl-assignpattern-replacement.successp
  (b* (((mv ?successp ?pairs ?new-warnings)
        (vl-assignpattern-replacement lhs-type x ctx warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-type-expr-pairs-p-of-vl-assignpattern-replacement.pairs

(defthm vl-type-expr-pairs-p-of-vl-assignpattern-replacement.pairs
  (b* (((mv ?successp ?pairs ?new-warnings)
        (vl-assignpattern-replacement lhs-type x ctx warnings)))
    (vl-type-expr-pairs-p pairs))
  :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-assignpattern-replacement.new-warnings

(defthm
      vl-warninglist-p-of-vl-assignpattern-replacement.new-warnings
  (b* (((mv ?successp ?pairs ?new-warnings)
        (vl-assignpattern-replacement lhs-type x ctx warnings)))
    (vl-warninglist-p new-warnings))
  :rule-classes :rewrite)

Theorem: vl-exprlist-max-count-of-vl-assignpattern-replacement

(defthm vl-exprlist-max-count-of-vl-assignpattern-replacement
 (implies
  (not (vl-atom-p x))
  (<
   (vl-exprlist-max-count
    (alist-vals
      (mv-nth
           1
           (vl-assignpattern-replacement lhs-type x ctx warnings))))
   (vl-expr-count x)))
 :rule-classes :linear)

Theorem: sum-sizes-of-vl-assignpattern-replacement

(defthm sum-sizes-of-vl-assignpattern-replacement
  (b* (((mv ok pairs &)
        (vl-assignpattern-replacement lhs-type x ctx warnings))
       ((mv warning size)
        (vl-datatype-size lhs-type))
       ((mv warning1 size-sum)
        (vl-type-expr-pairs-sum-datatype-sizes pairs)))
    (implies (and ok (not warning))
             (and (not warning1)
                  (equal size-sum size)))))

Theorem: vl-assignpattern-replacement-of-vl-datatype-fix-lhs-type

(defthm vl-assignpattern-replacement-of-vl-datatype-fix-lhs-type
  (equal (vl-assignpattern-replacement (vl-datatype-fix lhs-type)
                                       x ctx warnings)
         (vl-assignpattern-replacement lhs-type x ctx warnings)))

Theorem: vl-assignpattern-replacement-vl-datatype-equiv-congruence-on-lhs-type

(defthm
 vl-assignpattern-replacement-vl-datatype-equiv-congruence-on-lhs-type
 (implies
  (vl-datatype-equiv lhs-type lhs-type-equiv)
  (equal
      (vl-assignpattern-replacement lhs-type x ctx warnings)
      (vl-assignpattern-replacement lhs-type-equiv x ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-assignpattern-replacement-of-vl-expr-fix-x

(defthm vl-assignpattern-replacement-of-vl-expr-fix-x
  (equal (vl-assignpattern-replacement lhs-type (vl-expr-fix x)
                                       ctx warnings)
         (vl-assignpattern-replacement lhs-type x ctx warnings)))

Theorem: vl-assignpattern-replacement-vl-expr-equiv-congruence-on-x

(defthm vl-assignpattern-replacement-vl-expr-equiv-congruence-on-x
 (implies
  (vl-expr-equiv x x-equiv)
  (equal
      (vl-assignpattern-replacement lhs-type x ctx warnings)
      (vl-assignpattern-replacement lhs-type x-equiv ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-assignpattern-replacement-of-vl-context-fix-ctx

(defthm vl-assignpattern-replacement-of-vl-context-fix-ctx
  (equal
       (vl-assignpattern-replacement lhs-type x (vl-context-fix ctx)
                                     warnings)
       (vl-assignpattern-replacement lhs-type x ctx warnings)))

Theorem: vl-assignpattern-replacement-vl-context-equiv-congruence-on-ctx

(defthm
    vl-assignpattern-replacement-vl-context-equiv-congruence-on-ctx
 (implies
  (vl-context-equiv ctx ctx-equiv)
  (equal
      (vl-assignpattern-replacement lhs-type x ctx warnings)
      (vl-assignpattern-replacement lhs-type x ctx-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-assignpattern-replacement-of-vl-warninglist-fix-warnings

(defthm vl-assignpattern-replacement-of-vl-warninglist-fix-warnings
 (equal
  (vl-assignpattern-replacement lhs-type
                                x ctx (vl-warninglist-fix warnings))
  (vl-assignpattern-replacement lhs-type x ctx warnings)))

Theorem: vl-assignpattern-replacement-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-assignpattern-replacement-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
      (vl-assignpattern-replacement lhs-type x ctx warnings)
      (vl-assignpattern-replacement lhs-type x ctx warnings-equiv)))
 :rule-classes :congruence)