		Search-engine friendly clone of the ACL2 documentation.

Oprewrite

Vl-maybe-consolidate-multiconcat

Signature
(vl-maybe-consolidate-multiconcat x) → expr
Arguments: x — Guard (vl-expr-p x).
Returns: expr — Type (vl-expr-p expr).

Definitions and Theorems

Function: vl-maybe-consolidate-multiconcat

(defun vl-maybe-consolidate-multiconcat (x)
 (declare (xargs :guard (vl-expr-p x)))
 (declare (xargs :guard (and (not (vl-atom-p x))
                             (equal (vl-nonatom->op x)
                                    :vl-multiconcat))))
 (let ((__function__ 'vl-maybe-consolidate-multiconcat))
  (declare (ignorable __function__))
  (b*
   ((x (vl-expr-fix x))
    ((list arg1 arg2) (vl-nonatom->args x))
    ((unless (and (vl-fast-atom-p arg1)
                  (vl-fast-constint-p (vl-atom->guts arg1))
                  (posp (vl-constint->value (vl-atom->guts arg1)))
                  (not (vl-fast-atom-p arg2))
                  (eq (vl-nonatom->op arg2) :vl-concat)
                  (eql 1 (len (vl-nonatom->args arg2)))
                  (vl-fast-atom-p (first (vl-nonatom->args arg2)))))
     x)
    (num-copies (vl-constint->value (vl-atom->guts arg1)))
    (original (vl-atom->guts (first (vl-nonatom->args arg2))))
    ((when (and (vl-constint-p original)
                (posp (vl-constint->origwidth original))
                (natp (vl-constint->value original))))
     (b*
      ((width (vl-constint->origwidth original))
       (value (vl-constint->value original))
       (new-width (* num-copies width))
       (new-val
            (vl-replicate-constint-value num-copies width value))
       ((when (< new-val (expt 2 new-width)))
        (make-vl-atom :guts (make-vl-constint :origwidth new-width
                                              :origtype :vl-unsigned
                                              :value new-val))))
      (raise "Out of range??")
      x))
    ((when (and (vl-weirdint-p original)
                (posp (vl-weirdint->origwidth original))))
     (b* ((width (vl-weirdint->origwidth original))
          (bits (vl-weirdint->bits original)))
      (make-vl-atom
        :guts
        (make-vl-weirdint
             :origwidth (* num-copies width)
             :origtype :vl-unsigned
             :bits (vl-replicate-weirdint-bits num-copies bits))))))
   x)))

Theorem: vl-expr-p-of-vl-maybe-consolidate-multiconcat

(defthm vl-expr-p-of-vl-maybe-consolidate-multiconcat
  (b* ((expr (vl-maybe-consolidate-multiconcat x)))
    (vl-expr-p expr))
  :rule-classes :rewrite)

Theorem: vl-maybe-consolidate-multiconcat-of-vl-expr-fix-x

(defthm vl-maybe-consolidate-multiconcat-of-vl-expr-fix-x
  (equal (vl-maybe-consolidate-multiconcat (vl-expr-fix x))
         (vl-maybe-consolidate-multiconcat x)))

Theorem: vl-maybe-consolidate-multiconcat-vl-expr-equiv-congruence-on-x

(defthm
     vl-maybe-consolidate-multiconcat-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-maybe-consolidate-multiconcat x)
                  (vl-maybe-consolidate-multiconcat x-equiv)))
  :rule-classes :congruence)