		Search-engine friendly clone of the ACL2 documentation.

Expression-sizing

Vl-assignpattern-multi-replacement

Return the list of type/expression pairs to concatenate together to replace a positional assignment pattern.

Signature
(vl-assignpattern-multi-replacement lhs-type args orig-x ctx warnings) → (mv successp pairs new-warnings)
Arguments: lhs-type — Guard (vl-datatype-p lhs-type).; args — Guard (vl-exprlist-p args).; orig-x — Guard (vl-expr-p orig-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-multi-replacement

(defun vl-assignpattern-multi-replacement
       (lhs-type args orig-x ctx warnings)
 (declare (xargs :guard (and (vl-datatype-p lhs-type)
                             (vl-exprlist-p args)
                             (vl-expr-p orig-x)
                             (vl-context-p ctx)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-assignpattern-multi-replacement))
  (declare (ignorable __function__))
  (b*
   ((ctx (vl-context-fix ctx))
    (orig-x (vl-expr-fix orig-x))
    ((unless (and (eql (len args) 2)
                  (vl-expr-resolved-p (first args))
                  (not (eq (vl-expr-kind (second args)) :atom))
                  (eq (vl-nonatom->op (second args))
                      :vl-concat)))
     (mv
      nil nil
      (warn
          :type :vl-assignpattern-elim-fail
          :msg "~a0: Ill-formed replication assignment pattern: ~a1"
          :args (list ctx orig-x))))
    (replications (vl-resolved->val (first args)))
    (fields (append-n replications
                      (vl-nonatom->args (second args)))))
   (vl-assignpattern-positional-replacement
        lhs-type fields orig-x ctx warnings))))

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

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

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

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

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

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

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

(defthm vl-exprlist-max-count-of-vl-assignpattern-multi-replacement
 (<
  (vl-exprlist-max-count
      (alist-vals (mv-nth 1
                          (vl-assignpattern-multi-replacement
                               lhs-type args orig-x ctx warnings))))
  (vl-exprlist-count args))
 :rule-classes :linear)

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

(defthm sum-sizes-of-vl-assignpattern-multi-replacement
  (b* (((mv ok pairs &)
        (vl-assignpattern-multi-replacement
             lhs-type args orig-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-multi-replacement-of-vl-datatype-fix-lhs-type

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

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

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

Theorem: vl-assignpattern-multi-replacement-of-vl-exprlist-fix-args

(defthm vl-assignpattern-multi-replacement-of-vl-exprlist-fix-args
  (equal (vl-assignpattern-multi-replacement
              lhs-type (vl-exprlist-fix args)
              orig-x ctx warnings)
         (vl-assignpattern-multi-replacement
              lhs-type args orig-x ctx warnings)))

Theorem: vl-assignpattern-multi-replacement-vl-exprlist-equiv-congruence-on-args

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

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

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

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

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

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

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

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

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

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

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

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

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