(vl-partselect-type-top-dimension-replacement dim x ctx) → (mv warning range)
Function:
(defun vl-partselect-type-top-dimension-replacement (dim x ctx) (declare (xargs :guard (and (vl-packeddimension-p dim) (vl-expr-p x) (vl-context-p ctx)))) (declare (xargs :guard (and (not (vl-atom-p x)) (member (vl-nonatom->op x) '(:vl-select-colon :vl-select-pluscolon :vl-select-minuscolon :vl-partselect-colon :vl-partselect-pluscolon :vl-partselect-minuscolon))))) (let ((__function__ 'vl-partselect-type-top-dimension-replacement)) (declare (ignorable __function__)) (b* (((vl-nonatom x)) (x (vl-expr-fix x)) (dim (vl-packeddimension-fix dim)) (ctx (vl-context-fix ctx)) ((when (or (eq dim :vl-unsized-dimension) (not (vl-range-resolved-p dim)))) (mv (make-vl-warning :type :vl-partselect-type-unresolved :msg "~a0: Couldn't find type of ~a1 because the ~ most significant dimension of the type of ~ ~a2 was unsized or non-constant." :args (list ctx x (first x.args)) :fn __function__) nil)) ((unless (and (vl-expr-resolved-p (third x.args)) (or (not (member x.op '(:vl-partselect-colon :vl-select-colon))) (vl-expr-resolved-p (second x.args))))) (mv (make-vl-warning :type :vl-partselect-indices-unresolved :msg "~a0: Couldn't find type of ~a1 because the ~ partselect has non-constant indices." :args (list ctx x) :fn __function__) nil)) ((when (member x.op '(:vl-select-colon :vl-partselect-colon))) (mv nil (make-vl-range :msb (second x.args) :lsb (third x.args)))) (width (vl-resolved->val (third x.args))) ((unless (posp width)) (mv (make-vl-warning :type :vl-partselect-indices-unresolved :msg "~a0: Zero width in partselect operator?" :args (list ctx x) :fn __function__) nil)) ((unless (vl-expr-resolved-p (second x.args))) (mv nil (make-vl-range :msb (vl-make-index (1- width)) :lsb (vl-make-index 0)))) (m-or-lsb (vl-resolved->val (second x.args))) (backward-range-p (< (vl-resolved->val (vl-range->msb dim)) (vl-resolved->val (vl-range->lsb dim)))) (greater-idx (if (member x.op '(:vl-select-pluscolon :vl-partselect-pluscolon)) (+ m-or-lsb width -1) m-or-lsb)) (lesser-idx (if (member x.op '(:vl-select-pluscolon :vl-partselect-pluscolon)) m-or-lsb (+ m-or-lsb (- width) 1))) ((when (< lesser-idx 0)) (mv (make-vl-warning :type :vl-partselect-index-error :msg "~a0: Partselect ~s1 operator yields negative index: ~a2" :args (list ctx (if (eq x.op :vl-partselect-pluscolon) "+:" "-:") x) :fn __function__) nil)) (range (make-vl-range :msb (vl-make-index (if backward-range-p lesser-idx greater-idx)) :lsb (vl-make-index (if backward-range-p greater-idx lesser-idx))))) (mv nil range))))
Theorem:
(defthm return-type-of-vl-partselect-type-top-dimension-replacement.warning (b* (((mv common-lisp::?warning ?range) (vl-partselect-type-top-dimension-replacement dim x ctx))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-partselect-type-top-dimension-replacement.range (b* (((mv common-lisp::?warning ?range) (vl-partselect-type-top-dimension-replacement dim x ctx))) (implies (not warning) (vl-range-p range))) :rule-classes :rewrite)
Theorem:
(defthm context-irrelevance-of-vl-partselect-type-top-dimension-replacement (implies (syntaxp (not (equal ctx (list 'quote (with-guard-checking :none (vl-context-fix nil)))))) (and (equal (mv-nth 1 (vl-partselect-type-top-dimension-replacement dim x ctx)) (mv-nth 1 (vl-partselect-type-top-dimension-replacement dim x nil))) (iff (mv-nth 0 (vl-partselect-type-top-dimension-replacement dim x ctx)) (mv-nth 0 (vl-partselect-type-top-dimension-replacement dim x nil))))))
Theorem:
(defthm vl-partselect-type-top-dimension-replacement-of-vl-packeddimension-fix-dim (equal (vl-partselect-type-top-dimension-replacement (vl-packeddimension-fix dim) x ctx) (vl-partselect-type-top-dimension-replacement dim x ctx)))
Theorem:
(defthm vl-partselect-type-top-dimension-replacement-vl-packeddimension-equiv-congruence-on-dim (implies (vl-packeddimension-equiv dim dim-equiv) (equal (vl-partselect-type-top-dimension-replacement dim x ctx) (vl-partselect-type-top-dimension-replacement dim-equiv x ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-partselect-type-top-dimension-replacement-of-vl-expr-fix-x (equal (vl-partselect-type-top-dimension-replacement dim (vl-expr-fix x) ctx) (vl-partselect-type-top-dimension-replacement dim x ctx)))
Theorem:
(defthm vl-partselect-type-top-dimension-replacement-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-partselect-type-top-dimension-replacement dim x ctx) (vl-partselect-type-top-dimension-replacement dim x-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-partselect-type-top-dimension-replacement-of-vl-context-fix-ctx (equal (vl-partselect-type-top-dimension-replacement dim x (vl-context-fix ctx)) (vl-partselect-type-top-dimension-replacement dim x ctx)))
Theorem:
(defthm vl-partselect-type-top-dimension-replacement-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-partselect-type-top-dimension-replacement dim x ctx) (vl-partselect-type-top-dimension-replacement dim x ctx-equiv))) :rule-classes :congruence)