		Search-engine friendly clone of the ACL2 documentation.

Expression-sizing

Vl-assignpattern-positional-replacement

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

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

(defun vl-assignpattern-positional-replacement
       (lhs-type fields orig-x ctx warnings)
 (declare (xargs :guard (and (vl-datatype-p lhs-type)
                             (vl-exprlist-p fields)
                             (vl-expr-p orig-x)
                             (vl-context-p ctx)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-assignpattern-positional-replacement))
  (declare (ignorable __function__))
  (b*
   ((pdims (vl-datatype->pdims lhs-type))
    (udims (vl-datatype->udims lhs-type))
    ((unless (or (consp udims) (consp pdims)))
     (b*
      (((unless (eq (vl-datatype-kind lhs-type)
                    :vl-struct))
        (mv
         nil nil
         (warn
          :type :vl-assignpattern-elim-fail
          :msg
          "~a0: Positional assignment pattern must be in a ~
                              struct or array type context: ~a1"
          :args (list (vl-context-fix ctx)
                      (vl-expr-fix orig-x)))))
       ((vl-struct lhs-type))
       ((unless (eql (len fields)
                     (len lhs-type.members)))
        (mv
         nil nil
         (warn
          :type :vl-assignpattern-elim-fail
          :msg
          "~a0: Wrong number of fields in positional ~
                              assignment pattern ~a1"
          :args (list (vl-context-fix ctx)
                      (vl-expr-fix orig-x))))))
      (mv t
          (pairlis$ (vl-structmemberlist->types lhs-type.members)
                    (list-fix (vl-exprlist-fix fields)))
          (ok))))
    (dim (if (consp udims)
             (car udims)
           (car pdims)))
    ((unless (and (not (eq dim :vl-unsized-dimension))
                  (vl-range-resolved-p dim)))
     (mv
      nil nil
      (warn
        :type :vl-assignpattern-elim-fail
        :msg "~a0: Unresolved packed dimensions in LHS datatype ~a1"
        :args (list (vl-context-fix ctx)
                    (vl-datatype-fix lhs-type)))))
    ((unless (eql (vl-range-size dim) (len fields)))
     (mv
      nil nil
      (warn
       :type :vl-assignpattern-elim-fail
       :msg
       "~a0: Wrong number of fields in positional assignment ~
                        pattern ~a1"
       :args (list (vl-context-fix ctx)
                   (vl-expr-fix orig-x)))))
    (new-datatype (if (consp udims)
                      (vl-datatype-update-dims pdims (cdr udims)
                                               lhs-type)
                    (vl-datatype-update-dims (cdr pdims)
                                             nil lhs-type))))
   (mv t
       (pairlis$ (repeat (len fields) new-datatype)
                 (list-fix (vl-exprlist-fix fields)))
       (ok)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: vl-assignpattern-positional-replacement-of-vl-exprlist-fix-fields

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

Theorem: vl-assignpattern-positional-replacement-vl-exprlist-equiv-congruence-on-fields

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

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

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

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

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

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

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

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

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

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

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

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

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