Get the range, if any, for a data type.
(vl-datatype-range-conservative x) → (mv warning range)
The datatype should be fully resolved, as in the output from vl-datatype-usertype-elim.
This is like vl-datatype-range, but it only works on single-dimensional vectors of basic 1-bit types. Why? A lot of existing code is built around an assumption that the range of a variable determines its width. In that code, if we use vl-datatype-range, then we'll be silently doing the wrong thing in a lot of cases.
.Function:
(defun vl-datatype-range-conservative (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype-range-conservative)) (declare (ignorable __function__)) (b* (((fun (fail msg args)) (mv (make-vl-warning :type :vl-datatype-range-fail :msg msg :args args) nil)) ((fun (success range)) (mv nil range)) (x (vl-datatype-fix x)) (udims (vl-datatype->udims x)) ((when (consp udims)) (fail "Unpacked dims present." nil)) ((when (and (eq (vl-datatype-kind x) :vl-coretype) (member (vl-coretype->name x) '(:vl-logic :vl-reg :vl-bit)))) (b* ((dims (vl-coretype->pdims x)) ((when (atom dims)) (success nil)) ((when (and (atom (cdr dims)) (not (eq (car dims) :vl-unsized-dimension)))) (success (car dims)))) (fail "Multiple packed dims present" nil)))) (fail "Complex type." nil))))
Theorem:
(defthm return-type-of-vl-datatype-range-conservative.warning (b* (((mv common-lisp::?warning ?range) (vl-datatype-range-conservative x))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm vl-maybe-range-p-of-vl-datatype-range-conservative.range (b* (((mv common-lisp::?warning ?range) (vl-datatype-range-conservative x))) (vl-maybe-range-p range)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-range-conservative-of-vl-datatype-fix-x (equal (vl-datatype-range-conservative (vl-datatype-fix x)) (vl-datatype-range-conservative x)))
Theorem:
(defthm vl-datatype-range-conservative-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype-range-conservative x) (vl-datatype-range-conservative x-equiv))) :rule-classes :congruence)