Get the unpacked dimensions from any datatype.
(vl-datatype->udims x) → udims
Function:
(defun vl-datatype->udims (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype->udims)) (declare (ignorable __function__)) (vl-datatype-case x :vl-coretype x.udims :vl-struct x.udims :vl-union x.udims :vl-enum x.udims :vl-usertype x.udims)))
Theorem:
(defthm vl-dimensionlist-p-of-vl-datatype->udims (b* ((udims (vl-datatype->udims x))) (vl-dimensionlist-p udims)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype->udims-of-vl-datatype-fix-x (equal (vl-datatype->udims (vl-datatype-fix x)) (vl-datatype->udims x)))
Theorem:
(defthm vl-datatype->udims-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype->udims x) (vl-datatype->udims x-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-dimensionlist-count-of-vl-datatype->pdims/udims (b* nil (< (+ (vl-dimensionlist-count (vl-datatype->pdims x)) (vl-dimensionlist-count (vl-datatype->udims x))) (vl-datatype-count x))) :rule-classes :linear)
These are goofy rules: normally we want to normalize things to
Theorem:
(defthm vl-datatype-udims-when-vl-coretype (implies (vl-datatype-case x :vl-coretype) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-coretype))) (equal (vl-datatype->udims x) (vl-coretype->udims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-coretype)))) (equal (vl-coretype->udims x) (vl-datatype->udims x))))))
Theorem:
(defthm vl-datatype-udims-when-vl-struct (implies (vl-datatype-case x :vl-struct) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-struct))) (equal (vl-datatype->udims x) (vl-struct->udims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-struct)))) (equal (vl-struct->udims x) (vl-datatype->udims x))))))
Theorem:
(defthm vl-datatype-udims-when-vl-union (implies (vl-datatype-case x :vl-union) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-union))) (equal (vl-datatype->udims x) (vl-union->udims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-union)))) (equal (vl-union->udims x) (vl-datatype->udims x))))))
Theorem:
(defthm vl-datatype-udims-when-vl-enum (implies (vl-datatype-case x :vl-enum) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-enum))) (equal (vl-datatype->udims x) (vl-enum->udims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-enum)))) (equal (vl-enum->udims x) (vl-datatype->udims x))))))
Theorem:
(defthm vl-datatype-udims-when-vl-usertype (implies (vl-datatype-case x :vl-usertype) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-usertype))) (equal (vl-datatype->udims x) (vl-usertype->udims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-usertype)))) (equal (vl-usertype->udims x) (vl-datatype->udims x))))))